Implementing logical connectives in constraint programming

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 [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...

• Type: Journal
• Year: 2010
• Where: AI
• Authors: Christopher Jefferson, Neil C. A. Moore, Peter Nightingale, Karen E. Petrie
• Keywords: AI 2010, Artificial Intelligence, Considerable Efficiency Gains, Considerable Expressive Power, Constraint Programming