Encoding linear constraints into SAT

Ignasi Abío, Peter J. Stuckey

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

18 Citations (Scopus)


Linear integer constraints are one of the most important constraints in combinatorial problems since they are commonly found in many practical applications. Typically, encoding linear constraints to SAT performs poorly in problems with these constraints in comparison to constraint programming (CP) or mixed integer programming (MIP) solvers. But some problems contain a mix of combinatoric constraints and linear constraints, where encoding to SAT is highly effective. In this paper we define new approaches to encoding linear constraints into SAT, by extending encoding methods for pseudo-Boolean constraints. Experimental results show that these methods are not only better than the state-of-the-art SAT encodings, but also improve on MIP and CP solvers on appropriate problems. Combining the new encoding with lazy decomposition, which during runtime only encodes constraints that are important to the solving process that occurs, gives a robust approach to many highly combinatorial problems involving linear constraints.

Original languageEnglish
Title of host publicationPrinciples and Practice of Constraint Programming
Subtitle of host publication20th International Conference, CP 2014 Lyon, France, September 8-12, 2014 Proceedings
EditorsBarry O’Sullivan
Place of PublicationCham Switzerland
Number of pages17
ISBN (Electronic)9783319104287
ISBN (Print)9783319104270
Publication statusPublished - 2014
Externally publishedYes
EventInternational Conference on Principles and Practice of Constraint Programming 2014 - Lyon, France
Duration: 8 Sep 201412 Sep 2014
Conference number: 20th

Publication series

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


ConferenceInternational Conference on Principles and Practice of Constraint Programming 2014
Abbreviated titleCP 2014
Internet address

Cite this