@raph successfully nerd-sniped me into writing a translator... | Matt Keeter

Matt's posts Post Back to profile

@raph successfully nerd-sniped me into writing a translator from Sudoku grids → Z3 programs.

Doing it in Scheme was a fun exercise: quasiquoting makes it easy to generate SMT-LIB syntax inline, and the whole program is only 27 lines!

Here's the code: https://github.com/mkeeter/sudoku-z3

Screenshot of a Scheme program:

(define (run f rows cols) ; Maps a function across two lists
(let recurse ((rs rows) (cs cols))
(cond ((null? rs) '())
((null? cs) (recurse (cdr rs) cols))
(else (cons (f (car rs) (car cs)) (recurse rs (cdr cs)))))))

(define (sym row col) (string->symbol (format #f "v~A~A" row col)))
(define (assert-char row col) ; Read the board from stdin and declare consts
(define i (- (char->integer (read-char)) (char->integer #\0)))
(define s (sym row col))
(display `(declare-const ,s Int))
(display `(assert (and (>= ,s 1) (<= ,s 9))))
(when (and (>= i 1) (<= i 9)) (display `(assert (= ,s ,i)))))
(run assert-char (iota 9 1) (iota 10 1)) ; (include a '\n' in column count)

(define (assert-block a b) (display `(assert (distinct ,@(run sym a b)))))
(define (assert-row row) (assert-block `(,row) (iota 9 1)))
(define (assert-col col) (assert-block (iota 9 1) `(,col)))
(define (assert-3x3 row col) (assert-block (iota 3 row) (iota 3 col)))
(map (lambda (i) (assert-row i) (assert-col i)) (iota 9 1))
(run assert-3x3 '(1 4 7) '(1 4 7))

(display `(check-sat)) ; Solve, then print the resulting board
(define (digit row col) `(* ,(expt 10 (- 9 col)) ,(sym row col)))
(define (print-row row)
(display `(eval (+ ,@(map (lambda (col) (digit row col)) (iota 9 1))))))
(map print-row (iota 9 1))

Screenshot of a terminal window, reading

➜ sudoku git:(main) cat example.txt
--3-2-6--
9--3-5--1
--18-64--
--81-29--
7-------8
--67-82--
--26-95--
8--2-3--9
--5-1-3--
➜ sudoku git:(main) guile sudoku.scm < example.txt > out.sat && z3 out.sat
sat
483921657
967345821
251876493
548132976
729564138
136798245
372689514
814253769
695417382

Like 18 Nov 2022 at 0:41 | Open on hachyderm.io

No comments