Patent ID: 7565634

Claim:
Apparatus for solving Boolean satisfiability instances having N variables and M clauses, the apparatus comprising: a plurality of clause evaluation circuits (CECs); a plurality of variable evaluation circuits (VECs); wherein said N variables are partitioned into P≧2 partial variable sets, such that each of said N variables belongs to exactly one of said partial variable sets; wherein said M clauses are partitioned into Q≧2 partial clause sets, such that each of said M clauses belongs to exactly one of said partial clause sets; wherein each of said CECs has as inputs the variables of one of said partial variable sets, and provides CEC results for the clauses of one of said partial clause sets; wherein each of said VECs has as inputs said CEC results for the clauses of one of said partial clause sets, and provides VEC outputs for the variables of one of said partial variable sets; wherein said CEC results provide an indication, for each clause, of the number of free variables in the clause (0, 1 or more than 1), and whether or not the clause is in contradiction; wherein said VEC outputs provide identification of which variable is asserted in any clause having a CEC output of 1 free variable.