# 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
• 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 $x + y = z$, where the domain of all variables is $\{ 0, 1 \}$:

```(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.