Armin Biere, M. Heule, Matti Järvisalo,
"Blocked Clause Elimination"
: Lecture Notes in Computer Science (LNCS), Vol. 6015, Springer, Seite(n) 129-144, 2010
Original Titel:
Blocked Clause Elimination
Sprache des Titels:
Englisch
Original Buchtitel:
Lecture Notes in Computer Science (LNCS)
Original Kurzfassung:
Boolean satisfiability (SAT) and its extensions are becoming a core
technology for the analysis of systems. The SAT-based approach divides into
three steps: encoding, preprocessing, and search. It is often argued that by encoding
arbitrary Boolean formulas in conjunctive normal form (CNF), structural
properties of the original problem are not reflected in the CNF. This should result
in the fact that CNF-level preprocessing and SAT solver techniques have an inherent
disadvantage compared to related techniques applicable on the level of more
structural SAT instance representations such as Boolean circuits. In this work
we study the effect of a CNF-level simplification technique called blocked clause
elimination (BCE).We show that BCE is surprisingly effective both in theory and
in practice on CNFs resulting from a standard CNF encoding for circuits: without
explicit knowledge of the underlying circuit structure, it achieves the same level
of simplification as a combination of circuit-level simplifications and previously
suggested polarity-based CNF encodings. Experimentally, we show that by applying
BCE in preprocessing, further formula reduction and faster solving can be
achieved, giving promise for applying BCE to speed up solvers.
Forschungs-