zbMATH — the first resource for mathematics

Reconstructing solutions after blocked clause elimination. (English) Zbl 1306.68159
Strichman, Ofer (ed.) et al., Theory and applications of satisfiability testing – SAT 2010. 13th international conference, SAT 2010, Edinburgh, UK, July 11–14, 2010. Proceedings. Berlin: Springer (ISBN 978-3-642-14185-0/pbk). Lecture Notes in Computer Science 6175, 340-345 (2010).
Summary: Preprocessing has proven important in enabling efficient Boolean satisfiability (SAT) solving. For many real application scenarios of SAT it is important to be able to extract a full satisfying assignment for original SAT instances from a satisfying assignment for the instances after preprocessing. We show how such full solutions can be efficiently reconstructed from solutions to the conjunctive normal form (CNF) formulas resulting from applying a combination of various CNF preprocessing techniques implemented in the PrecoSAT solver – especially, blocked clause elimination combined with SatElite-style variable elimination and equivalence reasoning.
For the entire collection see [Zbl 1196.68013].

68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
Full Text: DOI