Patent ID: 6247164
Filing Date: 2001-06-12
Classification: G06F

Abstract:
A method for deriving a satisfying variable assignment for variables of a Boolean formula, comprising:deriving a conjunctive normal form representation of the Boolean formula;generating at least one state machine in the configurable logic circuit for sequentially assigning values to the variables and performing backtrack operations based on the assigned values and determining whether a conflict occurs;generating a plurality of implication circuits corresponding to said conjunctive normal form representation in a configurable logic circuit, wherein each implication circuit is assigned to a literal that corresponds to a variable of the Boolean formula using the conjunctive normal form representation, wherein each generated implication circuit comprises:a literal value output;an assigned literal input that receives an assigned value from the state machine; andan implied literal input that receives at least one of the literal value outputs from the plurality of implication circuits;generating a plurality of local contradiction gates to provide local contradiction signals indicating whether a contradiction exists between the two literals of a particular variable, wherein the number of local contradiction gates is equal to the number of variables; anddefining the assigned values as the satisfying variable assignment for the variables of the Boolean formula, when all of the variables have been assigned values which do not result in conflict.