Naslov
Modeling constraint satisfaction problem with model checker

Autori
Blašković, Bruno ; Škopljanac-Mačina, Frano ; Knežević, Petar ; Palić , Niko

Vrsta, podvrsta i kategorija rada
Radovi u zbornicima skupova, cjeloviti rad (in extenso), znanstveni

Izvornik
Proceedings of the 29th DAAAM International Symposium 2018 / - , 2018, 1-9

Skup
29th DAAAM International Symposium on intelligent manufacturing and automation

Mjesto i datum
Zadar, Hrvatska, 24.10.2018. - 27.10.2018

Vrsta sudjelovanja
Poster

Vrsta recenzije
Međunarodna recenzija

Ključne riječi
constraint satisfaction problem ; SMT solver ; model checking ; Spin/Promela ; sudoku

Sažetak
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.

Izvorni jezik
Engleski

Znanstvena područja
Elektrotehnika, Računarstvo

POVEZANOST RADA