The famous archetypicalNP-complete Problem of Boolean satisfiability (SAT) and its PSPACEcomplete
generalization of quantified Boolean satisfiability (QSAT) have become central declarative
programming paradigms through which real-world instances of various computationally hard
problems can be efficiently solved. This success has been achieved through several breakthroughs
in practical implementations of decision procedures for SAT and QSAT, that is, in SAT and QSAT
solvers. Here, simplification techniques for conjunctive normal form (CNF) for SAT and for
prenex conjunctive normal form (PCNF) for QSAT?the standard input formats of SAT and QSAT
solvers?have recently proven very effective in increasing solver efficiency.
Clause elimination procedures form a family of (P)CNF formula simplification techniques which
remove clauses that have specific (in practice polynomial-time) redundancy properties while maintaining
the satisfiability status of the formulas. Extending known procedures such as tautology,
subsumption, and blocked clause elimination, we introduce novel elimination procedures based
on asymmetric variants of these techniques, and also develop a novel family of so-called covered
clause elimination procedures, as well as natural liftings of the CNF-level procedures to PCNF. Furthermore, for the variants not preserving logical equivalence under clause elimination, we show how to reconstruct solutions to original CNFs from satisfying assignments to simplified CNFs, which is important
for practical applications for the procedures. Complementing the more theoretical analysis, we
present results on an empirical evaluation on the practical importance of the clause elimination procedures in terms of the effect on solver runtimes on standard real-world application benchmarks. It
turns out that the importance of applying the clause elimination procedures developed in this work
is empirically emphasized in the context of state-of-the-art QSAT solving.
Sprache der Kurzfassung:
Englisch
Journal:
Journal of Artificial Intelligence Research (JAIR)