Sequential machine for solving boolean satisfiability (SAT) problems in linear time

An apparatus that solves, in linear time O(M), any SAT problem instance representing a boolean formula of N variables and M clauses, being the maximum value of N constrained by hardware limitations, and said apparatus comprising:

• a. A 2×N to 2N SAT decoder unit, which, based on the value of 2×N inputs corresponding to a clause in a boolean formula F, sets each one of its 2N outputs to represent the coverage set of the clause, defined as the set of distinct variable assigments of the formula F for which the input clause evaluates to 0, where each one of the 2N outputs corresponds to one element in the coverage set, each one of such elements corresponding to a unique assignment of values to the N variables in the formula F.
• b. An R-S Flip Flop Array unit, consisting of 2N flip-flops, each one corresponding to an output of the 2×N to 2N SAT decoder unit. The R-S Flip-Flop Array unit serves as a memory for each output of the decoder unit, to remember whether such output has been previously set to 1. The unit has a RESET input, to clear or set to 0 the contents of each flip-flop, and a CLK input to set each flip-flop in the array to be equal to the value of its corresponding input.
• c. A negative-and (NAND) gate unit, whose inputs are the outputs of the R-S Flip Flop Array unit, and whose output will be set to 0 only if all its inputs are set to 1.