MASSIVELY PARALLEL BOOLEAN SATISFIABILITY IMPLICATION CIRCUIT

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.