Encoding linear constraints with implication chains to CNF

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

Research output: Chapter in Book/Report/Conference proceedingConference PaperResearchpeer-review

5 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 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
Place of PublicationCham Switzerland
PublisherSpringer
Pages3-11
Number of pages9
ISBN (Electronic)9783319232195
ISBN (Print)9783319232188
DOIs
Publication statusPublished - 2015
Externally publishedYes
EventInternational Conference on Principles and Practice of Constraint Programming 2015 - Cork, Ireland
Duration: 31 Aug 20154 Sep 2015
Conference number: 21st
https://web.archive.org/web/20150810094235/http://booleconferences.ucc.ie/cp2015

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume9255
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

ConferenceInternational Conference on Principles and Practice of Constraint Programming 2015
Abbreviated titleCP 2015
CountryIreland
CityCork
Period31/08/154/09/15
Internet address

Cite this