Matti Järvisalo, Marijn Heule, Armin Biere,
"Inprocessing Rules"
: Proc. 6th Intl. Joint Conf. on Automated Reasoning (IJCAR'12), Serie Lecture Notes in Computer Science (LNCS), Vol. 7364, Springer, Seite(n) 355-370, 2012
Original Titel:
Inprocessing Rules
Sprache des Titels:
Englisch
Original Buchtitel:
Proc. 6th Intl. Joint Conf. on Automated Reasoning (IJCAR'12)
Original Kurzfassung:
Decision procedures for Boolean satisfiability (SAT), especially modern
conflict-driven clause learning (CDCL) solvers, act routinely as core solving
engines in various real-world applications. Preprocessing, i.e., applying formula
rewriting/simplification rules to the input formula before the actual search for
satisfiability, has become an essential part of the SAT solving tool chain. Further,
some of the strongest SAT solvers today add more reasoning to search by interleaving
formula simplification and CDCL search. Such inprocessing SAT solvers
witness the fact that implementing additional deduction rules in CDCL solvers
leverages the efficiency of state-of-the-art SAT solving further. In this paper we
establish formal underpinnings of inprocessing SAT solving via an abstract inprocessing
framework that covers a wide range of modern SAT solving techniques.