Matti Järvisalo, Armin Biere, Marijn Heule,
"Simulating Circuit-Level Simplifications on CNF. Journal of Automated Reasoning"
, in Journal of Automated Reasoning, Serie 49, Vol. 4, Springer, Seite(n) 583-619, 2012
Simulating Circuit-Level Simplifications on CNF. Journal of Automated Reasoning
Sprache des Titels:
Boolean satisfiability (SAT) 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 (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. Motivated by this, various simplification techniques and intricate CNF encodings
for circuit-level SAT instance representations have been proposed. On the other hand, 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 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 when applying a combination of
BCE and VE.
Sprache der Kurzfassung:
Journal of Automated Reasoning
Anzahl der Seiten:
Aufsatz / Paper in sonstiger referierter Fachzeitschrift