ML Anthology

Satisfiability Modulo Constraint Handling Rules (Extended Abstract)

Gregory James Duck
IJCAI 2013 pp. 2997-3001
/ijcai/2013/duck2013ijcai-satisfiability/

Abstract

Satisfiability Modulo Constraint Handling Rules (SMCHR) is the integration of the Constraint Handling Rules (CHRs) solver programming language into a Satisfiability Modulo Theories (SMT) solver framework. Constraint solvers are implemented in CHR as a set of high-level rules that specify the simplification (rewriting) and constraint propagation behavior. The traditional CHR execution algorithm manipulates a global store representing a flat conjunction of constraints. This paper introduces SMCHR: a tight integration of CHR with a modern Boolean Satisfiability (SAT) solver. Unlike CHR, SMCHR can handle (quantifier-free) formulae with an arbitrary propositional structure. SMCHR is essentially a Satisfiability Modulo Theories (SMT) solver where the theory T is implemented in CHR.

PDF IJCAI Semantic Scholar

Cite

Text

Duck. "Satisfiability Modulo Constraint Handling Rules (Extended Abstract)." International Joint Conference on Artificial Intelligence, 2013.

Markdown

[Duck. "Satisfiability Modulo Constraint Handling Rules (Extended Abstract)." International Joint Conference on Artificial Intelligence, 2013.](https://mlanthology.org/ijcai/2013/duck2013ijcai-satisfiability/)

BibTeX

@inproceedings{duck2013ijcai-satisfiability,
  title     = {{Satisfiability Modulo Constraint Handling Rules (Extended Abstract)}},
  author    = {Duck, Gregory James},
  booktitle = {International Joint Conference on Artificial Intelligence},
  year      = {2013},
  pages     = {2997-3001},
  url       = {https://mlanthology.org/ijcai/2013/duck2013ijcai-satisfiability/}
}