SAT encoding and CSP reduction for interconnected alldiff constraints

Frederic Lardeux, Eric Monfroy, Frederic Saubion, Broderick Crawford, Carlos Castro

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

8 Scopus citations

Abstract

Constraint satisfaction problems (CSP) or Boolean satisfiability problem (SAT) are two well known paradigm to model and solve combinatorial problems. Modeling and resolution of CSP is often strengthened by global constraints (e.g., Alldiff constraint). This paper highlights two different ways of handling specific structural information: a uniform propagation framework to handle (interleaved) Alldiff constraints with some CSP reduction rules; and a SAT encoding of these rules that preserves the reduction properties of CSP.

Original languageEnglish
Title of host publicationMICAI 2009
Subtitle of host publicationAdvances in Artificial Intelligence - 8th Mexican International Conference on Artificial Intelligence, Proceedings
Pages360-371
Number of pages12
DOIs
StatePublished - 2009
Event8th Mexican International Conference on Artificial Intelligence, MICAI 2009 - Guanajuato, Mexico
Duration: 9 Nov 200913 Nov 2009

Publication series

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

Conference

Conference8th Mexican International Conference on Artificial Intelligence, MICAI 2009
Country/TerritoryMexico
CityGuanajuato
Period9/11/0913/11/09

Fingerprint

Dive into the research topics of 'SAT encoding and CSP reduction for interconnected alldiff constraints'. Together they form a unique fingerprint.

Cite this