Benjamin Kiesl, Marijn Heule, Armin Biere,
"Truth Assignments as Conditional Autarkies"
, in Yu-Fang Chen and Chih-Hong Cheng and Javier Esparza: Automated Technology for Verification and Analysis - 17th International Symposium, ATVA 2019, Taipei, Taiwan, October 28-31, 2019, Proceedings, Serie Lecture Notes in Computer Science (LNCS), Vol. 11781, Springer, Seite(n) 48-64, 2019
Original Titel:
Truth Assignments as Conditional Autarkies
Sprache des Titels:
Englisch
Original Buchtitel:
Automated Technology for Verification and Analysis - 17th International Symposium, ATVA 2019, Taipei, Taiwan, October 28-31, 2019, Proceedings
Original Kurzfassung:
An autarky for a formula in propositional logic is a truth
assignment that satisfies every clause it touches, i.e., every clause for
which the autarky assigns at least one variable. In this paper, we present
how conditional autarkies, a generalization of autarkies, give rise to novel
preprocessing techniques for SAT solving. We show that conditional au-
tarkies correspond to a new type of redundant clauses, termed globally-
blocked clauses, and that the elimination of these clauses can simulate
existing circuit-simplification techniques on the CNF level.
Forschungs-