Exploiting short supports for improved encoding of arbitrary constraints into SAT

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

3 Citations (Scopus)

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 languageEnglish
Title of host publicationPrinciples and Practice of Constraint Programming
Subtitle of host publication22nd International Conference, CP 2016, Toulouse, France, September 5-9, 2016, Proceedings
EditorsMichael Rueher
PublisherSpringer
Pages3-12
ISBN (Electronic)9783319449531
ISBN (Print)9783319449524
DOIs
Publication statusPublished - 2016
Event22nd International Conference on Principles and Practice of Constraint Programming (CP 2016) - Toulouse Business School, Toulouse, France
Duration: 5 Sept 20169 Sept 2016

Publication series

NameLecture Notes in Computer Science
Volume9892
ISSN (Print)0302-9743

Conference

Conference22nd International Conference on Principles and Practice of Constraint Programming (CP 2016)
Country/TerritoryFrance
CityToulouse
Period5/09/169/09/16

Fingerprint

Dive into the research topics of 'Exploiting short supports for improved encoding of arbitrary constraints into SAT'. Together they form a unique fingerprint.

Cite this