×

zbMATH — the first resource for mathematics

Translating pseudo-Boolean constraints into SAT. (English) Zbl 1116.68083
Summary: We describe and evaluate three different techniques for translating pseudo-Boolean constraints (linear constraints over Boolean variables) into clauses that can be handled by a standard SAT-solver. We show that by applying a proper mix of translation techniques, a SAT-solver can perform on a par with the best existing native pseudo-Boolean solvers. This is particularly valuable in those cases where the constraint problem of interest is naturally expressed as a SAT problem, except for a handful of constraints. Translating those constraints to get a pure clausal problem will take full advantage of the latest improvements in SAT research. A particularly interesting result of this work is the efficiency of sorting networks to express pseudo-Boolean constraints. Although tangential to this presentation, the result gives a suggestion as to how synthesis tools may be modified to produce arithmetic circuits more suitable for SAT based reasoning.

MSC:
68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
Software:
MiniSat
PDF BibTeX XML Cite