Satisfiability Modulo Constraint Handling Rules (Extended Abstract)

1 Introduction

Constraint Handling Rules (CHR) [Fr¨uhwirth, 1998] is an established [Sneyers et al., 2010] rule-based programming language for the specification and implementation of constraint solvers. CHR has two main types of rules: simplification rules (H ⇐⇒ B) that rewrites constraints H to B, and propagation rules (H =⇒ B) that adds (propagates) constraints B for every H. Constraint solvers are specified as sets of rules.

Example 1 (Bounds Propagation Solver). A bounds propagation solver propagates constraints of the form (x ≥ l) and (x ≤ u) for numeric constants l (lower bound) and u (upper bound). We can specify bounds propagation through addition via the following rules:

Here plus(x, y, z) represents x = y + z, lb(x, l) represents x ≥ l, and ub(x, u) represents x ≤ u. Given an initial goal plus(a, b, c) ∧ lb(b, 3) ∧ ub(b, 10) ∧ lb(c, 4) ∧ ub(c, 6), the rules will propagate lb(a, 7) ∧ ub(a, 16). We can similarly write rules to propagate bounds in other directions.

∗The paper on which this extended abstract is based was the recipient of the best paper award of the 2012 International Conference on Logic Programming [Duck, 2012].

The operational semantics of CHR [Fr¨uhwirth, 1998][Duck et al., 2004][Sneyers et al., 2010] manipulate a global constraint store. The store represents a flat conjunction of constraints. By default CHR does not support goals/stores that are formulae with a rich propositional structure, i.e. containing disjunction, negation, etc. Some CHR systems, such as the K.U.Leuven CHR system [Schrijvers and Demoen, 2004], rely on the host language to provide such functionality. For example, using Prolog's backtracking search to implement disjunction.

In this paper we use a different approach: we extend CHR with a modern Boolean Satisfiability (SAT) solver to form Satisfiability Modulo Constraint Handling Rules (SMCHR). The idea is to specify constraint solvers using CHR in the usual way, such as the rules in Example 1. SMCHR goals are then quantifier-free formulae of CHR constraints over any arbitrary propositional structure.

Example 2 (SMCHRGoal). For example, the following SMCHR goal encodes the classic n-queens problem for the instance n = 2.

This goal can be evaluated using an extended version of the bounds propagation solver from Example 1. For n = 2 the goal is unsatisfiable.

SMCHR is essentially an extensible Satisfiability Modulo Theory (SMT) solver [Moura and Bjørner, 2011] where the theory T solver is implemented in CHR. CHR is a well established [Sneyers et al., 2010] solver specification/implementation language, and is therefore a natural choice for implementing theory solvers.

This paper is organized as follows: Section 2 introduces the CHR language, Section 3 introduces the extended SMCHR language, Section 4 presents the SMCHR execution algorithm DPLL(CHR), Section 5 presents an experimental evaluation, and in Section 6 we conclude.

2 Constraint Handling Rules

This section presents an informal overview of Constraint Handling Rules (CHR). For a formal treatment, see [Fr¨uhwirth, 1998].

CHR is a rule-based programming language with three types of rules:

where the head H, H1, H2, and body B are conjunctions of constraints. CHR solvers apply rules to a set (representing a conjunction) of constraints S known as the constraint store. The store may contain both CHR constraints (as defined by the rules) and/or built-in constraints such as equality x = y, etc. Given a store S, subsets H′ ,E ⊆ S where E are equality constraints, and a matching substitution θ such that E → θ.H = H′ , then a simplification rule (H ⇐⇒ B) rewrites H′ to (θ.B), i.e. S := (S\H′ ) ∪ (θ.B). Likewise, a propagation rule (H =⇒ B) adds (θ.B) whilst retaining H′ , i.e. S := S ∪ (θ.B). Finally a simpagation rule (H1\H2 =⇒ B) is a hybrid between a simplification and propagation rule, where only the constraints H′2 ⊆ S matching H2 are rewritten, i.e. S := (S\H′2 ) ∪ (θ.B). The body B may also contain built-in constraints. The CHR execution algorithm repeatedly applies rules to the store until a fixedpoint is reached or failure occurs.

Example 3 (Less-than-or-equal-to Solver). The following is a simple "less-than-or-equal-to" solver implemented in CHR:

This solver defines a leq constraint with three rules. Rule (1) simplifies any constraint of the form leq(X,X) to the true constraint. Rule (2) simplifies constraints leq(X, Y ) ∧ leq(Y,X) to X = Y . Finally, propagation rule (3) adds a constraint leq(X, Z) for every pair leq(X, Y ) ∧ leq(Y, Z).

Consider the initial store (a.k.a. the goal) G ≡ leq(A, B)∧ leq(B, C) ∧ leq(C, A), then one possible execution sequence (a.k.a. derivation) is as follows:

Here the underlined constraints indicate where the rule is applied. Execution proceeds by first applying the propagation rule (3) which adds the constraint leq(A,C). Next, the simplification rule (2) is applied twice, replacing the leq constraints with equalities. In the final store, no more rules are applicable, so execution stops. In general there may be more than one possible derivation for a given goal.

The logical semantics (or logical interpretation) JRK of a given rule R is defined as follows:

where ∀F represents the universal closure of F. Here and throughout this paper we assume vars(B) ⊆ vars(H).

Example 4 (Logical Semantics). The logical interpretation of each rule from Example 3 is a corresponding partial order axiom, namely: rule (1) is reflexivity ∀x : x ≤ x, rule (2) is antisymmetry ∀x, y : x ≤ y ∧ y ≤ x ↔ x = y, and rule (3) is transitivity ∀x, y, z : x ≤ y ∧ y ≤ z → x ≤ z.

Note the close correspondence between the syntax of CHR and the logical interpretation.

3 SatisfiabilityModulo CHR

Satisfiability Modulo Constraint Handling Rules (SMCHR) differs from CHR in several ways. This section outlines the differences.

The SMCHR language is an extension of CHR. Unlike CHR, SMCHR allows negation in rules.

Example 5 (Negation in SMCHR). If we assume that leq is a total order relation, then we can extend Example 3 with the following rules defining the negation of leq:

Operationally, these rules match negated constraints that explicitly appear in the store, e.g:

The logical semantics of CHR is also extended to allow for negation. The logical interpretation for the above rules is:

Other key differences between CHR and SMCHR include:

• Range-Restricted: We assume all SMCHR rules are range restricted, i.e. for rule head H and body B we have that vars(B) ⊆ vars(H). CHR does not have such a restriction.
• Set-Semantics: CHR uses a multi-set semantics by default, meaning that more than one copy of a constraint may appear in the store at once. SMCHR assumes setsemantics that assumes at most one copy. This is equivalent to assuming the following rules are "built-in" for each constraint symbol c:

Set-Semantics ensures that each constraint c(¯x) can be associated with exactly one propositional variable b. This simplifies the overall design of the SMCHR system.

Goals in CHR are flat conjunctions of constraints. In contrast, SMCHR allows for goals that are any (quantifier-free) formulae with an arbitrary propositional structure, such as that shown in Example 2. Range-Restricted CHR programs ensure that no new (existentially) quantified variables are introduced by rule application.

For a given goal G and a CHR program P , SMCHR generates one of two possible answers: UNSAT or UNKNOWN.

UNSAT means that G is unsatisfiable w.r.t. the theory JPK, i.e. JPK |= ∀¬G. The answer UNKNOWN means that SMCHR was unable to prove unsatisfiability. This may be because G is satisfiable, or that the solver P is incomplete and unable to prove unsatisfiability. This behavior mirrors CHR: if G ↣∗ false, then G is unsatisfiable. Otherwise if G↣∗ S ̸= false, then it is unknown if G is (un)satisfiable.

4 DPLL(CHR): Execution Algorithm

The SMCHR execution algorithm is based on a variant of the Davis-Putnam-Logemann-Loveland (DPLL) [Davis et al., 1962] decision procedure for propositional formulae combined with CHR solving, i.e. DPLL(CHR).

The first step is to translate the goal G into normal form B ∧ D such that:

1. B is a pure propositional formula in CNF;
2. D is a conjunction of equivalences of the form b ↔ c(¯x) where b is a propositional variable and c(¯x) is a constraint; and
3. For all valuations (functions mapping variables to values) s there exists a valuation s′ such that

and s(v) = s′ (v) for all v ∈ vars(G).

The last condition ensures that B ∧ D is equisatisfiable to G and the solutions of G and B ∧ D correspond. There may be many possible normalizations for a given goal G, and the exact normalization algorithm is left to the implementation.

The propositional component B is solved with a Boolean Satisfiability (SAT) solver using a variant of DPLL algorithm. Let Clauses be the set of clauses in B. We assume each clause is a set of the form {l1, .., ln} (representing the disjunction l1 ∨ .. ∨ ln), where each li is a literal b or ¬b for some propositional variable b ∈ vars(B). The pseudo-code for the DPLL algorithm is as follows:

function dpll(Clauses) = while ∃b ∈ vars(Clauses) : unset(b) l := selectLiteral(Clauses) Clauses := setLiteral(Clauses, l) Clauses := unitPropagate(Clauses) if ∅ ∈ Clauses Clauses := backtrack(Clauses) if Level = 0 return UNSAT return UNKNOWN

The DPLL algorithm works by periodically selecting literals l (via selectLiteral()) and setting l to true (via setLiteral()). Next unit propagation (via unitPropagate()) propagates the change through Clauses by eliminating unit clauses {l} and setting l. If this process generates the empty clauses ∅, then the algorithm backtracks (via backtrack()) to a previous state and the search resumes. If the entire search space has been explored (represented by Level = 0), then UNSAT is returned. Otherwise, the algorithm has constructed a valuation s over the propositional variables vars(B) that satisfies B, and the answer UNKNOWN is returned. 1 Our pseudo-code is a simplification. An actual SMCHR implementation will typically use a modern SAT solver design [Een and Srensson, 2003] with conflict-driven search, no-good learning, back-jumping, etc.

1 The answer is "UNKNOWN" since s satisfies B, and not necessarily B ∧ D.

The CHR component of the SMCHR system maintains a global Store of constraints (as shown in Example 3). Whenever the SAT solvers sets a literal l ∈ {b, ¬b} for propositional variable b ∈ vars(B), a chrPropagate() routine is invoked, which is defined as follows:

function chrPropagate(l,Clauses) = if D ≡ (b ↔ c(¯x) ∧ ..) Store := Store ∪ {(l ≡ b? c(¯x) : ¬c(¯x)} let ChrClauses = chrMatch(Rules, Store) Clauses := Clauses ∪ChrClauses return Clauses

If l (via b) corresponds to a constraint c(¯x), then the Store is updated to include c(¯x) if l ≡ b or ¬c(¯x) if l ≡ ¬b. Next the chrMatch routine attempts to match (and apply) a CHR rule. We shall use the notation ˆ c(¯x) to represent a constraint literal c(¯x) or ¬c(¯x). The chrMatch routine searches for a (renamed apart) rule (H1 \ H2 ⇐⇒ B) ∈ Rules and sets of constraints C1,C2,E ⊆ Store such that E is (a minimal set of) equality constraints, and for C1 ⊎ C2 = {ˆ c1(¯x1), .., ˆ cn(¯xn)} and H1 ⊎ H2 = {ˆ c1(¯ y1), .., ˆ cn(¯ yn)} there exists a matching substitution θ such that E → θ.ˆ ci(¯ yi) = ˆ ci(¯xi) for each i ∈ 1..n. If such a matching θ is found, then

1. Delete: We delete C2 by setting Store := Store -C2
2. Create: We create the body constraints as follows: For the rule body B = {ˆ cn+1(¯ z1), .., ˆ cm(¯ zm)} we check for a corresponding conjunct (bi ↔ θ.ci(¯ zi)) in D for some bi. If no such conjunct exists, then we create a new propositional variable b and set D := (b ↔ θ.ci(¯ zi))∧D
3. Generate: Finally we generate clauses that explain the rule application as follows: First we define a function literals() that maps a set of constraints Cs to the set of corresponding set of literals as follows:

where bi ↔ ci(¯x) is the corresponding conjunct of D. Next we define the set of equality literals LE, head literals LH, and body literals LB as follows:

Finally we generate the following set of clauses:

where ¬{l1, .., ln} is shorthand for {¬l1, .., ¬ln} and true(l) indicates that literal l has been set to true.

The generated clauses ChrClauses are added to the clause database of the SAT solver. Note that each generated clause is either a unit clause (if l is unset) or the empty clause (if l is set to false). A unit clause will cause l to be set to true (via unitPropagate()), which in turn causes chrPropagate() to be reinvoked and the corresponding body constraint to be inserted into the Store. This may cause further rule application and clause generation. An empty clause will immediately cause failure and backtracking.

Example 6 (SMCHR Execution). Consider the solver from Example 3 and following goal G:

First we normalize G into a propositional formula in CNF and reify CHR constraints as follows

One possible (simplified) execution tree for G is shown in Figure 1. Here we select literals in order b1, .., b5. Conflict (failure) states are represented by a cross. The states of interest are:

• (A) The start state (no literal set).
• (B) After setting b1 and b2, the constraints leq(A,B) and leq(B,C) appear in the store. Rule (3) from Example 3 is applied, which generates the clause (¬b1 ∨ ¬b2 ∨ b3).
• (C) This branch fails thanks to the clause generated at (B).
• (D) After setting b1, b2, and b5, the constraints leq(A,B), leq(B,C), and A = C appear in the store. Rule (2) from Example 3 is applied, which generates the clause (¬b1 ∨ ¬b2 ∨ ¬b5 ∨ b4).
• (E) The generated clause from (D) is empty and immediately causes failure.

Since all branches lead to failure, the answer for G is UNSAT, i.e. G is unsatisfiable.

Our method is related to lazy clause generation [Ohrimenko et al., 2009] for finite domain solvers, but generalized to any arbitrary CHR solver. Some SMT solvers, such as Z3 [De Moura and Bjørner, 2008], also support clause generation. For example, see T-Propagate from [Bjørner, 2011].

5 Experiments

Since the original publication in [Duck, 2012], the SMCHR system has been actively developed. We experimentally compare four systems: SMCHR is the latest version (alpha release) of the SMCHR system, Native is a built-in (i.e. nonCHR) bounds propagation solver, SMCHR* is the original prototype implementation from [Duck, 2012], and CHR* is the K.U.Leuven CHR system [Schrijvers and Demoen, 2004] running on SWI Prolog [Wielemaker et al., 2012] version 5.8.2. All timings (in milliseconds) are on Intel i5-2500K CPU clocked at 4Ghz and averaged over 10 runs. The results are shown in Figure 1. Here (t.o.) indicates a timeout of 10 minutes, and a dash (-) indicates a benchmark not implemented or not applicable.

The cycle(n), queens(n), and subsets(n, v) benchmarks are from [Duck, 2012]. The remaining benchmarks are: money is the send+more=money crypto-arithmetic puzzle, sudoku is a Sudoku instance, zebra is the zebra puzzle, and steiner(n) computes Steiner triples. The CHR solvers are: leq, lt are the solvers from Examples 3 and 5 respectively, bounds is a bounds propagation solver (see Example 1), domain is a domain propagation solver, and set is a set solver. These solvers are distributed with the SMCHR system.

The no-good learning and search space pruning of SMCHR (both versions) give SMCHR a clear advantage over Prolog CHR for benchmarks that use search. The latest version of SMCHR is a clear improvement over the original implementation. This is mainly because of several new optimizations, such as better search heuristics and hash-table based indexing for the constraint store. Finally, the native implementation of a bounds propagation solver is faster than the SMCHR implementation. This is in line with expectations: a solver implemented in CHR is generally slower than a native implementation, as CHR is generally a trade-off between implementation effort vs. solver speed. Nevertheless, the results suggest that there is room for further optimization.

6 Conclusions

In this paper we presented Satisfiability Modulo Constraint Handling Rules: the natural merger of SMT with CHR. Our experimental results show that SMCHR is faster than CHR, especially for problems that benefit from no-good learning. Furthermore, the latest version of SMCHR is a significant improvement over the original prototype.

Development of SMCHR is ongoing. Future work includes further optimization, applications, and extensions of the SMCHR system.