Automatic generation of implied constraints

John Charnley, Simon Colton, Ian Miguel

Research output: Chapter in Book/Report/Conference proceedingChapter (Book)Researchpeer-review

41 Citations (Scopus)


A well-known difficulty with solving Constraint Satisfaction Problems (CSPs) is that, while one formulation of a CSP may enable a solver to solve it quickly, a different formulation may take prohibitively long to solve. We demonstrate a system for automatically reformulating CSP solver models by combining the capabilities of machine learning and automated theorem proving with CSP systems. Our system is given a basic CSP formulation and outputs a set of reformulations, each of which includes additional constraints. The additional constraints are generated through a machine learning process and are proven to follow from the basic formulation by a theorem prover. Experimenting with benchmark problem classes from finite algebras, we show how the time invested in reformulation is often recovered many times over when searching for solutions to more difficult problems from the problem class.

Original languageEnglish
Title of host publicationECAI 2006
Subtitle of host publication17th European Conference on Artificial Intelligence August 29 - September 1, 2006, Riva del Garda, Italy
EditorsGerhard Brewka, Silvia Coradeschi, Anna Perini, Paolo Traverso
Number of pages5
Publication statusPublished - 1 Dec 2006
Externally publishedYes

Publication series

NameFrontiers in Artificial Intelligence and Applications
ISSN (Print)0922-6389

Cite this