Automatic Generation of Implied Constraints

John Charnley, Simon Colton, Ian Miguel

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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, PROCEEDINGS
EditorsG Brewka, S Coraeschi, A Perini, P Traverso
Place of PublicationAMSTERDAM
PublisherI O S PRESS
Number of pages5
ISBN (Print)978-1-58603-642-3
Publication statusPublished - 2006
Event17th European Conference on Artificial Intelligence - Riva del Garda, Italy
Duration: 29 Aug 20061 Sept 2006


Conference17th European Conference on Artificial Intelligence
CityRiva del Garda


Dive into the research topics of 'Automatic Generation of Implied Constraints'. Together they form a unique fingerprint.

Cite this