Implementing logical connectives in constraint programming

Christopher Jefferson, Neil C. A. Moore, Peter Nightingale, Karen E. Petrie

    Research output: Contribution to journalArticlepeer-review

    22 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