Reconstructing Solutions after Blocked Clause Elimination

Matti Järvisalo; Armin Biere

Reconstructing Solutions after Blocked Clause Elimination

Matti Järvisalo
, Armin Biere

Institute of Formal Models and Verification

Research output: Chapter in Book/Report/Conference proceeding › Conference proceedings › peer-review

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.

Original language	English
Title of host publication	Proc. 13th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'10), Lecture Notes in Computer Science
Publisher	Springer
Pages	44-57
Number of pages	14
Volume	6175
Publication status	Published - 2010

Publication series

Name	Lecture Notes in Computer Science (LNCS)

Fields of science

102011 Formal languages
102 Computer Sciences
101 Mathematics

JKU Focus areas

Computation in Informatics and Mathematics

Cite this

@inproceedings{f555da38c05941bdb2bf896e327ff646,

title = "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.",

author = "Matti J{\"a}rvisalo and Armin Biere",

year = "2010",

language = "English",

volume = "6175",

series = "Lecture Notes in Computer Science (LNCS)",

publisher = "Springer",

pages = "44--57",

booktitle = "Proc. 13th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'10), Lecture Notes in Computer Science",

}

Reconstructing Solutions after Blocked Clause Elimination. / Järvisalo, Matti; Biere, Armin.
Proc. 13th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'10), Lecture Notes in Computer Science. Vol. 6175 Springer, 2010. p. 44-57 (Lecture Notes in Computer Science (LNCS)).

Research output: Chapter in Book/Report/Conference proceeding › Conference proceedings › peer-review

TY - GEN

T1 - Reconstructing Solutions after Blocked Clause Elimination

AU - Järvisalo, Matti

AU - Biere, Armin

PY - 2010

Y1 - 2010

N2 - 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.

AB - 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.

M3 - Conference proceedings

VL - 6175

T3 - Lecture Notes in Computer Science (LNCS)

SP - 44

EP - 57

BT - Proc. 13th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'10), Lecture Notes in Computer Science

PB - Springer

ER -