Patent ID: 7992113
Filing Date: 2011-08-02
Classification: G06F

Abstract:
1. A method, implemented on a computer system having one or more processors, of producing a satisfiability report on a design problem comprising: (a) converting a design problem, into a conjunctive normal form formula to be solved; (b) generating a reference point from the design problem, the reference point comprising an assignment of values to all variables in the conjunctive normal form formula; (c) deriving, with one or more of the processors, a first set of clauses from the formula, the first set comprising the clauses that are falsified by the reference point; (d) forming, with one or more of the processors, a second set of clauses from the first set, the second set of clauses initially equal to a non-empty subset of clauses falsified by the reference point; (e) making a decision assignment satisfying at least one clause in the second set; (f) performing, with one or more of the processors, Boolean Constraint Propagation by making a plurality of implied assignments, each implied assignment satisfying a yet unsatisfied clause having only one unassigned literal; (g) recomputing, with one or more of the processors, the second set of clauses after each decision assignment and each implied assignment, the recomputing comprising (h) generating, with one or more of the processors, a new reference point when the second set of clauses is empty, the new reference point being obtained from the previous reference point by flipping all the assignments of the previous reference point that disagree with new assignments; and (i) reporting satisfiability of the formula if the new reference point satisfies all the clauses.