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.

68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)