  Constraint Handling Rules (CHRs) are a high-level rule-based programming
language for specification and implementation of constraint solvers. CHR
manipulates a global store representing a flat conjunction of constraints. By
default, CHR does not support goals with a more complex propositional structure
including disjunction, negation, etc., or CHR relies on the host system to
provide such features. In this paper we introduce Satisfiability Modulo
Constraint Handling Rules (SMCHR): a tight integration of CHR with a modern
Boolean Satisfiability (SAT) solver for 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. The execution
algorithm of SMCHR is based on lazy clause generation, where a new clause for
the SAT solver is generated whenever a rule is applied. We shall also explore
the practical aspects of building an SMCHR system, including extending a
"built-in" constraint solver supporting equality with unification and
justifications.
