SE547: BDDs: Logical Satisfaction [7/22]

Logical satisfaction is solved by SAT-solvers.

High-quality production SAT-solvers exist Chaff, zChaff, ... See http://www.satlive.org.

We have success stories of using zChaff to solve problems with more than one million variables and 10 million clauses.
    -- zChaff web site

A common simple solution is binary decision diagrams.

Try it... file:simplebdd.zip contains a BDD-based file:simplebdd/test/TestArith.java [source] [doc-public] [doc-private] class.