Divide and Conquer: Towards Faster Pseudo-Boolean Solving
Divide and Conquer: Towards Faster Pseudo-Boolean Solving
Jan Elffers, Jakob Nordström
Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence
Main track. Pages 1291-1299.
https://doi.org/10.24963/ijcai.2018/180
The last 20 years have seen dramatic improvements in the performance
of algorithms for Boolean satisfiability---so-called SAT solvers---and
today conflict-driven clause learning (CDCL) solvers are routinely
used in a wide range of application areas. One serious short-coming
of CDCL, however, is that the underlying method of reasoning is quite
weak. A tantalizing solution is to instead use stronger
pseudo-Boolean (PB) reasoning, but so far the promise of exponential
gains in performance has failed to materialize---the increased
theoretical strength seems hard to harness algorithmically, and in
many applications CDCL-based methods are still superior. We propose a
modified approach to pseudo-Boolean solving based on division instead
of the saturation rule used in [Chai and Kuehlmann '05] and other PB
solvers. In addition to resulting in a stronger conflict analysis,
this also improves performance by keeping integer coefficient sizes
down, and yields a very competitive solver as shown by the results in
the Pseudo-Boolean Competitions 2015 and 2016.
Keywords:
Constraints and SAT: Constraints and SAT
Constraints and SAT: SAT
Constraints and SAT: SAT: Evaluation and Analysis
Constraints and SAT: SAT: Solvers and Tools