Sciweavers

SAT
2010
Springer

Reconstructing Solutions after Blocked Clause Elimination

14 years 3 months ago
Reconstructing Solutions after Blocked Clause Elimination
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.
Matti Järvisalo, Armin Biere
Added 16 Aug 2010
Updated 16 Aug 2010
Type Conference
Year 2010
Where SAT
Authors Matti Järvisalo, Armin Biere
Comments (0)