How does SAT4J solve Pseudo-Boolean problems? Does it use a custom Pseudo-boolean solver or translates the constraints to CNF?

Question

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?

score 1 · Accepted Answer · answered Apr 23 '19 at 05:30

1

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.

answered Apr 23 '19 at 05:30

Daniel Le Berre

161
3

How does SAT4J solve Pseudo-Boolean problems? Does it use a custom Pseudo-boolean solver or translates the constraints to CNF?

1 Answers1