ECAI-2002 Conference Paper

[full paper]

Computing Minimal Conflicts for Rich Constraint Languages

Jakob Mauss, Mugur Tatar

We address here the following question: Given an inconsistent theory, find a minimal subset of it responsible for the inconsistency. Such conflicts are essential for problem solvers that make use of conflict-driven search, for interactive applications where explanations are required, or as supporting tools for consistency maintenance in knowledge-bases. Conflict computation in AI applications was usually associated with dependency recording as performed by TMSs. This techniques, however, have a rather limited applicability for languages that go beyond the expressiveness power of propositional logic. For more powerful languages and solvers constraint suspension appeared, until now, to be the only available alternative for the computation of minimal conflicts. We present here an algorithm for computing minimal conflicts that can be used with powerful constraint languages, e.g. possibly including finite and non-finite variable domains, algebraic and FD constraints, etc. The conflicts are extracted post mortem from the proof (a tree with inferences of the form A & B => C) that lead to the derivation of the inconsistency by an informed search that computes and generalizes conflicting relations. The algorithm is based on a simple but powerful principle that allows to recursively decompose the minimization problem into smaller sub-problems. This principle can also lay the foundation for efficient constraint suspension algorithms that can be used in case no intermediary results are cached during the constraint solving, i.e. in case no proof structures are available.

Keywords: Constraint Programming, Model-Based Reasoning, Automated Reasoning

Citation: Jakob Mauss, Mugur Tatar: Computing Minimal Conflicts for Rich Constraint Languages. In F. van Harmelen (ed.): ECAI2002, Proceedings of the 15th European Conference on Artificial Intelligence, IOS Press, Amsterdam, 2002, pp.151-155.