Armin Biere, Benjamin Kiesl, Matti Järvisalo,
"Preprocessing in SAT Solving"
, in Armin Biere, Marijn Heule, Hans van Maaren, Toby Walsh: Handbook of Satisfiability, Serie Frontiers in Artificial Intelligence and Applications, Vol. Vol. 336, IOS Press, Seite(n) 391 - 435, 2021, ISBN: 978-1-64368-160-3
Preprocessing in SAT Solving
Sprache des Titels:
Handbook of Satisfiability
Preprocessing has become a key component of the Boolean satisfiability (SAT) solving workflow. In practice, preprocessing is situated between the encoding phase and the solving phase, with the aim of decreasing the total solving time by applying efficient simplification techniques on SAT instances to speed up the search subsequently performed by a SAT solver. In this chapter, we overview key preprocessing techniques proposed in the literature. While the main focus is on techniques applicable to formulas in conjunctive normal form (CNF), we also selectively cover main ideas for preprocessing structural and higher-level SAT instance representations.
Sprache der Kurzfassung:
Frontiers in Artificial Intelligence and Applications