Alembic: An Efficient Algorithm for CNF Preprocessing

Satisfiability (SAT) solvers often benefit from a preprocessing of the formula to be decided. For formulae in conjunctive normal form (CNF), subsumed clauses may be removed or partial resolution may be applied. Preprocessing aims at simplifying the formula and at increasing the deductive power of the solver. These two objectives are sometimes competing. We present a new algorithm that combines simplification and increase of deductive power and we show its effectiveness in speeding up SAT solvers. Categories and Subject Descriptors B.6.3 [Logic design]: Design aids--Verification General Terms: Verification, Algorithms

• Type: Conference
• Year: 2007
• Where: DAC
• Authors: HyoJung Han, Fabio Somenzi
• Keywords: Aids--verification General Terms, Conjunctive Normal Form, DAC 2007, Deductive Power, Design Automation