SMCHR: satisfiability modulo constraint handling rules
From MaRDI portal
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.
Recommendations
Cites work
- Adaptive CHR Meets CHR ∨
- As time goes by: constraint handling rules
- Parma—bridging the performance gap between imperative and logic programming
- Propagation via lazy clause generation
- Solving SAT and SAT modulo theories, from an abstract Davis-Putnam-Logemann-Loveland procedure to \(\operatorname{DPLL}(T)\)
- SWI-Prolog
Cited in
(4)
This page was built for publication: SMCHR: satisfiability modulo constraint handling rules
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4911137)
