Title :
Alembic: An Efficient Algorithm for CNF Preprocessing
Author :
Han, Hyojung ; Somenzi, Fabio
Author_Institution :
Univ. of Colorado, Boulder
Abstract :
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.
Keywords :
computability; program processors; Alembic; CNF preprocessing; conjunctive normal form; deductive power; satisfiability; Algorithm design and analysis; Costs; Data preprocessing; Electronic design automation and methodology; Forward contracts; Logic design; Logic testing; Permission; Symbiosis; Timing; Algorithms; CNF; SAT; Verification; distillation; preprocessing;
Conference_Titel :
Design Automation Conference, 2007. DAC '07. 44th ACM/IEEE
Conference_Location :
San Diego, CA
Print_ISBN :
978-1-59593-627-1
