Incrementally encoding cardinality and pseudo-boolean constraints in SAT

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.