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.