Implementing logical connectives in constraint programming

Christopher Anthony Jefferson, Neil Charles Armour Moore, Peter Nightingale, Karen E. Petrie

Research output: Contribution to journalArticlepeer-review

23 Citations (Scopus)

Abstract

Combining constraints using logical connectives such as disjunction is ubiquitous in constraint programming, because it adds considerable expressive power to a constraint language. We explore the solver architecture needed to propagate such combinations of constraints efficiently. In particular we describe two new features named satisfying sets and constraint trees. We also make use of movable triggers (Gent et al., 2006) [1], and with these three complementary features we are able to make considerable efficiency gains.

A key reason for the success of Boolean Satisfiability (SAT) solvers is their ability to propagate OR constraints efficiently, making use of movable triggers. We successfully generalise this approach to an OR of an arbitrary set of constraints, maintaining the crucial property that at most two constraints are active at any time, and no computation at all is done on the others. We also give an AND propagator within our framework, which may be embedded within the OR. Using this approach, we demonstrate speedups of over 10,000 times in some cases, compared to traditional constraint programming approaches. We also prove that the OR algorithm enforces generalised arc consistency (GAC) when all its child constraints have a GAC propagator, and no variables are shared between children. By extending the OR propagator, we present a propagator for ATLEASTK, which expresses that at least k of its child constraints are satisfied in any solution.

Some logical expressions (e.g. exclusive-or) cannot be compactly expressed using AND, OR and ATLEASTK. Therefore we investigate reification of constraints. We present a fast generic algorithm for reification using satisfying sets and movable triggers. (C) 2010 Published by Elsevier B.V.

Original languageEnglish
Pages (from-to)1407-1429
Number of pages23
JournalArtificial Intelligence
Volume174
Issue number16-17
DOIs
Publication statusPublished - Nov 2010

Keywords

  • Constraint programming
  • Constraint satisfaction problems
  • Propagation algorithms
  • Logical connectives
  • ARC-CONSISTENCY
  • PROPAGATION

Fingerprint

Dive into the research topics of 'Implementing logical connectives in constraint programming'. Together they form a unique fingerprint.

Cite this