SMCHR: Satisfiability Modulo Constraint Handling Rules

TL;DR

This paper introduces SMCHR, a novel integration of Constraint Handling Rules with a SAT solver, enabling complex propositional goals within constraint solvers, and explores its practical implementation details.

Contribution

It presents SMCHR, a new system combining CHR with SAT solving, allowing complex propositional constraints and demonstrating practical implementation strategies.

Findings

SMCHR supports complex propositional goals in CHR.

The system uses lazy clause generation for efficient solving.

Practical extensions include equality constraints with unification.

Abstract

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.