Boolean equi-propagation for optimized SAT encoding

Amit Metodi; Michael Codish; Vitaly Lagoon; Peter J. Stuckey

doi:10.1007/978-3-642-23786-7_47

Boolean equi-propagation for optimized SAT encoding

Amit Metodi
, Michael Codish
, Vitaly Lagoon
, Peter J. Stuckey

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

16 Citations (Scopus)

Abstract

We present an approach to propagation based SAT encoding, Boolean equi-propagation, where constraints are modelled as Boolean functions which propagate information about equalities between Boolean literals. This information is then applied as a form of partial evaluation to simplify constraints prior to their encoding as CNF formulae. We demonstrate for a variety of benchmarks that our approach leads to a considerable reduction in the size of CNF encodings and subsequent speed-ups in SAT solving times.

Original language	English
Title of host publication	Principles and Practice of Constraint Programming, CP 2011 - 17th International Conference, Proceedings
Publisher	Springer
Pages	621-636
Number of pages	16
ISBN (Print)	9783642237850
DOIs	https://doi.org/10.1007/978-3-642-23786-7_47
Publication status	Published - 26 Sept 2011
Externally published	Yes
Event	International Conference on Principles and Practice of Constraint Programming 2011 - Perugia, Italy Duration: 12 Sept 2011 → 16 Sept 2011 Conference number: 17th http://www.dmi.unipg.it/cp2011/

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	6876 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	International Conference on Principles and Practice of Constraint Programming 2011
Abbreviated title	CP 2011
Country/Territory	Italy
City	Perugia
Period	12/09/11 → 16/09/11
Internet address	http://www.dmi.unipg.it/cp2011/

Access to Document

10.1007/978-3-642-23786-7_47

Cite this

Metodi, A., Codish, M., Lagoon, V., & Stuckey, P. J. (2011). Boolean equi-propagation for optimized SAT encoding. In Principles and Practice of Constraint Programming, CP 2011 - 17th International Conference, Proceedings (pp. 621-636). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 6876 LNCS). Springer. https://doi.org/10.1007/978-3-642-23786-7_47

Metodi, Amit ; Codish, Michael ; Lagoon, Vitaly et al. / Boolean equi-propagation for optimized SAT encoding. Principles and Practice of Constraint Programming, CP 2011 - 17th International Conference, Proceedings. Springer, 2011. pp. 621-636 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{7a2c3c39d0e946e18062c2c999a9d843,

title = "Boolean equi-propagation for optimized SAT encoding",

abstract = "We present an approach to propagation based SAT encoding, Boolean equi-propagation, where constraints are modelled as Boolean functions which propagate information about equalities between Boolean literals. This information is then applied as a form of partial evaluation to simplify constraints prior to their encoding as CNF formulae. We demonstrate for a variety of benchmarks that our approach leads to a considerable reduction in the size of CNF encodings and subsequent speed-ups in SAT solving times.",

author = "Amit Metodi and Michael Codish and Vitaly Lagoon and Stuckey, \{Peter J.\}",

year = "2011",

month = sep,

day = "26",

doi = "10.1007/978-3-642-23786-7\_47",

language = "English",

isbn = "9783642237850",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer",

pages = "621--636",

booktitle = "Principles and Practice of Constraint Programming, CP 2011 - 17th International Conference, Proceedings",

address = "Switzerland",

note = "International Conference on Principles and Practice of Constraint Programming 2011, CP 2011 ; Conference date: 12-09-2011 Through 16-09-2011",

url = "http://www.dmi.unipg.it/cp2011/",

}

Metodi, A, Codish, M, Lagoon, V & Stuckey, PJ 2011, Boolean equi-propagation for optimized SAT encoding. in Principles and Practice of Constraint Programming, CP 2011 - 17th International Conference, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 6876 LNCS, Springer, pp. 621-636, International Conference on Principles and Practice of Constraint Programming 2011, Perugia, Italy, 12/09/11. https://doi.org/10.1007/978-3-642-23786-7_47

Boolean equi-propagation for optimized SAT encoding. / Metodi, Amit; Codish, Michael; Lagoon, Vitaly et al.
Principles and Practice of Constraint Programming, CP 2011 - 17th International Conference, Proceedings. Springer, 2011. p. 621-636 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 6876 LNCS).

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

TY - GEN

T1 - Boolean equi-propagation for optimized SAT encoding

AU - Metodi, Amit

AU - Codish, Michael

AU - Lagoon, Vitaly

AU - Stuckey, Peter J.

N1 - Conference code: 17th

PY - 2011/9/26

Y1 - 2011/9/26

N2 - We present an approach to propagation based SAT encoding, Boolean equi-propagation, where constraints are modelled as Boolean functions which propagate information about equalities between Boolean literals. This information is then applied as a form of partial evaluation to simplify constraints prior to their encoding as CNF formulae. We demonstrate for a variety of benchmarks that our approach leads to a considerable reduction in the size of CNF encodings and subsequent speed-ups in SAT solving times.

AB - We present an approach to propagation based SAT encoding, Boolean equi-propagation, where constraints are modelled as Boolean functions which propagate information about equalities between Boolean literals. This information is then applied as a form of partial evaluation to simplify constraints prior to their encoding as CNF formulae. We demonstrate for a variety of benchmarks that our approach leads to a considerable reduction in the size of CNF encodings and subsequent speed-ups in SAT solving times.

UR - https://www.scopus.com/pages/publications/80053014980

U2 - 10.1007/978-3-642-23786-7_47

DO - 10.1007/978-3-642-23786-7_47

M3 - Conference Paper

AN - SCOPUS:80053014980

SN - 9783642237850

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 621

EP - 636

BT - Principles and Practice of Constraint Programming, CP 2011 - 17th International Conference, Proceedings

PB - Springer

T2 - International Conference on Principles and Practice of Constraint Programming 2011

Y2 - 12 September 2011 through 16 September 2011

ER -

Metodi A, Codish M, Lagoon V, Stuckey PJ. Boolean equi-propagation for optimized SAT encoding. In Principles and Practice of Constraint Programming, CP 2011 - 17th International Conference, Proceedings. Springer. 2011. p. 621-636. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-642-23786-7_47

Boolean equi-propagation for optimized SAT encoding

Abstract

Publication series

Conference

Access to Document

Other files and links

Cite this