Matti Järvisalo, Armin Biere,
"Reconstructing Solutions after Blocked Clause Elimination"
: Proc. 13th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'10), Lecture Notes in Computer Science, Serie LNCS, Vol. 6175, Springer, Seite(n) 44-57, 2010
Reconstructing Solutions after Blocked Clause Elimination
Sprache des Titels:
Proc. 13th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'10), Lecture Notes in Computer Science
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.