Truth Assignments as Conditional Autarkies

Benjamin Kiesl; Marijn Heule; Armin Biere

Truth Assignments as Conditional Autarkies

Benjamin Kiesl, Marijn Heule, Armin Biere

Institute of Formal Models and Verification

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

Abstract

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.

Original language	English
Title of host publication	Automated Technology for Verification and Analysis - 17th International Symposium, ATVA 2019, Taipei, Taiwan, October 28-31, 2019, Proceedings
Editors	Yu-Fang Chen and Chih-Hong Cheng and Javier Esparza
Publisher	Springer
Pages	48-64
Number of pages	17
Volume	11781
Publication status	Published - 2019

Publication series

Name	Lecture Notes in Computer Science (LNCS)

Fields of science

102 Computer Sciences
102001 Artificial intelligence
102011 Formal languages
102022 Software development
102031 Theoretical computer science
603109 Logic
202006 Computer hardware

Logical Methods in Computer Science - Periode II (DK W-1255)
Biere, A. (PI) & Seidl, M. (PI)
01.03.2018 → 28.02.2023
Project: Funded research › FWF - Austrian Science Fund

Cite this

Kiesl, B., Heule, M., & Biere, A. (2019). Truth Assignments as Conditional Autarkies. In Yu-Fang Chen and Chih-Hong Cheng and Javier Esparza (Ed.), Automated Technology for Verification and Analysis - 17th International Symposium, ATVA 2019, Taipei, Taiwan, October 28-31, 2019, Proceedings (Vol. 11781, pp. 48-64). (Lecture Notes in Computer Science (LNCS)). Springer.

Kiesl, Benjamin ; Heule, Marijn ; Biere, Armin. / Truth Assignments as Conditional Autarkies. Automated Technology for Verification and Analysis - 17th International Symposium, ATVA 2019, Taipei, Taiwan, October 28-31, 2019, Proceedings. editor / Yu-Fang Chen and Chih-Hong Cheng and Javier Esparza. Vol. 11781 Springer, 2019. pp. 48-64 (Lecture Notes in Computer Science (LNCS)).

@inproceedings{7b29b206962f4f04a45c4400f2b25402,

title = "Truth Assignments as Conditional Autarkies",

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

author = "Benjamin Kiesl and Marijn Heule and Armin Biere",

year = "2019",

language = "English",

volume = "11781",

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

publisher = "Springer",

pages = "48--64",

editor = "{Yu-Fang Chen and Chih-Hong Cheng and Javier Esparza}",

booktitle = "Automated Technology for Verification and Analysis - 17th International Symposium, ATVA 2019, Taipei, Taiwan, October 28-31, 2019, Proceedings",

}

Truth Assignments as Conditional Autarkies. / Kiesl, Benjamin; Heule, Marijn; Biere, Armin.
Automated Technology for Verification and Analysis - 17th International Symposium, ATVA 2019, Taipei, Taiwan, October 28-31, 2019, Proceedings. ed. / Yu-Fang Chen and Chih-Hong Cheng and Javier Esparza. Vol. 11781 Springer, 2019. p. 48-64 (Lecture Notes in Computer Science (LNCS)).

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

TY - GEN

T1 - Truth Assignments as Conditional Autarkies

AU - Kiesl, Benjamin

AU - Heule, Marijn

AU - Biere, Armin

PY - 2019

Y1 - 2019

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

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

M3 - Conference proceedings

VL - 11781

T3 - Lecture Notes in Computer Science (LNCS)

SP - 48

EP - 64

BT - Automated Technology for Verification and Analysis - 17th International Symposium, ATVA 2019, Taipei, Taiwan, October 28-31, 2019, Proceedings

A2 - Yu-Fang Chen and Chih-Hong Cheng and Javier Esparza, null

PB - Springer

ER -

Truth Assignments as Conditional Autarkies

Abstract

Publication series

Fields of science

Projects

Logical Methods in Computer Science - Periode II (DK W-1255)

Cite this