Automatic implication checking for CHR constraints

Tom Schrijvers, Bart Demoen, Gregory Duck, Peter Stuckey, Thom Frühwirth

Research output: Contribution to journalArticleResearchpeer-review

11 Citations (Scopus)


Constraint Handling Rules (CHRs) are a high-level rule-based programming language commonly used to define constraint solvers. We present a method for automatic implication checking between constraints of CHR solvers. Supporting implication is important for implementing extensible solvers and reification, and for building hierarchical CHR constraint solvers. Our method does not copy the entire constraint store, but performs the check in place using a trailing mechanism. The necessary code enhancements can be done by automatic program transformation based on the rules of the solver. We extend our method to work for hierarchically organized modular CHR solvers. We show the soundness of our method and its completeness for a restricted class of canonical solver as well as for specific existing non-canonical CHR solvers. We evaluate our trailing method experimentally by comparing with the copy approach: runtime is almost halved.

Original languageEnglish
Pages (from-to)93-111
Number of pages19
JournalElectronic Notes in Theoretical Computer Science
Issue number1
Publication statusPublished - 31 Jan 2006
Externally publishedYes


  • Constraint Handling Rules
  • Constraint solver hierarchy
  • Implication checking
  • Program transformation

Cite this