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)))))
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.