 |
Simplifying Pseudo-Boolean Constraints in Residual Number Systems
Yoav Fekete and Michael Codish
17th International Conference on Theory and Applications of
Satisfiability Testing (SAT 2014);
2014
Abstract:
We present an encoding of pseudo-Boolean constraints based on decomposition with respect to a residual number system. We illustrate that careful selection of the base for the residual number system, and when bit-blasting modulo arithmetic, results in a powerful approach when solving hard pseudo-Boolean constraints. We demonstrate, using a range of pseudo-Boolean constraint solvers, that the obtained constraints are often substantially easier to solve.Available: bibtex entry pdf
Michael Codish
The Department of Computer Science
Ben-Gurion University of the Negev
PoB 653, Beer-Sheva, 84105, Israel
mcodish@cs.bgu.ac.il