synthesize: Failing to generate a sudoku puzzle

[m4burns]

Hello,

I'm attempting to generate a sudoku puzzle with N clues. A valid sudoku puzzle can have only one distinct solution, so I'm synthesizing a set of clues such that any two solutions that satisfy the clues must be equal.

This approach works when N is set to a high value (e.g. 50 or 81), but synthesize returns (unsat) when N is set to a lower value for which sudokus still exist (e.g. 24).

I'm using Rosette 4.0 on a snapshot build of Racket (8.3.0.5). Here's the code:

#lang rosette

(current-bitwidth #f)

; a filled sudoku
(define (make-sudoku)
  (for/list ([i 81])
    (define-symbolic* x integer?)
    (assume (<= 1 x 9))
    x))

; an unfilled sudoku
; value 0 represents a blank space in the sudoku
(define (make-cluegrid)
  (for/list ([i 81])
    (define-symbolic* x integer?)
    (assume (<= 0 x 9))
    x))

; count number of non-blank spaces in a cluegrid
(define (cluegrid-clues cg)
  (foldl + 0 (map (lambda (x) (if (= x 0) 0 1)) cg)))

; check that the value of each non-blank space in the cluegrid
; matches the corresponding value in the sudoku
(define (cluegrid-satisfied? cluegrid sudoku)
  (andmap
   (lambda (c x)
     (or (= 0 c)
         (= c x)))
   cluegrid sudoku))

; get value at row r column c
(define (ref s r c)
  (list-ref s (+ (* 9 r) c)))

; check that s respects all the sudoku constraints
(define (solution? s)
  (and
   (andmap identity
           (for/list ([i 9])
             (and
              ; column values distinct
              (apply distinct? (for/list ([j 9]) (ref s i j)))
              ; row values distinct
              (apply distinct? (for/list ([j 9]) (ref s j i))))))
   (andmap identity
           (for*/list ([r 3] [c 3])
             ; 3x3 subgrid values distinct
             (apply distinct?
                    (for*/list ([dr 3] [dc 3])
                      (ref s (+ (* 3 r) dr) (+ (* 3 c) dc))))))))

(define g (make-cluegrid))
(define x (make-sudoku))
(define y (make-sudoku))

; find a cluegrid with N non-blank entries having
; only one distinct sudoku solution
(define (find-cluegrid N)
  (synthesize
   #:forall (append x y)
   #:guarantee
   (begin
     (assume (and (= (cluegrid-clues g) N)
                  (cluegrid-satisfied? g x)
                  (cluegrid-satisfied? g y)
                  (solution? x)
                  (solution? y)))
     (assert (equal? x y)))))

; this works
(find-cluegrid 81)

; this also works
(find-cluegrid 50)

; this returns (unsat), but there are many examples of sudokus with 24 clues
(find-cluegrid 24)

I've tried similar approaches using choice* and bitvectors, but I hit the same issue every time. I'd really appreciate some help finding any mistake here that I'm not seeing.

PS: Thank you for the excellent tool!

[emina]

Hello,

The way your synthesis query is formulated is slightly wrong. The desired query is this: there exists a clue-grid g and a solution x for that clue-grid, such that for all y, if y is a solution for g, then y must be equal to x. Your query is doing universal quantification over x too and is asking for something stronger.

Below is the modified query, and I've changed the rest of the code slightly to accommodate it. The modified query works for N = 35, for example, while the original one doesn't work for N < 40. This bound for the original query might be related to the mathematics of Sudoku: https://cs.stackexchange.com/questions/163/minimum-number-of-clues-to-fully-specify-any-sudoku

I haven't had the patience to wait for N = 24 to come back for the modified query :)

#lang rosette

(current-bitwidth #f)

(define (sudoku-values? xs)
  (andmap (lambda (x) (<= 1 x 9)) xs))

(define (cluegrid-values? xs)
  (andmap (lambda (x) (<= 0 x 9)) xs))

; count number of non-blank spaces in a cluegrid
(define (cluegrid-clues cg)
  (apply + (map (lambda (x) (if (= x 0) 0 1)) cg)))

; check that the value of each non-blank space in the cluegrid
; matches the corresponding value in the sudoku
(define (cluegrid-satisfied? cluegrid sudoku)
  (andmap
   (lambda (c x)
     (or (= 0 c)
         (= c x)))
   cluegrid sudoku))

; get value at row r column c
(define (ref s r c)
  (list-ref s (+ (* 9 r) c)))

; check that s respects all the sudoku constraints
(define (solution? s)
  (and
   (andmap identity
           (for/list ([i 9])
             (&&
              ; column values distinct
              (apply distinct? (for/list ([j 9]) (ref s i j)))
              ; row values distinct
              (apply distinct? (for/list ([j 9]) (ref s j i))))))
   (andmap identity
           (for*/list ([r 3] [c 3])
             ; 3x3 subgrid values distinct
             (apply distinct?
                    (for*/list ([dr 3] [dc 3])
                      (ref s (+ (* 3 r) dr) (+ (* 3 c) dc))))))))

(define-symbolic* g integer? #:length 81)
(define-symbolic* x integer? #:length 81)
(define-symbolic* y integer? #:length 81)

; find a cluegrid with N non-blank entries having
; only one distinct sudoku solution
(define (find-cluegrid N)
  (synthesize
   #:forall y
   #:guarantee
   (begin
     (assert (sudoku-values? x))
     (assert (cluegrid-values? g))
     (assert (= (cluegrid-clues g) N))
     (assert (cluegrid-satisfied? g x))
     (assert (solution? x))
     (assert
      (=>
       (&& (solution? y)
           (sudoku-values? y)
           (cluegrid-satisfied? g y))
       (equal? x y))))))

; this works
;(find-cluegrid 81)

; this also works
;(find-cluegrid 50)

; this also works:
; this also works:
(define m35 (find-cluegrid 35))
(evaluate x m35)
(evaluate g m35)

; this is taking a long time ...
; (find-cluegrid 24)

[m4burns]

Thank you for the quick answer! The changes you made make sense to me, and I understand why your version successfully synthesizes. However, I couldn't understand why the query in my version is asking for something stronger. Perhaps this is missing some nuance, but here's my thought process:

Let P = there exists a clue-grid g and a solution x for that clue-grid, such that for all y, if y is a solution for g, then y = x

Let Q = for all u and v that are solutions for g, u = v

Fix some g and x satisfying P. Seeking a contradiction, suppose Q fails for this g, and (u,v) is a counterexample. Assume WLOG u =/= x. Since u is a solution for g, setting y to u in P causes P to fail. So Q succeeds for the fixed value of g. Therefore, whenever P is satisfiable, ∃ g. Q is also satisfiable.

I edited your version into this simpler program where solve on a quantified formula produces a model but synthesize on what should be the same formula produces unsat:

#lang rosette
(current-bitwidth #f)

(define (solution-values? xs)
  (andmap (lambda (x) (<= 1 x 3)) xs))

(define (cluegrid-values? xs)
  (andmap (lambda (x) (<= 0 x 3)) xs))

; count number of non-blank spaces in a cluegrid
(define (cluegrid-clues cg)
  (apply + (map (lambda (x) (if (= x 0) 0 1)) cg)))

; check that the value of each non-blank space in the cluegrid
; matches the corresponding value in the solution
(define (cluegrid-satisfied? cluegrid solution)
  (andmap
   (lambda (c x)
     (or (= 0 c)
         (= c x)))
   cluegrid solution))

; get value at row r column c
(define (ref s r c)
  (list-ref s (+ (* 3 r) c)))

; check that rows and columns of s contain distinct values
(define (solution? s)
  (and
   (andmap identity
           (for/list ([i 3])
             (&&
              ; column values distinct
              (apply distinct? (for/list ([j 3]) (ref s i j)))
              ; row values distinct
              (apply distinct? (for/list ([j 3]) (ref s j i))))))))

(define-symbolic* g integer? #:length 9)
(define-symbolic* x integer? #:length 9)
(define-symbolic* y integer? #:length 9)

(define N 2)

; this should be synthesize's pre(H, I)
; let x be free to simplify this
(define pre
  (and (cluegrid-values? g)
       (= (cluegrid-clues g) N)
       (solution? y)
       (solution-values? y)
       (cluegrid-satisfied? g y)))

; this should be synthesize's post(H, I)
(define post
  (equal? x y))

(clear-vc!)

; this produces unsat
(synthesize
 #:forall y
 #:guarantee
 (begin
   ; pre(H, I) = (vc-assumes P) ∧ (vc-asserts P) ∧ (vc-assumes Q)
   ; P was cleared above
   ; (vc-assumes Q) = pre
   ; post(H, I) = (vc-asserts Q) = post
   (assume pre)
   (assert post)))

(clear-vc!)

; this produces (model ...)
(solve
 (assert
  ; this should be equivalent to the documented formula for `synthesize`:
  ;  ∃ H. (∃ I. pre(H, I)) ∧ (∀ I. pre(H, I) ⇒ post(H, I))
  ; where I = { y }
  ;       H = { x, g }
  ;       pre(H, I) = pre
  ;       post(H, I) = post
  (and (exists y pre)
       (forall y (=> pre post)))))

Should solve and synthesize produce the same result in this program?

I adopted your changes and rewrote synthesize to solve in my original program, still quantifying over x and y. This produced a 4x4 sudoku model for N = 5, where synthesize fails to do so:

#lang rosette

(current-bitwidth #f)

(define (sudoku-values? xs)
  (andmap (lambda (x) (<= 1 x 4)) xs))

(define (cluegrid-values? xs)
  (andmap (lambda (x) (<= 0 x 4)) xs))

; count number of non-blank spaces in a cluegrid
(define (cluegrid-clues cg)
  (foldl + 0 (map (lambda (x) (if (= x 0) 0 1)) cg)))

; check that the value of each non-blank space in the cluegrid
; matches the corresponding value in the sudoku
(define (cluegrid-satisfied? cluegrid sudoku)
  (andmap
   (lambda (c x)
     (or (= 0 c)
         (= c x)))
   cluegrid sudoku))

; get value at row r column c
(define (ref s r c)
  (list-ref s (+ (* 4 r) c)))

; check that s respects all the sudoku constraints
(define (solution? s)
  (and
   (andmap identity
           (for/list ([i 4])
             (and
              ; column values distinct
              (apply distinct? (for/list ([j 4]) (ref s i j)))
              ; row values distinct
              (apply distinct? (for/list ([j 4]) (ref s j i))))))
   (andmap identity
           (for*/list ([r 2] [c 2])
             ; 3x3 subgrid values distinct
             (apply distinct?
                    (for*/list ([dr 2] [dc 2])
                      (ref s (+ (* 2 r) dr) (+ (* 2 c) dc))))))))

(define-symbolic* g integer? #:length 16)
(define-symbolic* x integer? #:length 16)
(define-symbolic* y integer? #:length 16)

(define N 5)

(define pre (and (= (cluegrid-clues g) N)
                 (sudoku-values? x)
                 (sudoku-values? y)
                 (cluegrid-values? g)
                 (cluegrid-satisfied? g x)
                 (cluegrid-satisfied? g y)
                 (solution? x)
                 (solution? y)))

(define post (equal? x y))

(clear-vc!)

; (unsat)
(synthesize
 #:forall (append x y)
 #:guarantee
 (begin
   (assume pre)
   (assert post)))

(clear-vc!)

; (model ...)
(solve
 (assert
  (and
   (exists (append x y) pre)
   (forall (append x y) (=> pre post)))))

This leads me to believe my understanding of what synthesize is doing is not quite right, or there is some mismatch between synthesize and solve (and (exists I pre) (forall I (=> pre post))).

Any further guidance would be greatly appreciated :)

[emina]

Yes, synthesize does something different. It doesn't solve the "\exists\forall" query in the same way that a direct call to the solver would. The semantics is explained here: https://docs.racket-lang.org/rosette-guide/ch_syntactic-forms_rosette.html#%28part._.Synthesis%29

Essentially, the classic "\exists\forall" query will synthesize a "vacuous" program whenever the precondition of that query is equivalent to "false". It's fine to return any program in that case, because there are, of course, no inputs that satisfy its precondition.

Rosette's synthesize query will refuse to synthesize a program in this case, and it will return unsat. So, when you get a program out, you also know that there are at least some inputs that satisfy the program's precondition.

The following snippet demonstrates the difference:

#lang rosette

(define-symbolic x y integer?)

; This returns unsat:
(synthesize
 #:forall x
 #:guarantee
 (begin
   (assume (= (+ x 2) (+ x 3))) ; false
   (assert (= x y))))

; This returns a vacuous solution (y = 0):
(solve
 (assert
  (forall (list x)
   (=> (= (+ x 2) (+ x 3)) (= x y)))))

[m4burns]

Yes, that makes sense, but the mismatch I encountered is that (solve (assert (and (exists I pre) (forall I (=> pre post))))) is satisfiable while (synthesize #:forall I #:guarantee (begin (assume pre) (assert post))) is not. I will try to find a simpler example that triggers this.

[emina]

I looked into this more, and it turns out that Rosette's CEGIS implementation was solving for a formula that's too strong.

Instead of solving for ∃ H. (∃ I. pre(H, I)) ∧ (∀ I. pre(H, I) ⇒ post(H, I)), as intended, it was actually searching for more than one input that satisfies the precondition.

That's why synthesize was returning unsat on your example when it should have been sat.

I've pushed a patch to the implementation, which now requires just one input to satisfy the precondition. Your examples work as expected with the patched query (modulo the 24-clue example taking longer than I have the patience to wait :).

Great catch; thank you!

P.S. I'd still recommend using the solution that quantifies over fewer variables, as the smaller number of quantified variables leads to better performance.

[m4burns]

Glad I could help, and thanks for the advice!