Matti Järvisalo, Armin Biere, Marijn Heule,
"Simulating Circuit-Level Simplifications on CNF"
, in Journal of Automated Reasoning, 2011, ISSN: 0168-7433
Original Titel:
Simulating Circuit-Level Simplifications on CNF
Sprache des Titels:
Englisch
Original Kurzfassung:
Boolean satisfiability and its extensions have become a core technology in
many application domains, such as planning and formal verification, and continue finding
various new application domains today. 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, 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. Motivated by this, various simplification techniques and intricate CNF encodings
for circuit-level SAT instance representations have been proposed. Based on the highly efficient CNF-level clause learning SAT solvers, there is also strong support
for the claim that CNF is sufficient as an input format for SAT solvers.
In this work we study the effect of CNF-level simplification techniques, focusing on
SatElite-style variable elimination (VE) and what we call blocked clause elimination (BCE).
We show that BCE is surprisingly effective both in theory and in practice on CNF formulas
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. We
also show that VE can achieve many of the same effects as BCE, but not all. On the other
hand, it turns out that VE and BCE are indeed partially orthogonal techniques.We also study the practical effects of combining BCE and VE for reducing the size of formulas and on the
running times of state-of-the-art SAT solvers. Furthermore, we address the problem of how
to construct original witnesses to satisfiable CNF formulas.
Sprache der Kurzfassung:
Englisch
Journal:
Journal of Automated Reasoning
Erscheinungsjahr:
2011
ISSN:
0168-7433
Anzahl der Seiten:
35
Reichweite:
international
Publikationstyp:
Aufsatz / Paper in sonstiger referierter Fachzeitschrift