Prime clauses for fast enumeration of satisfying assignments to boolean circuits

Finding all satisfying assignments of a propositional formula has many applications in the design of hardware and software. An approach to this problem augments a clause-recording propositional satisfiability solver with the ability to add blocking clauses, which prevent the solver from visiting the same solution more than once. One generates a blocking clause from a satisfying assignment by taking its complement. In this paper, we present an improved algorithm for finding all satisfying assignments for a generic Boolean circuit. An optimization based on lifting—which generates minimal satisfying assignments—yields prime blocking clauses. Thanks to the primality of the blocking clauses, the derived conflict clauses usually prune both satisfiable and unsatisfiable points at once. The efficiency of our new algorithm is demonstrated by our preliminary results on SAT-based unbounded model checking. Categories and Subject Descriptors B.6.3 [Logic design]: Design aids—Verificat...

• Type: Conference
• Year: 2005
• Where: DAC
• Authors: HoonSang Jin, Fabio Somenzi
• Keywords: Computer Architecture, DAC 2005, Prime Blocking Clauses, Propositional Satisfiability Solver, Satisfying Assignments