DocumentCode
465349
Title
Alembic: An Efficient Algorithm for CNF Preprocessing
Author
Han, Hyojung ; Somenzi, Fabio
Author_Institution
Univ. of Colorado, Boulder
fYear
2007
fDate
4-8 June 2007
Firstpage
582
Lastpage
587
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;
fLanguage
English
Publisher
ieee
Conference_Titel
Design Automation Conference, 2007. DAC '07. 44th ACM/IEEE
Conference_Location
San Diego, CA
ISSN
0738-100X
Print_ISBN
978-1-59593-627-1
Type
conf
Filename
4261250
Link To Document