Abstract
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. © 2010 Springer-Verlag.
Cite
CITATION STYLE
Järvisalo, M., & Biere, A. (2010). Reconstructing solutions after blocked clause elimination. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6175 LNCS, pp. 340–345). https://doi.org/10.1007/978-3-642-14186-7_30
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
