Satisfiability Modulo Constraint Handling Rules (Extended Abstract)
Proceedings of the Twenty-Third International Joint Conference on Artificial Intelligence. Pages 2997-3000.
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.
@inproceedings{ijcai2013p444,
title = {Satisfiability Modulo Constraint Handling Rules (Extended Abstract)},
author = {Duck, Gregory James},
booktitle = {Proceedings of the Twenty-Third International Joint Conference on
Artificial Intelligence, {IJCAI-13}},
publisher = {AAAI Press / International Joint Conferences on Artificial Intelligence},
editor = {Francesca Rossi},
pages = {2997--3000},
year = {2013},
month = {8},
url = {https://ijcai.org/proceedings/2013/444},
}
TY - CPAPER TI - Satisfiability Modulo Constraint Handling Rules (Extended Abstract) AU - Duck, Gregory James T2 - Proceedings of the Twenty-Third International Joint Conference on Artificial Intelligence, IJCAI-13 PB - AAAI Press / International Joint Conferences on Artificial Intelligence PY - 2013 SP - 2997 EP - 3000 UR - https://ijcai.org/proceedings/2013/444 ER -Copied
Machine-readable versions of this paper, for tools and AI agents:
