Structure Based Extended Resolution for Constraint Programming
  Nogood learning is a powerful approach to reducing search in Constraint
Programming (CP) solvers. The current state of the art, called Lazy Clause
Generation (LCG), uses resolution to derive nogoods expressing the reasons for
each search failure. Such nogoods can prune other parts of the search tree,
producing exponential speedups on a wide variety of problems. Nogood learning
solvers can be seen as resolution proof systems. The stronger the proof system,
the faster it can solve a CP problem. It has recently been shown that the proof
system used in LCG is at least as strong as general resolution. However,
stronger proof systems such as \emph{extended resolution} exist. Extended
resolution allows for literals expressing arbitrary logical concepts over
existing variables to be introduced and can allow exponentially smaller proofs
than general resolution. The primary problem in using extended resolution is to
figure out exactly which literals are useful to introduce. In this paper, we
show that we can use the structural information contained in a CP model in
order to introduce useful literals, and that this can translate into
significant speedups on a range of problems.
