Exploiting short supports for improved encoding of arbitrary constraints into SAT

Özgür Akgün; Ian Philip Gent; Christopher Anthony Jefferson; Ian James Miguel; Peter William Nightingale

doi:10.1007/978-3-319-44953-1_1

Exploiting short supports for improved encoding of arbitrary constraints into SAT

Özgür Akgün, Ian Philip Gent, Christopher Anthony Jefferson, Ian James Miguel, Peter William Nightingale

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

Abstract

Encoding to SAT and applying a highly efficient modern SAT solver is an increasingly popular method of solving finite-domain constraint problems. In this paper we study encodings of arbitrary constraints where unit propagation on the encoding provides strong reasoning. Specifically, unit propagation on the encoding simulates generalised arc consistency on the original constraint.
To create compact and efficient encodings we use the concept of short support. Short support has been successfully applied to create efficient propagation algorithms for arbitrary constraints. A short support of a constraint is similar to a satisfying tuple however a short support is not required to assign every variable in scope. Some variables are left free to take any value. In some cases a short support representation is smaller than the table of satisfying tuples by an exponential factor. We present two encodings based on short supports and evaluate them on a set of benchmark problems, demonstrating a substantial improvement over the state of the art.

Original language	English
Title of host publication	Principles and Practice of Constraint Programming
Subtitle of host publication	22nd International Conference, CP 2016, Toulouse, France, September 5-9, 2016, Proceedings
Editors	Michael Rueher
Publisher	Springer
Pages	3-12
ISBN (Electronic)	9783319449531
ISBN (Print)	9783319449524
DOIs	https://doi.org/10.1007/978-3-319-44953-1_1
Publication status	Published - 2016
Event	22nd International Conference on Principles and Practice of Constraint Programming (CP 2016) - Toulouse Business School, Toulouse, France Duration: 5 Sept 2016 → 9 Sept 2016

Publication series

Name	Lecture Notes in Computer Science
Volume	9892
ISSN (Print)	0302-9743

Conference

Conference	22nd International Conference on Principles and Practice of Constraint Programming (CP 2016)
Country/Territory	France
City	Toulouse
Period	5/09/16 → 9/09/16

Access to Document

10.1007/978-3-319-44953-1_1

Akgun_2016_SAT_CP2016_AAM
© 2016, Springer. This work is made available online in accordance with the publisher’s policies. This is the author created, accepted version manuscript following peer review and may differ slightly from the final published version. The final published version of this work is available at link.springer.com / https://dx.doi.org/10.1007/978-3-319-44953-1_1
Accepted author manuscript, 192 KB

Combining Constraints and Verification: Combining Constraints and Verification
Jefferson, C. A. (PI)
EPSRC
31/07/14 → 30/07/17
Project: Standard
University Research Fellowship 2013: University Research Fellowship 2013
Jefferson, C. A. (PI)
The Royal Society
1/10/13 → 30/09/18
Project: Fellowship
Working Together in ICT: Working Together: Constraint Programming and Cloud Computing
Miguel, I. J. (PI) & Barker, A. D. (CoI)
EPSRC
1/01/13 → 30/09/16
Project: Standard

Cite this

Akgün, Ö., Gent, I. P., Jefferson, C. A., Miguel, I. J., & Nightingale, P. W. (2016). Exploiting short supports for improved encoding of arbitrary constraints into SAT. In M. Rueher (Ed.), Principles and Practice of Constraint Programming: 22nd International Conference, CP 2016, Toulouse, France, September 5-9, 2016, Proceedings (pp. 3-12). (Lecture Notes in Computer Science; Vol. 9892). Springer. https://doi.org/10.1007/978-3-319-44953-1_1

Akgün, Özgür ; Gent, Ian Philip ; Jefferson, Christopher Anthony et al. / Exploiting short supports for improved encoding of arbitrary constraints into SAT. Principles and Practice of Constraint Programming: 22nd International Conference, CP 2016, Toulouse, France, September 5-9, 2016, Proceedings. editor / Michael Rueher. Springer, 2016. pp. 3-12 (Lecture Notes in Computer Science).

@inproceedings{03feab994c4544a49e1387c269b809e0,

title = "Exploiting short supports for improved encoding of arbitrary constraints into SAT",

abstract = "Encoding to SAT and applying a highly efficient modern SAT solver is an increasingly popular method of solving finite-domain constraint problems. In this paper we study encodings of arbitrary constraints where unit propagation on the encoding provides strong reasoning. Specifically, unit propagation on the encoding simulates generalised arc consistency on the original constraint. To create compact and efficient encodings we use the concept of short support. Short support has been successfully applied to create efficient propagation algorithms for arbitrary constraints. A short support of a constraint is similar to a satisfying tuple however a short support is not required to assign every variable in scope. Some variables are left free to take any value. In some cases a short support representation is smaller than the table of satisfying tuples by an exponential factor. We present two encodings based on short supports and evaluate them on a set of benchmark problems, demonstrating a substantial improvement over the state of the art. ",

author = "{\"O}zg{\"u}r Akg{\"u}n and Gent, {Ian Philip} and Jefferson, {Christopher Anthony} and Miguel, {Ian James} and Nightingale, {Peter William}",

year = "2016",

doi = "10.1007/978-3-319-44953-1_1",

language = "English",

isbn = "9783319449524",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "3--12",

editor = "Michael Rueher",

booktitle = "Principles and Practice of Constraint Programming",

address = "Netherlands",

note = "22nd International Conference on Principles and Practice of Constraint Programming (CP 2016) ; Conference date: 05-09-2016 Through 09-09-2016",

}

Akgün, Ö , Gent, IP , Jefferson, CA , Miguel, IJ & Nightingale, PW 2016, Exploiting short supports for improved encoding of arbitrary constraints into SAT. in M Rueher (ed.), Principles and Practice of Constraint Programming: 22nd International Conference, CP 2016, Toulouse, France, September 5-9, 2016, Proceedings. Lecture Notes in Computer Science, vol. 9892, Springer, pp. 3-12, 22nd International Conference on Principles and Practice of Constraint Programming (CP 2016), Toulouse, France, 5/09/16. https://doi.org/10.1007/978-3-319-44953-1_1

Exploiting short supports for improved encoding of arbitrary constraints into SAT. / Akgün, Özgür ; Gent, Ian Philip ; Jefferson, Christopher Anthony et al.
Principles and Practice of Constraint Programming: 22nd International Conference, CP 2016, Toulouse, France, September 5-9, 2016, Proceedings. ed. / Michael Rueher. Springer, 2016. p. 3-12 (Lecture Notes in Computer Science; Vol. 9892).

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

TY - GEN

T1 - Exploiting short supports for improved encoding of arbitrary constraints into SAT

AU - Akgün, Özgür

AU - Gent, Ian Philip

AU - Jefferson, Christopher Anthony

AU - Miguel, Ian James

AU - Nightingale, Peter William

PY - 2016

Y1 - 2016

N2 - Encoding to SAT and applying a highly efficient modern SAT solver is an increasingly popular method of solving finite-domain constraint problems. In this paper we study encodings of arbitrary constraints where unit propagation on the encoding provides strong reasoning. Specifically, unit propagation on the encoding simulates generalised arc consistency on the original constraint. To create compact and efficient encodings we use the concept of short support. Short support has been successfully applied to create efficient propagation algorithms for arbitrary constraints. A short support of a constraint is similar to a satisfying tuple however a short support is not required to assign every variable in scope. Some variables are left free to take any value. In some cases a short support representation is smaller than the table of satisfying tuples by an exponential factor. We present two encodings based on short supports and evaluate them on a set of benchmark problems, demonstrating a substantial improvement over the state of the art.

AB - Encoding to SAT and applying a highly efficient modern SAT solver is an increasingly popular method of solving finite-domain constraint problems. In this paper we study encodings of arbitrary constraints where unit propagation on the encoding provides strong reasoning. Specifically, unit propagation on the encoding simulates generalised arc consistency on the original constraint. To create compact and efficient encodings we use the concept of short support. Short support has been successfully applied to create efficient propagation algorithms for arbitrary constraints. A short support of a constraint is similar to a satisfying tuple however a short support is not required to assign every variable in scope. Some variables are left free to take any value. In some cases a short support representation is smaller than the table of satisfying tuples by an exponential factor. We present two encodings based on short supports and evaluate them on a set of benchmark problems, demonstrating a substantial improvement over the state of the art.

U2 - 10.1007/978-3-319-44953-1_1

DO - 10.1007/978-3-319-44953-1_1

M3 - Conference contribution

SN - 9783319449524

T3 - Lecture Notes in Computer Science

SP - 3

EP - 12

BT - Principles and Practice of Constraint Programming

A2 - Rueher, Michael

PB - Springer

T2 - 22nd International Conference on Principles and Practice of Constraint Programming (CP 2016)

Y2 - 5 September 2016 through 9 September 2016

ER -

Akgün Ö , Gent IP , Jefferson CA , Miguel IJ, Nightingale PW. Exploiting short supports for improved encoding of arbitrary constraints into SAT. In Rueher M, editor, Principles and Practice of Constraint Programming: 22nd International Conference, CP 2016, Toulouse, France, September 5-9, 2016, Proceedings. Springer. 2016. p. 3-12. (Lecture Notes in Computer Science). Epub 2016 Aug 23. doi: 10.1007/978-3-319-44953-1_1

Exploiting short supports for improved encoding of arbitrary constraints into SAT

Abstract

Publication series

Conference

Access to Document

Fingerprint

Projects

Combining Constraints and Verification: Combining Constraints and Verification

University Research Fellowship 2013: University Research Fellowship 2013

Working Together in ICT: Working Together: Constraint Programming and Cloud Computing

Cite this