A simple Constraint Programming implementation

Constraint programming is a programming paradigm where problems are stated declaratively. In this post, I will implement a very simple constraint solver.

Lately everything has been revolving around constraint programming, to name a few:

• My master’s thesis is using the programming language Dafny, which in turn uses Z3 which uses several constraint techniques
• I played Superliminal lately, which was also related to constraints in a way
• Had a discussion with a friend about extending Sudoku constraints
• This tweet

I think those hints were enough for me to implement a very basic constraint solver 🙂 I found these slides online, and they were helpful enough to dive into Racket.

I started by defining the structures that we’ll need:

(define-struct variable (name domain) #:prefab)
(define-struct constraint (variables formula) #:prefab)
(define-struct cpair (name value) #:prefab)

A simple example, representing the problem , where the domain of all variables is :

(constraint (list (variable 'x '(0 1))
                  (variable 'y '(0 1))
                  (variable 'z '(0 1)))
            '(= (+ x y) z))

How can we approach to solving this problem? The easiest way is to use a brute-force approach, by generating all possible combinations for the variables and testing every combination against the formula. There is a harder and more optimal way, by using partial evaluation (backtracking), but we will not do that here.

First, we start by defining a procedure for calculating all possible combinations of variables and domains:

(define (get-all-pairs c)
  (letrec ([vars (constraint-variables c)]
           [varnames (map variable-name vars)]
           [tuples (apply cartesian-product (map variable-domain vars))])
    (map (lambda (x) (map cpair varnames x)) tuples)))

So calling that against the example constraint we used earlier will return:

'((#s(cpair x 0) #s(cpair y 0) #s(cpair z 0))
  (#s(cpair x 0) #s(cpair y 0) #s(cpair z 1))
  (#s(cpair x 0) #s(cpair y 1) #s(cpair z 0))
  (#s(cpair x 0) #s(cpair y 1) #s(cpair z 1))
  (#s(cpair x 1) #s(cpair y 0) #s(cpair z 0))
  (#s(cpair x 1) #s(cpair y 0) #s(cpair z 1))
  (#s(cpair x 1) #s(cpair y 1) #s(cpair z 0))
  (#s(cpair x 1) #s(cpair y 1) #s(cpair z 1)))

Next, we need a procedure to test a pair:

(define (test-pair f p)
  (cond ((eq? p '()) (eval-expr f))
        (else (let ([current-pair (car p)]
                    [remaining-pairs (cdr p)])
                (test-pair (subst (cpair-name current-pair)
                                  (cpair-value current-pair)
                                  f)
                           remaining-pairs)))))

It uses an earlier definition of subst, and also a simple evaluator based off of my book.

Finally, the last procedure for finding the solution:

(define (find-sat c)
  (define (go f ps)
    (cond ((null? ps) '())
          ((test-pair f (car ps)) (car ps))
          (else (go f (cdr ps)))))
  (letrec ([formula (constraint-formula c)]
           [pairs (get-all-pairs c)])
    (go formula pairs)))

So calling it on the previous constraint will return:

'(#s(cpair x 0) #s(cpair y 0) #s(cpair z 0))

You can check the complete example here which also includes a solver model for 2×2 Sudoku.