↫ Home

Solving a mathemattic problem using Rosette

Would n’t it be interesting if programming language is aided with SMT solvers. Rosette is such language. Using SMT solvers Rosette can verify that programs comply their specifications, synthesis programs given specifications, find counter examples when program doesn’t meet its specification and solve puzzles.

In this blogpost, I will be using Rosette to solve a puzzle which is taken from Crux Volume 47, Issue 5.

Let’s fire up Dr Racket where Rosette is available, give language directive to Racket and import a Rosette module.

#lang rosette
(require rosette/lib/angelic)

Next lets define all professions mentioned in the puzzle as elements of a list.

(define professions (list 'baker 'carpenter 'driver 'plumber))

Now we will assign professions to persons. But instead of traditional assignment, We will say profession of a person is any one within list. choose* method from angelic module allows us to do this. A note on encoding I am using variables for persons and symbols for professions.

(define baker (apply choose* profession))
(define carpenter (apply choose* profession))
(define driver (apply choose* profession))
(define plumber (apply choose* profession))

Let us list down constraints (fixed) which are true. Each person has different profession and person name don’t coincide with their profession. Even though we have n’t assigned profession to person in traditional sense, first constraint instructs that assigned values are all distinct.

(define (f-constraints)
  (list (distinct? baker driver carpenter plumber)
        (not (equal? baker 'baker))
        (not (equal? driver 'driver))
        (not (equal? carpenter 'carpenter))
        (not (equal? plumber 'plumber))))

Next note down constraints (variable) which may or may not hold as some statements might be false.

(define (v-constraints)
  (list (equal? baker 'plumber)
        (equal? driver 'baker)
        (! (equal? carpenter 'plumber))
        (! (equal? plumber 'carpenter))))

Before proceeding further we need helper method to find who is assigned given profession in solution once assignment is done by SMT solver. profession is an element of professions and sol is solution returned by SMT solver. evaluate find assignement of variable in solution.

(define (assigned profession sol)
  (first (filter (lambda (p) (equal? (evaluate p sol) profession))
          (list baker carpenter driver plumber))))

We are now at crux of our small program where we write function to fix assignment of person (variable) to profession (symbol) with help of SMT solver which is invoked using solve+. First we will find assignment with constraint given as parameter. If no assignment exists due constraints being too restricting we return empty list else we try to find another solution where driver profession is not assigned to same person as first solution. If such assignment exists we return these two solutions in list otherwise we return only one solution in list.

(define (m-solve constraint)
  (define s-solve (solve+))
  (let ([sol (s-solve constraint)])
    (if (sat? sol)
        (letrec ([a-driver (assigned 'driver sol)]
                 [n-sol (s-solve (not (equal? 'driver a-driver)))])
            (cons sol (if (sat? n-sol) (list n-sol) (list))))
        (list))))

Finally let us solve the puzzle. We iterate through 0 to 4 assuming it is number of true statements which is anded with fixed constraints then asking for solution using m-solve. If only one solution exists we have found what we are looking for. Once we find that solution we ask profession assigned to each person. As you can see answer to our little puzzle is baker.

(define a-solutions 
    (filter (lambda (s) (= (length s) 1))
            (for/list ([t (range 5)])
                (m-solve 
                  (and (apply && (f-constraints))
                       (= t (length (filter identity (v-constraints)))))))))

(length a-solutions)
(define sol (first (first a-solutions)))
(evaluate (list baker carpenter driver plumber) sol)
Welcome to DrRacket, version 8.0 [cs].
Language: rosette, with debugging; memory limit: 128 MB.
1
'(driver plumber carpenter baker)
> 

Complete source code can be found here.