Structure Based Extended Resolution for Constraint Programming

TL;DR

This paper introduces a structure-based extended resolution method for constraint programming that leverages model structure to introduce useful literals, leading to significant speedups in solving various problems.

Contribution

It proposes a novel approach to incorporate extended resolution in CP by using structural information to identify beneficial literals, enhancing solver efficiency.

Findings

Significant speedups on multiple problem types.

Structural information guides useful literal introduction.

Extended resolution can outperform general resolution in CP.

Abstract

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.