SAT solvers for problems with counting
|
Supervisor |
|
|
Suitable for |
Abstract
SAT solvers nowadays prove very effective in practice for solving Constraint Satisfaction Problems (CSPs), even though encoding constraints as Boolean formulas in CNF can result in a very large problem representation. A very frequent type of constraint is counting the number of things that satisfy some property. In [1] it has been shown that throughout the search for a solution of the SAT problem we can ignore the auxiliary variables introduced for counting - however, it has only been shown for counting up to one. The scope of this thesis is to extend these results to arbitrary n and show their impact in practice by modifying a state-of-the-art SAT solver accordingly.[1] Towards Robust CNF Encodings of Cardinality Constraints - J. Marques-Silva and Ines Lynce, Proceedings of Principles and Practice of Constraint Programming, 2007, CP'07