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. 336, IOS Press, Seite(n) 391 - 435, 2021, ISBN: 978-1-64368-160-3
Original Titel:
Preprocessing in SAT Solving
Sprache des Titels:
Englisch
Original Buchtitel:
Handbook of Satisfiability
Original Kurzfassung:
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:
Englisch
Veröffentlicher:
IOS Press
Serie:
Frontiers in Artificial Intelligence and Applications