SMCHR - Satisfiability Modulo Constraint Handling Rules

Δ The SMCHR System 1.0

The SMCHR system is an implementation of Satisfiability Modulo Theories (SMT), where the Theory part can be implemented in Constraint Handling Rules (CHR). In practice the SMCHR system is much more, and merges several ideas into one unified platform, including: Boolean Satisfiability (SAT), Satisfiability Modulo Theories (SMT), Constraint Programming (CP), Lazy Clause Generation (LCG) Finite Domain (FD) Solving, and Constraint Handling Rules (CHR) Some applications of the SMCHR system include: solving Constraint Satisfaction Problems (CSPs), solving Boolean Satisfiability problems (SAT), prototyping new theories, theorem proving, program verification and analysis, and any other traditional SMT application.

The name "SMCHR" stands for "Satisfiability Modulo Constraint Handling Rules", and pays homage to the original goal of the SMCHR system, namely the integration of Constraint Handling Rules (CHR) into a Satisfiability Modulo Theories (SMT) solver. In addition to CHR, the SMCHR system support several built-in theory solvers, including, unification (equality) solvers, finite domain (lazy clause generation) solvers, linear arithmetic (Simplex-based) solvers, and Separation-Logic style heap reasoning solvers for program analysis/verification. All built-in solvers are compatible with solvers implemented in Constraint Handling Rules.

Δ Examples

Solvers can be loaded into the SMCHR system using the `--solver name' (or `-s name') command-line option. Once loaded, the SMCHR system can test the satisfiability of (quantifier-free) formulae that include solver-defined constraints. Some example solvers include:

  • leq.chr -- A "less-than-or-equal-to" solver

    The classic less-than-or-equal-to CHR solver is defined by the following rules:

        leq(x, x) <=> true;
        leq(x, y) /\ leq(y, x) ==> x = y;
        leq(x, y) /\ leq(y, z) ==> leq(x, z);
    Each rule encodes a standard axiom for a partial order:

           ∀ x : leq(x, x)        (Reflexivity)
    ∀ x, y: leq(x, y) ∧ leq(y, x) → x = y (Antisymmetry)
    ∀ x, y, z: leq(x, y) ∧ leq(y, z) → leq(x, z) (Transitivity)

    Assuming that the solver is saved in leq.chr, we can load it into the SMCHR system as follows:
        smchr --solver leq.chr --solver eq
    We include the additional built-in solver `eq' to handle the underlying equality constraints. We can use the system to the satisfiability of (quantifier-free) formulae containing CHR-defined constraints. For example, the SMCHR goal
        leq(x, y) /\ leq(y, z) /\ (not leq(x, z) \/ (x != y /\ x = z))
    represents the formula (leq(x, y) ∧ leq(y, z) ∧ (¬ leq(x, z) ∨ (x ≠ y ∧ x = z))) . The SMCHR returns the answer "UNSAT" indicating that the goal is unsatisfiable.

  • heaps.chr -- Separation-Logic style heaps for program reasoning

    Most traditional program reasoning/verification/analysis frameworks model program memory (a.k.a. the heap) as a giant global array, and solve using an array solver. An alternative formalism is Separation Logic, where the heap is represented as a finite partial map between allocated locations (pointers) and the corresponding stored values. Smaller heaps can be combined to form larger heaps with separating conjunction (*). For example the the Separation Logic formula list(l) * tree(t) represents a heap comprised of two smaller disjoint sub-heaps; one containing a list data-structure, and the other containing a tree.

    Separation Logic is formalized as an extension of Hoare Logic. In our CP'2013 paper, we re-encode and generalize some of the ideas of Separation Logic into a constraint language H. We can then build a sound and complete solver for H-constraints defined by the following CHR rules:

        in(h, p, v) /\ in(h, p, w) ==> v = w;
        emp(h) /\ in(h, p, v) ==> false;
        one(h, p, v)                ==> in(h, p, v);
        one(h, p, v) /\ in(h, q, w) ==> p = q /\ v = w;
        sep(h, h1, _) /\ in(h1, p, v)                  ==> in(h, p, v);
        sep(h, _, h2) /\ in(h2, p, v)                  ==> in(h, p, v);
        sep(_, h1, h2) /\ in(h1, p, _) /\ in(h2, q, _) ==> not p = q;
        sep(h, h1, h2) /\ in(h, p, v)                  ==> in(h1, p, v) \/ in(h2, p, v);
    • in(h, p, v) represents heap membership, i.e. (p, v) ∈ h
    • emp(h) constrains h to be the empty heap , i.e. h = ∅
    • one(h, p, v) constrains h to be the singleton heap, i.e. h = {(p, v)}
    • sep(h, h1, h2) constrains h to be the union of two separate sub-heaps, i.e.
      • h = h1 ∪ h2; and
      • dom(h1) ∩ dom(h2) = ∅
    The sep constraint corresponds to separating conjunction, i.e. h is h1 * h2. The first rule defines the functional dependency for the heap membership constraint, i.e., each pointer points to exactly one value. The remaining rules propagate heap membership through the empty, singleton, and separation constraints. This is enough for a sound and complete H-solver.

    Using the SMCHR system loaded with this solver, we can decide program verification problems encoded as satisfiability. For example, consider the following Hoare triple:

    {H = H} x = malloc(1); free(x) {H = H}
    This triple states that the global heap (represented by H) is unchanged by the code (i.e., a malloc followed by an immediate free). This triple is valid iff the following H-formula is unsatisfiable (see our paper for the details)
        emp(T_1) /\ sep(H, H_0, T_1) /\ one(T_2, x, v0) /\ sep(H_1, T_2, H_0) /\
        one(T_3, x, v1) /\ sep(H_1, T_3, Heap) /\ ((one(T_4, s, t) /\ one(T_5, s, u) /\
        sep(H, T_4, T_6) /\ sep(Heap, T_5, T_7) /\ t != u) \/ (sep(H, T_8, T_9) /\
        sep(Heap, T_8, T_10) /\ sep(T_11, T_9, T_10) /\ one(T_12, x, y) /\ sep(T_11, T_12, T_13)))
    We invoke that SMCHR system and the following command-line options:
        smchr --solver heaps.chr --solver eq --solver linear
    Here the built-in solvers `eq' and `linear' handle unification and linear arithmetic respectively. The SMCHR system returns "UNSAT" indicating that the above goal is unsatisfiable, and therefore the above triple is proved to be valid.

    The SMCHR system also supports a built-in implementation of the H-solver, which can be loaded via the `--solver heaps' (without the .chr) command-line option. The built-in implementation is generally faster than pure the CHR version.

  • sudoku.chr -- Solver modeling

    Constraint modeling involves encoding a problem (e.g. a Sudoku puzzle) as a set of constraints in a well-understood domain (e.g. the integers), and to use a constraint solver (e.g. simplex, bounds propagation, etc.) to find a solution. We present an alternative idea: solver modeling, where we encode the problem directly as a constraint theory. For example, we can encode the rules for Sudoku directly as follows:

        square(x, y, a, b, v) /\ square(x, y, a, b, w) ==> v = w;
        square(x, y, a, b, v) /\ square(x, y, c, d, v) ==> a $!= c | false;
        square(x, y, a, b, v) /\ square(x, y, c, d, v) ==> b $!= d | false;
        square(x, y, a, b, v) /\ square(x, z, a, _, v) ==> y $!= z | false;
        square(x, y, a, b, v) /\ square(z, y, _, b, v) ==> x $!= z | false;
    Here square(x, y, a, b, v) represents a square, where (x, y) are the outer grid coordinates, and (a, b) are the inner sub-grid coordinates, and v is the value of the square. The first rule states that a square may only have one value. The remaining rules encode the rules for sudoku, i.e. squares in the same sub-grid must not have the same value, etc.

    In addition to the above rules, we need an auxiliary rule to say what values each square can take:

        squares(x, y, a, b, 0) <=> false;
        squares(x, y, a, b, v) <=> v $> 0 /\ w := v - 1 |
            square(x, y, a, b, v) \/ squares(x, y, a, b, w);
    We also define an auxiliary sudoku(0) constraint that fills all squares. A Sudoku puzzle is merely an initial assignment of squares, which we can represent as a goal:
        sudoku(0) /\ square(1, 1, 1, 1, 3) /\ square(1, 1, 2, 2, 1) /\
        square(1, 1, 2, 3, 2) /\ square(1, 1, 3, 1, 7) /\ square(1, 2, 1, 2, 2) /\
        square(1, 3, 1, 1, 7) /\ square(1, 3, 2, 2, 6) /\ square(1, 3, 3, 2, 3) /\
        square(1, 3, 3, 3, 4) /\ square(2, 1, 1, 2, 5) /\ square(2, 1, 3, 3, 1) /\
        square(2, 2, 1, 2, 7) /\ square(2, 2, 2, 1, 9) /\ square(2, 2, 2, 3, 1) /\
        square(2, 2, 3, 2, 3) /\ square(2, 3, 1, 1, 1) /\ square(2, 3, 3, 2, 8) /\
        square(3, 1, 1, 1, 4) /\ square(3, 1, 1, 2, 2) /\ square(3, 1, 2, 2, 8) /\
        square(3, 1, 3, 3, 6) /\ square(3, 2, 3, 2, 8) /\ square(3, 3, 1, 3, 9) /\
        square(3, 3, 2, 1, 6) /\ square(3, 3, 2, 2, 1) /\ square(3, 3, 3, 3, 2)
    When we invoke the SMCHR system as follows:
        smchr --solver sudoku.chr
    then SMCHR will print the following constraints:
        square(1,1,1,1,3) /\
        square(1,1,1,2,4) /\
        square(1,1,1,3,9) /\
        square(1,1,2,1,5) /\
    which represents the solution to the puzzle.

Δ No SMTLIB Support

The SMCHR system supports a simple and easy-to-use interface that is not based on the SMTLIB syntax. For an example, consider the goal representation of the formula p ∧ ¬ p in both SMTLIB and SMCHR syntax:

SMTLIB Syntax SMCHR Syntax
(set-logic QF_UF)
(declare-fun p () Bool)
(assert (and p (not p)))
      p /\ not p      
Δ FlatZinc Support

The SMCHR package also includes a simple FlatZinc translation tool. Only a subset of FlatZinc is supported, and there currently is no support for optimization problems (i.e. `solve satisfy' only). To use SMCHR to solve a problem encoded in FlatZinc, run the following command:

$ tools/flatzinc.linux model.fzn | ./smchr.linux --solver bounds,dom | tools/answer.linux
Here tools/flatzinc.linux is the FlatZinc translation tool, and tools/answer.linux pretty prints the output in a more human readable form. The options `--solver bounds,dom' load the built-in bounds propagation and domain solvers.

Δ Downloads

The SMCHR system is released under the terms of the GNU General Public License (version 3). Currently 64-bit (x86_64/AMD64) Linux/MacOSX/Windows systems are supported.

Note: The SMCHR garbage collector uses large amounts of virtual address space by design. This may cause problems if memory overcommit is disabled, or if the maximum virtual address space size is restricted (e.g. with ulimit -v). To fix these problems (on Linux) run:

$ sudo echo 0 > /proc/sys/vm/overcommit_memory
$ ulimit -S -v unlimited

Δ Further Reading

More information is available in the SMCHR manual:

The following publications relate to SMCHR:

The SMCHR system uses a new type of conservative Garbage Collector (GC) design. See this page for more information.

© Copyright 2013, all rights reserved