Encoding linear constraints with implication chains to CNF

Ignasi Abío; Valentin Mayer-Eichberger; Peter J. Stuckey

doi:10.1007/978-3-319-23219-5_1

Encoding linear constraints with implication chains to CNF

Ignasi Abío, Valentin Mayer-Eichberger, Peter J. Stuckey

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

6 Citations (Scopus)

Abstract

Linear constraints are the most common constraints occurring in combinatorial problems. For some problems which combine linear constraints with highly combinatorial constraints, the best solving method is translation to SAT. Translation of a single linear constraint to SAT is a well studied problem, particularly for cardinality and pseudo- Boolean constraints. In this paper we describe how we can improve encodings of linear constraints by taking into account implication chains in the problem. The resulting encodings are smaller and can propagate more strongly than separate encodings. We illustrate benchmarks where the encoding improves performance.

Original language	English
Title of host publication	Principles and Practice of Constraint Programming
Subtitle of host publication	21st International Conference, CP 2015 Cork, Ireland, August 31 – September 4, 2015 Proceedings
Editors	Gilles Pesant
Place of Publication	Cham Switzerland
Publisher	Springer
Pages	3-11
Number of pages	9
ISBN (Electronic)	9783319232195
ISBN (Print)	9783319232188
DOIs	https://doi.org/10.1007/978-3-319-23219-5_1
Publication status	Published - 2015
Externally published	Yes
Event	International Conference on Principles and Practice of Constraint Programming 2015 - Cork, Ireland Duration: 31 Aug 2015 → 4 Sep 2015 Conference number: 21st https://web.archive.org/web/20150810094235/http://booleconferences.ucc.ie/cp2015

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	9255
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	International Conference on Principles and Practice of Constraint Programming 2015
Abbreviated title	CP 2015
Country/Territory	Ireland
City	Cork
Period	31/08/15 → 4/09/15
Internet address	https://web.archive.org/web/20150810094235/http://booleconferences.ucc.ie/cp2015

Access to Document

10.1007/978-3-319-23219-5_1

Cite this

Abío, I., Mayer-Eichberger, V., & Stuckey, P. J. (2015). Encoding linear constraints with implication chains to CNF. In G. Pesant (Ed.), Principles and Practice of Constraint Programming : 21st International Conference, CP 2015 Cork, Ireland, August 31 – September 4, 2015 Proceedings (pp. 3-11). (Lecture Notes in Computer Science ; Vol. 9255). Springer. https://doi.org/10.1007/978-3-319-23219-5_1

Abío, Ignasi ; Mayer-Eichberger, Valentin ; Stuckey, Peter J. / Encoding linear constraints with implication chains to CNF. Principles and Practice of Constraint Programming : 21st International Conference, CP 2015 Cork, Ireland, August 31 – September 4, 2015 Proceedings. editor / Gilles Pesant. Cham Switzerland : Springer, 2015. pp. 3-11 (Lecture Notes in Computer Science ).

@inproceedings{a1e835aed8b44dffae4afc7bd47ef470,

title = "Encoding linear constraints with implication chains to CNF",

abstract = "Linear constraints are the most common constraints occurring in combinatorial problems. For some problems which combine linear constraints with highly combinatorial constraints, the best solving method is translation to SAT. Translation of a single linear constraint to SAT is a well studied problem, particularly for cardinality and pseudo- Boolean constraints. In this paper we describe how we can improve encodings of linear constraints by taking into account implication chains in the problem. The resulting encodings are smaller and can propagate more strongly than separate encodings. We illustrate benchmarks where the encoding improves performance.",

author = "Ignasi Ab{\'i}o and Valentin Mayer-Eichberger and Stuckey, {Peter J.}",

year = "2015",

doi = "10.1007/978-3-319-23219-5_1",

language = "English",

isbn = "9783319232188",

series = "Lecture Notes in Computer Science ",

publisher = "Springer",

pages = "3--11",

editor = "Gilles Pesant",

booktitle = "Principles and Practice of Constraint Programming",

note = "International Conference on Principles and Practice of Constraint Programming 2015, CP 2015 ; Conference date: 31-08-2015 Through 04-09-2015",

url = "https://web.archive.org/web/20150810094235/http://booleconferences.ucc.ie/cp2015",

}

Abío, I, Mayer-Eichberger, V & Stuckey, PJ 2015, Encoding linear constraints with implication chains to CNF. in G Pesant (ed.), Principles and Practice of Constraint Programming : 21st International Conference, CP 2015 Cork, Ireland, August 31 – September 4, 2015 Proceedings. Lecture Notes in Computer Science , vol. 9255, Springer, Cham Switzerland, pp. 3-11, International Conference on Principles and Practice of Constraint Programming 2015, Cork, Ireland, 31/08/15. https://doi.org/10.1007/978-3-319-23219-5_1

Encoding linear constraints with implication chains to CNF. / Abío, Ignasi; Mayer-Eichberger, Valentin; Stuckey, Peter J.

Principles and Practice of Constraint Programming : 21st International Conference, CP 2015 Cork, Ireland, August 31 – September 4, 2015 Proceedings. ed. / Gilles Pesant. Cham Switzerland : Springer, 2015. p. 3-11 (Lecture Notes in Computer Science ; Vol. 9255).

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

TY - GEN

T1 - Encoding linear constraints with implication chains to CNF

AU - Abío, Ignasi

AU - Mayer-Eichberger, Valentin

AU - Stuckey, Peter J.

N1 - Conference code: 21st

PY - 2015

Y1 - 2015

N2 - Linear constraints are the most common constraints occurring in combinatorial problems. For some problems which combine linear constraints with highly combinatorial constraints, the best solving method is translation to SAT. Translation of a single linear constraint to SAT is a well studied problem, particularly for cardinality and pseudo- Boolean constraints. In this paper we describe how we can improve encodings of linear constraints by taking into account implication chains in the problem. The resulting encodings are smaller and can propagate more strongly than separate encodings. We illustrate benchmarks where the encoding improves performance.

AB - Linear constraints are the most common constraints occurring in combinatorial problems. For some problems which combine linear constraints with highly combinatorial constraints, the best solving method is translation to SAT. Translation of a single linear constraint to SAT is a well studied problem, particularly for cardinality and pseudo- Boolean constraints. In this paper we describe how we can improve encodings of linear constraints by taking into account implication chains in the problem. The resulting encodings are smaller and can propagate more strongly than separate encodings. We illustrate benchmarks where the encoding improves performance.

UR - http://www.scopus.com/inward/record.url?scp=84944632054&partnerID=8YFLogxK

U2 - 10.1007/978-3-319-23219-5_1

DO - 10.1007/978-3-319-23219-5_1

M3 - Conference Paper

AN - SCOPUS:84944632054

SN - 9783319232188

T3 - Lecture Notes in Computer Science

SP - 3

EP - 11

BT - Principles and Practice of Constraint Programming

A2 - Pesant, Gilles

PB - Springer

CY - Cham Switzerland

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

Y2 - 31 August 2015 through 4 September 2015

ER -

Abío I, Mayer-Eichberger V, Stuckey PJ. Encoding linear constraints with implication chains to CNF. In Pesant G, editor, Principles and Practice of Constraint Programming : 21st International Conference, CP 2015 Cork, Ireland, August 31 – September 4, 2015 Proceedings. Cham Switzerland: Springer. 2015. p. 3-11. (Lecture Notes in Computer Science ). https://doi.org/10.1007/978-3-319-23219-5_1

Encoding linear constraints with implication chains to CNF

Abstract

Publication series

Conference

Access to Document

Other files and links

Cite this