Patent ID: 7356519

Claim:
A method of solving satisfiability problems, the method comprising: (a) organizing a plurality of clauses in a satisfiability problem as a chronologically ordered structure comprising a top and a bottom, wherein newly deduced conflict clauses are added to the top of the structure, and maintaining individual activity counters for variables in the plurality of clauses, wherein the individual activity counters are incremented only based upon clauses that are involved in a conflict where a clause C is involved in the conflict if during Boolean Constraint Propagation, the clause C becomes a unit and a deduced assignment is made to satisfy C which leads to the conflict; (b) selecting a branching variable from a plurality of unassigned variables in the satisfiability problem, in which the branching variable is selected by selecting a clause and an active variable from the clause based upon the activity counter, wherein the branching variable is selected based upon a high activity counter; (c) assigning value 0 or 1 to the selected branching variable; (d) marking literals set to 0; (e) invoking Boolean Constraint Propagation when the structure comprises one or more unit clauses; (f) repeating (b)-(e) when the structure only comprises one or more non-unit clauses; and (g) returning a solution if a solution is found.