Method and system for efficient implementation of boolean satisfiability

Abstract

Disclosed is a complete SAT solver, Chaff, which is one to two orders of magnitude faster than existing SAT solvers. Using the Davis-Putnam (DP) backtrack search strategy, Chaff employs efficient Boolean Constraint Propagation (BCP), termed two literal watching, and a low overhead decision making strategy, termed Variable State Independent Decaying Sum (VSIDS). During BCP, Chaff watches two literals not assigned to zero. The literals can be specifically ordered or randomly selected. VSIDS ranks variables, the highest-ranking literal having the highest counter value, where counter value is incremented by one for each occurrence of a literal in a clause. Periodically, the counters are divided by a constant to favor literals included in recently created conflict clauses. VSIDS can also be used to select watched literals, the literal least likely to be set (i.e., lowest VSIDS rank, or lowest VSIDS rank combined with last decision level) being selected to watch.