By the same authors

Automatically improving SAT encoding of constraint problems through common subexpression elimination in Savile Row

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Standard

Automatically improving SAT encoding of constraint problems through common subexpression elimination in Savile Row. / Nightingale, Peter; Spracklen, Patrick; Miguel, Ian James.

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

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Harvard

Nightingale, P, Spracklen, P & Miguel, IJ 2015, Automatically improving SAT encoding of constraint problems through common subexpression elimination in Savile Row. in G Pesant (ed.), Principles and Practice of Constraint Programming: 21st International Conference, CP 2015, Cork, Ireland, August 31 -- September 4, 2015, Proceedings. vol. 9255, Lecture Notes in Computer Science, Springer, Netherlands, pp. 330-340. https://doi.org/10.1007/978-3-319-23219-5_23

APA

Nightingale, P., Spracklen, P., & Miguel, I. J. (2015). Automatically improving SAT encoding of constraint problems through common subexpression elimination in Savile Row. In G. Pesant (Ed.), Principles and Practice of Constraint Programming: 21st International Conference, CP 2015, Cork, Ireland, August 31 -- September 4, 2015, Proceedings (Vol. 9255, pp. 330-340). (Lecture Notes in Computer Science). Springer. https://doi.org/10.1007/978-3-319-23219-5_23

Vancouver

Nightingale P, Spracklen P, Miguel IJ. Automatically improving SAT encoding of constraint problems through common subexpression elimination in Savile Row. In Pesant G, editor, Principles and Practice of Constraint Programming: 21st International Conference, CP 2015, Cork, Ireland, August 31 -- September 4, 2015, Proceedings. Vol. 9255. Netherlands: Springer. 2015. p. 330-340. (Lecture Notes in Computer Science). https://doi.org/10.1007/978-3-319-23219-5_23

Author

Nightingale, Peter ; Spracklen, Patrick ; Miguel, Ian James. / Automatically improving SAT encoding of constraint problems through common subexpression elimination in Savile Row. Principles and Practice of Constraint Programming: 21st International Conference, CP 2015, Cork, Ireland, August 31 -- September 4, 2015, Proceedings. editor / Gilles Pesant. Vol. 9255 Netherlands : Springer, 2015. pp. 330-340 (Lecture Notes in Computer Science).

Bibtex - Download

@inproceedings{06d793a02d6544c8a3a6dd50c1407812,
title = "Automatically improving SAT encoding of constraint problems through common subexpression elimination in Savile Row",
abstract = "The formulation of a Propositional Satisfiability (SAT) problem instance is vital to efficient solving. This has motivated research on preprocessing, and inprocessing techniques where reformulation of a SAT instance is interleaved with solving. Preprocessing and inprocessing are highly effective in extending the reach of SAT solvers, however they necessarily operate on the lowest level representation of the problem, the raw SAT clauses, where higher-level patterns are difficult and/or costly to identify. Our approach is different: rather than reformulate the SAT representation directly, we apply automated reformulations to a higher level representation (a constraint model) of the original problem. Common Subexpression Elimination (CSE) is a family of techniques to improve automatically the formulation of constraint satisfaction problems, which are often highly beneficial when using a conventional constraint solver. In this work we demonstrate that CSE has similar benefits when the reformulated constraint model is encoded to SAT and solved using a state-of-the-art SAT solver. In some cases we observe speed improvements of over 100 times.",
author = "Peter Nightingale and Patrick Spracklen and Miguel, {Ian James}",
year = "2015",
month = oct,
day = "1",
doi = "10.1007/978-3-319-23219-5_23",
language = "English",
isbn = "978-3-319-23218-8",
volume = "9255",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "330--340",
editor = "Gilles Pesant",
booktitle = "Principles and Practice of Constraint Programming",

}

RIS (suitable for import to EndNote) - Download

TY - GEN

T1 - Automatically improving SAT encoding of constraint problems through common subexpression elimination in Savile Row

AU - Nightingale, Peter

AU - Spracklen, Patrick

AU - Miguel, Ian James

PY - 2015/10/1

Y1 - 2015/10/1

N2 - The formulation of a Propositional Satisfiability (SAT) problem instance is vital to efficient solving. This has motivated research on preprocessing, and inprocessing techniques where reformulation of a SAT instance is interleaved with solving. Preprocessing and inprocessing are highly effective in extending the reach of SAT solvers, however they necessarily operate on the lowest level representation of the problem, the raw SAT clauses, where higher-level patterns are difficult and/or costly to identify. Our approach is different: rather than reformulate the SAT representation directly, we apply automated reformulations to a higher level representation (a constraint model) of the original problem. Common Subexpression Elimination (CSE) is a family of techniques to improve automatically the formulation of constraint satisfaction problems, which are often highly beneficial when using a conventional constraint solver. In this work we demonstrate that CSE has similar benefits when the reformulated constraint model is encoded to SAT and solved using a state-of-the-art SAT solver. In some cases we observe speed improvements of over 100 times.

AB - The formulation of a Propositional Satisfiability (SAT) problem instance is vital to efficient solving. This has motivated research on preprocessing, and inprocessing techniques where reformulation of a SAT instance is interleaved with solving. Preprocessing and inprocessing are highly effective in extending the reach of SAT solvers, however they necessarily operate on the lowest level representation of the problem, the raw SAT clauses, where higher-level patterns are difficult and/or costly to identify. Our approach is different: rather than reformulate the SAT representation directly, we apply automated reformulations to a higher level representation (a constraint model) of the original problem. Common Subexpression Elimination (CSE) is a family of techniques to improve automatically the formulation of constraint satisfaction problems, which are often highly beneficial when using a conventional constraint solver. In this work we demonstrate that CSE has similar benefits when the reformulated constraint model is encoded to SAT and solved using a state-of-the-art SAT solver. In some cases we observe speed improvements of over 100 times.

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

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

M3 - Conference contribution

SN - 978-3-319-23218-8

VL - 9255

T3 - Lecture Notes in Computer Science

SP - 330

EP - 340

BT - Principles and Practice of Constraint Programming

A2 - Pesant, Gilles

PB - Springer

CY - Netherlands

ER -