I would like to know how the Java SAT4j SAT solver API solves its pseudo-boolean problems. I've had a browse through the javadoc but im quite new to SAT problems.

From the release doc (https://www.researchgate.net/publication/220163278_The_Sat4j_library_release_22), I think a custom pseudo-boolean solver is used for everything rather than vise versa (Pseudo-boolean constraints translated to SAT CNF).

Anyone have concrete knowledge?

1 Answers

Daniel Le Berre On

Sat4j does not translate cardinality or pseudo-Boolean constraints in CNF, it handles them natively, using either the resolution proof system or some kind of "cutting planes" proof system called generalized resolution.