Massively parallel boolean satisfiability implication circuit
AssigneeThe Regents of the University of California, Santa Cruz
InventorsMark J. Boyd, Tracy Larrabee
Life of this patent
Estimating the term…
Abstract
The application concerns prototyped custom Programmable Logic Devices (Pills) for Boolean satisfiability (SAT) problems. This approach is based on the use of clause evaluation circuits (CECs), which indicate whether or not a single variable of the clause is asserted by the clause, and variable evaluation circuits (VECs), which identify the asserted variable of a clause having exactly one variable asserted by the clause. Scaling is provided by the use of partial CEC and VEC circuits.
Claims10
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.
Dependencies are inferred from the claim text.