Patent ID: 7047139

Claim:
A computer-implemented method for satisfiability (SAT) testing, given a set of formulas describing a target system, the formulas including clauses, which include variables and which express constraints on states of the system, the set of the formulas including at least a first and a second formula, the method comprising: analyzing the first formula so as to deduce one or more conflict clauses, each such conflict clause expressing assignments of the variables that prevent a respective conflict, subject to which the first formula cannot be satisfied, while determining, for each of the conflict clauses, the clauses in the first formula that lead to the respective conflict; identifying the conflict clauses for which the clauses that lead to the respective conflict in the first formula are a subset of the clauses in the second formula; and analyzing the second formula subject to the identified conflict clauses, in order to determine whether the second formula can be satisfied.