Pretražite po imenu i prezimenu autora, mentora, urednika, prevoditelja

Napredna pretraga

Pregled bibliografske jedinice broj: 971515

Modeling constraint satisfaction problem with model checker


Blašković, Bruno; Škopljanac-Mačina, Frano; Knežević, Petar; Palić , Niko
Modeling constraint satisfaction problem with model checker // Proceedings of the 29th DAAAM International Symposium 2018
Zadar, Hrvatska, 2018. str. 1-9 (poster, međunarodna recenzija, cjeloviti rad (in extenso), znanstveni)


CROSBI ID: 971515 Za ispravke kontaktirajte CROSBI podršku putem web obrasca

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
The 29th DAAAM International Symposium Intelligent Manufacturing & Automation: Focus on Sustainability

Mjesto i datum
Zadar, Hrvatska, 24-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


Ustanove:
Fakultet elektrotehnike i računarstva, Zagreb


Citiraj ovu publikaciju:

Blašković, Bruno; Škopljanac-Mačina, Frano; Knežević, Petar; Palić , Niko
Modeling constraint satisfaction problem with model checker // Proceedings of the 29th DAAAM International Symposium 2018
Zadar, Hrvatska, 2018. str. 1-9 (poster, međunarodna recenzija, cjeloviti rad (in extenso), znanstveni)
Blašković, B., Škopljanac-Mačina, F., Knežević, P. & Palić , N. (2018) Modeling constraint satisfaction problem with model checker. U: Proceedings of the 29th DAAAM International Symposium 2018.
@article{article, year = {2018}, pages = {1-9}, keywords = {constraint satisfaction problem, SMT solver, model checking, Spin/Promela, sudoku}, title = {Modeling constraint satisfaction problem with model checker}, keyword = {constraint satisfaction problem, SMT solver, model checking, Spin/Promela, sudoku}, publisherplace = {Zadar, Hrvatska} }
@article{article, year = {2018}, pages = {1-9}, keywords = {constraint satisfaction problem, SMT solver, model checking, Spin/Promela, sudoku}, title = {Modeling constraint satisfaction problem with model checker}, keyword = {constraint satisfaction problem, SMT solver, model checking, Spin/Promela, sudoku}, publisherplace = {Zadar, Hrvatska} }




Contrast
Increase Font
Decrease Font
Dyslexic Font