Incrementally encoding cardinality and pseudo-boolean constraints in SAT
J. Langerak (TU Delft - Electrical Engineering, Mathematics and Computer Science)
E. Demirović – Mentor (TU Delft - Algorithmics)
N. Yorke-Smith – Graduation committee member (TU Delft - Algorithmics)
C. Hauff – Graduation committee member (TU Delft - Web Information Systems)
More Info
expand_more
Other than for strictly personal use, it is not permitted to download, forward or distribute the text or part of it, without the consent of the author(s) and/or copyright holder(s), unless the work is under an open content license such as Creative Commons.
Abstract
Satisfiability solvers have been shown to be a powerful tool for solving constraint problems. These problems often contain pseudo-boolean and cardinality constraints. These constraints can either be encoded into SAT or handled by extending the solver with special propagators. Which method will perform better is often not known in advance. It has been shown that adding the encoding during the search can be beneficial. This thesis extends those methods by incrementally constructing the encoding during the search. This work proposes several methods that only encode the active parts of the constraint. In contrast to previous work the full encoding of the constraint is not determined beforehand but instead is determined during the search. The results show that during the search the same subset of variables is active and therefore not all variables are needed for the encoding. Furthermore, this work shows that the order of the literals in the encoding has effect on the performance. However, this mostly affects the first part of the solve process, and therefore the effect on optimization problems is limited. Finally, it shows that an incremental encoding can lead to a smaller encoding while having similar results as adding the full encoding during the search.