Constraint Satisfaction Problems: CSP Solvers or SAT solvers?

Graduate Thesis uoadl:1668042 695 Read counter

Unit:
Department of Informatics and Telecommunications
Πληροφορική
Deposit date:
2017-06-15
Year:
2017
Author:
ALEXIS KONSTANTINOS
Supervisors info:
Παναγιώτης Σταματόπουλος, Επίκουρος Καθηγητής, Τμήμα Πληροφορικής και Τηλεπικοινωνιών, Εθνικό και Καποδιστριακό Πανεπιστήμιο Αθηνών
Original Title:
Προβλήματα Ικανοποίησης Περιορισμών: Επιλυτές Περιορισμών ή Επιλυτές Ικανοποιησιμότητας;
Languages:
Greek
Translated title:
Constraint Satisfaction Problems: CSP Solvers or SAT solvers?
Summary:
The purpose of this paper is to investigate Constraint Satisfaction Problems (CSP). In particular, the subject of the study is the parallel comparison of two different approaches to CSP solving. The first approach is to solve the problem directly by a dedicated CSP Solver. The second one investigates encodings of the initial problem into an equivalent Boolean Satisfiability Problem (SAT) and then solves it through a general SAT Solver.
In order to accomplish this comparison, three classic CSP were selected (N queens, Map Coloring, Car Sequencing) and examined by both approaches. These problems were modeled as CSP and SAT instances and then solved by the corresponding CSP and SAT Solvers. For the CSP case, the models were created using the MiniZinc software and their solution was searched by internally calling the Gecode Solver. Respectively, in the case of SAT, the problems were implemented in C++ environment and solved by the MiniSat package.
From the results obtained, the pure CSP approach seems to be superior to the alternative SAT approach. Although this conclusion is not universal, however, it is noted that the special advantage of the CSP strategy is its consistency and reliability in contrast of the corresponding SAT.
Main subject category:
Artificial Intelligence
Keywords:
constraint satisfaction problems, SAT instances, SAT encodings, CSP solvers, SAT solvers
Index:
Yes
Number of index pages:
2
Contains images:
No
Number of references:
6
Number of pages:
54
Ptyxiaki Konstantinos Alexis.pdf (831 KB) Open in new window