Conflict directed lazy decomposition

Ignasi Abío, Peter J. Stuckey

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

14 Citations (Scopus)


Two competing approaches to handling complex constraints in satisfaction and optimization problems using SAT and LCG/SMT technology are: decompose the complex constraint into a set of clauses; or (theory) propagate the complex constraint using a standalone algorithm and explain the propagation. Each approach has its benefits. The decomposition approach is prone to an explosion in size to represent the problem, while the propagation approach may require exponentially more search since it does not have access to intermediate literals for explanation. In this paper we show how we can obtain the best of both worlds by lazily decomposing a complex constraint propagator using conflicts to direct it. If intermediate literals are not helpful for conflicts then it will act like the propagation approach, but if they are helpful it will act like the decomposition approach. Experimental results show that it is never much worse than the better of the decomposition and propagation approaches, and sometimes better than both.

Original languageEnglish
Title of host publicationPrinciples and Practice of Constraint Programming - 18th International Conference, CP 2012, Proceedings
Number of pages16
ISBN (Print)9783642335570
Publication statusPublished - 7 Nov 2012
Externally publishedYes
EventInternational Conference on Principles and Practice of Constraint Programming 2012 - Quebec, Canada
Duration: 8 Oct 201212 Oct 2012
Conference number: 18th

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume7514 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


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

Cite this