engleski

Modeling constraint satisfaction problem with model checker

In this paper we interpret constraint satisfaction problem (CSP) with model checker Spin and bounded model checkers from satisfiability modulo theories (SMT) solvers. Our previous experience shows that single example modelled in different ways and interpreted with the same solver can have different space and time consumption. The goal is to find a feasible translation from of CSP problem to model checker and SMT solver. For that purpose we build Promela models for Spin model checker and Z3 models for SMT solver. Domain problem used in examples is graph colouring applied to Sudoku puzzle. In the beginning we briefly introduce CSP, model checking, graph colouring and Sudoku puzzle. The central part of this paper deals with various modelling efforts of Sudoku puzzle. After that results are analysed and compared. The main benefits of this paper are twofold, as we use them for educational purposes within Formal Methods in System Design course and as a solution to industrial scale problems like wavelength assignment in photonic networks respectively. At the end we give a conclusion and propose future research directions.

constraint satisfaction problem ; SMT solver ; model checking ; Spin/Promela ; sudoku

nije evidentirano