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 Lecture Notes in Computer Science (LNCS), Vol. 6175, Springer, Seite(n) 44-57, 2010
Original Titel:
Reconstructing Solutions after Blocked Clause Elimination
Sprache des Titels:
Englisch
Original Buchtitel:
Proc. 13th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'10), Lecture Notes in Computer Science
Original Kurzfassung:
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.
Forschungs-