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

Peter Nightingale, Patrick Spracklen, Ian James Miguel

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

11 Citations (Scopus)

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.
Original languageEnglish
Title of host publicationPrinciples and Practice of Constraint Programming
Subtitle of host publication21st International Conference, CP 2015, Cork, Ireland, August 31 -- September 4, 2015, Proceedings
EditorsGilles Pesant
PublisherSpringer
Pages330-340
Number of pages11
Volume9255
ISBN (Electronic)978-3-319-23219-5
ISBN (Print)978-3-319-23218-8
DOIs
Publication statusPublished - Oct 2015
Event21st International Conference on Principles and Practice of Constraint Programming (CP 2015) - Western Gateway Building, University College Cork, Cork, Ireland
Duration: 31 Aug 20154 Sept 2015

Publication series

NameLecture Notes in Computer Science
PublisherSpringer International Publishing AG
Volume9255
ISSN (Print)0302-9743

Conference

Conference21st International Conference on Principles and Practice of Constraint Programming (CP 2015)
Country/TerritoryIreland
CityCork
Period31/08/154/09/15

Fingerprint

Dive into the research topics of 'Automatically improving SAT encoding of constraint problems through common subexpression elimination in Savile Row'. Together they form a unique fingerprint.

Cite this