@inproceedings{JarvisaloHB:IJCAR2012,
 author = {Matti J\"arvisalo and Marijn Heule and Armin Biere},
 title  = {Inprocessing Rules},
 editor = {Bernhard Gramlich and Dale Miller and Uli Sattler},
 booktitle = {Proceedings of the 6th International Joint Conference on 
		Automated Reasoning (IJCAR 2012)},
 publisher = {Springer},
 series = {Lecture Notes in Computer Science},
 volume = {7364},
 pages  = {355--370},
 year   = {2012},
}

Abstract:

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.