A Boolean SAT solver uses reconfigurable hardware to solve a specific input problem. Each of the plurality of ordered variables has a corresponding one of a plurality of state machines. Each state machine has an implication circuit for its respective variable, and operates in parallel according to an identical state machine. One state machine implements the Davis-Putnam method in hardware and provides improved performance over software by virtue of the parallel checking of direct and transitive implications. Another state machine implements a novel non-chronological backtracking method that takes advantage of the parallel implication checking and avoids the need to maintain or to traverse a GRASP type implication graph in the event of backtracking. The novel non-chronological backtracking provides for setting a blocking variable as a leaf variable and for changing only the value of the leaf variable, but possibly changing both the value and identity of a backtracking variable.
展开▼
