---
title: "Satisfiability Modulo Constraint Handling Rules (Extended Abstract)"
authors:
  - "Gregory James Duck"
doi: ""
url: "https://ijcai.org/proceedings/2013/444"
pdf: "https://ijcai.org/proceedings/2013/0444.pdf"
venue: "Proceedings of the Twenty-Third International Joint Conference on Artificial Intelligence"
year: 2013
pages: "2997-3000"
track: ""
keywords:
---

# Satisfiability Modulo Constraint Handling Rules (Extended Abstract)

Gregory James Duck

*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.