https://rise4fun.com/z3/tutorial
; Sudoku 9x9
; setup board
; a11 a12 a13 | b11 b12 b13 | c11 c12 c13
; a21 a22 a23 | b21 b22 b23 | c21 c22 c23
; a31 a32 a33 | b31 b32 b33 | c31 c32 c33
; ------------+-------------+------------
; d11 d12 d13 | e11 e12 e13 | f11 f12 f13
; d21 d22 d23 | e21 e22 e23 | f21 f22 f23
; d31 d32 d33 | e31 e32 e33 | f31 f32 f33
; ------------+-------------+------------
; g11 g12 g13 | h11 h12 h13 | i11 i12 i13
; g21 g22 g23 | h21 h22 h23 | i21 i22 i23
; g31 g32 g33 | h31 h32 h33 | i31 i32 i33
(declare-const a11 Int)
(declare-const a12 Int)
(declare-const a13 Int)
(declare-const a21 Int)
(declare-const a22 Int)
(declare-const a23 Int)
(declare-const a31 Int)
(declare-const a32 Int)
(declare-const a33 Int)
(declare-const b11 Int)
(declare-const b12 Int)
(declare-const b13 Int)
(declare-const b21 Int)
(declare-const b22 Int)
(declare-const b23 Int)
(declare-const b31 Int)
(declare-const b32 Int)
(declare-const b33 Int)
(declare-const c11 Int)
(declare-const c12 Int)
(declare-const c13 Int)
(declare-const c21 Int)
(declare-const c22 Int)
(declare-const c23 Int)
(declare-const c31 Int)
(declare-const c32 Int)
(declare-const c33 Int)
(declare-const d11 Int)
(declare-const d12 Int)
(declare-const d13 Int)
(declare-const d21 Int)
(declare-const d22 Int)
(declare-const d23 Int)
(declare-const d31 Int)
(declare-const d32 Int)
(declare-const d33 Int)
(declare-const e11 Int)
(declare-const e12 Int)
(declare-const e13 Int)
(declare-const e21 Int)
(declare-const e22 Int)
(declare-const e23 Int)
(declare-const e31 Int)
(declare-const e32 Int)
(declare-const e33 Int)
(declare-const f11 Int)
(declare-const f12 Int)
(declare-const f13 Int)
(declare-const f21 Int)
(declare-const f22 Int)
(declare-const f23 Int)
(declare-const f31 Int)
(declare-const f32 Int)
(declare-const f33 Int)
(declare-const g11 Int)
(declare-const g12 Int)
(declare-const g13 Int)
(declare-const g21 Int)
(declare-const g22 Int)
(declare-const g23 Int)
(declare-const g31 Int)
(declare-const g32 Int)
(declare-const g33 Int)
(declare-const h11 Int)
(declare-const h12 Int)
(declare-const h13 Int)
(declare-const h21 Int)
(declare-const h22 Int)
(declare-const h23 Int)
(declare-const h31 Int)
(declare-const h32 Int)
(declare-const h33 Int)
(declare-const i11 Int)
(declare-const i12 Int)
(declare-const i13 Int)
(declare-const i21 Int)
(declare-const i22 Int)
(declare-const i23 Int)
(declare-const i31 Int)
(declare-const i32 Int)
(declare-const i33 Int)
; constrain values 1-9
(define-fun between ((num Int) (min Int) (max Int)) Bool
(and (>= num min) (<= num max)))
(assert (between a11 1 9))
(assert (between a12 1 9))
(assert (between a13 1 9))
(assert (between a21 1 9))
(assert (between a22 1 9))
(assert (between a23 1 9))
(assert (between a31 1 9))
(assert (between a32 1 9))
(assert (between a33 1 9))
(assert (between b11 1 9))
(assert (between b12 1 9))
(assert (between b13 1 9))
(assert (between b21 1 9))
(assert (between b22 1 9))
(assert (between b23 1 9))
(assert (between b31 1 9))
(assert (between b32 1 9))
(assert (between b33 1 9))
(assert (between c11 1 9))
(assert (between c12 1 9))
(assert (between c13 1 9))
(assert (between c21 1 9))
(assert (between c22 1 9))
(assert (between c23 1 9))
(assert (between c31 1 9))
(assert (between c32 1 9))
(assert (between c33 1 9))
(assert (between d11 1 9))
(assert (between d12 1 9))
(assert (between d13 1 9))
(assert (between d21 1 9))
(assert (between d22 1 9))
(assert (between d23 1 9))
(assert (between d31 1 9))
(assert (between d32 1 9))
(assert (between d33 1 9))
(assert (between e11 1 9))
(assert (between e12 1 9))
(assert (between e13 1 9))
(assert (between e21 1 9))
(assert (between e22 1 9))
(assert (between e23 1 9))
(assert (between e31 1 9))
(assert (between e32 1 9))
(assert (between e33 1 9))
(assert (between f11 1 9))
(assert (between f12 1 9))
(assert (between f13 1 9))
(assert (between f21 1 9))
(assert (between f22 1 9))
(assert (between f23 1 9))
(assert (between f31 1 9))
(assert (between f32 1 9))
(assert (between f33 1 9))
(assert (between g11 1 9))
(assert (between g12 1 9))
(assert (between g13 1 9))
(assert (between g21 1 9))
(assert (between g22 1 9))
(assert (between g23 1 9))
(assert (between g31 1 9))
(assert (between g32 1 9))
(assert (between g33 1 9))
(assert (between h11 1 9))
(assert (between h12 1 9))
(assert (between h13 1 9))
(assert (between h21 1 9))
(assert (between h22 1 9))
(assert (between h23 1 9))
(assert (between h31 1 9))
(assert (between h32 1 9))
(assert (between h33 1 9))
(assert (between i11 1 9))
(assert (between i12 1 9))
(assert (between i13 1 9))
(assert (between i21 1 9))
(assert (between i22 1 9))
(assert (between i23 1 9))
(assert (between i31 1 9))
(assert (between i32 1 9))
(assert (between i33 1 9))
; distinct numbers in boxes
(assert (distinct a11 a12 a13 a21 a22 a23 a31 a32 a33))
(assert (distinct b11 b12 b13 b21 b22 b23 b31 b32 b33))
(assert (distinct c11 c12 c13 c21 c22 c23 c31 c32 c33))
(assert (distinct d11 d12 d13 d21 d22 d23 d31 d32 d33))
(assert (distinct e11 e12 e13 e21 e22 e23 e31 e32 e33))
(assert (distinct f11 f12 f13 f21 f22 f23 f31 f32 f33))
(assert (distinct g11 g12 g13 g21 g22 g23 g31 g32 g33))
(assert (distinct h11 h12 h13 h21 h22 h23 h31 h32 h33))
(assert (distinct i11 i12 i13 i21 i22 i23 i31 i32 i33))
; distinct numbers in rows
(assert (distinct a11 a12 a13 b11 b12 b13 c11 c12 c13))
(assert (distinct a21 a22 a23 b21 b22 b23 c21 c22 c23))
(assert (distinct a31 a32 a33 b31 b32 b33 c31 c32 c33))
(assert (distinct d11 d12 d13 e11 e12 e13 f11 f12 f13))
(assert (distinct d21 d22 d23 e21 e22 e23 f21 f22 f23))
(assert (distinct d31 d32 d33 e31 e32 e33 f31 f32 f33))
(assert (distinct g11 g12 g13 h11 h12 h13 i11 i12 i13))
(assert (distinct g21 g22 g23 h21 h22 h23 i21 i22 i23))
(assert (distinct g31 g32 g33 h31 h32 h33 i31 i32 i33))
; distinct numbers in columns
(assert (distinct a11 a21 a31 d11 d21 d31 g11 g21 g31))
(assert (distinct a12 a22 a32 d12 d22 d32 g12 g22 g32))
(assert (distinct a13 a23 a33 d13 d23 d33 g13 g23 g33))
(assert (distinct b11 b21 b31 e11 e21 e31 h11 h21 h31))
(assert (distinct b12 b22 b32 e12 e22 e32 h12 h22 h32))
(assert (distinct b13 b23 b33 e13 e23 e33 h13 h23 h33))
(assert (distinct c11 c21 c31 f11 f21 f31 i11 i21 i31))
(assert (distinct c12 c22 c32 f12 f22 f32 i12 i22 i32))
(assert (distinct c13 c23 c33 f13 f23 f33 i13 i23 i33))
; setup complete
(push)
; puzzle
; a11 a12 (1) | b11 (4) (6) | c11 c12 (2)
; a21 (9) a23 | b21 b22 (8) | c21 c22 c23
; a31 (8) a33 | (5) b32 b33 | c31 c32 c33
; ------------+-------------+------------
; d11 d12 d13 | (2) e12 e13 | f11 f12 f13
; (1) (3) (8) | e21 e22 e23 | f21 (5) f23
; d31 (7) (6) | (3) e32 e33 | f31 f32 f33
; ------------+-------------+------------
; g11 (1) g13 | h11 (9) h13 | i11 i12 (8)
; (3) g22 g23 | h21 h22 (5) | (4) (2) i23
; g31 g32 g33 | h31 h32 h33 | i31 (6) (1)
(assert (= a13 1))
(assert (= a22 9))
(assert (= a32 8))
(assert (= b12 4))
(assert (= b13 6))
(assert (= b23 8))
(assert (= b31 5))
(assert (= c13 2))
(assert (= d21 1))
(assert (= d22 3))
(assert (= d23 8))
(assert (= d32 7))
(assert (= d33 6))
(assert (= e11 2))
(assert (= e31 3))
(assert (= f22 5))
(assert (= g12 1))
(assert (= g21 3))
(assert (= h12 9))
(assert (= h23 5))
(assert (= i13 8))
(assert (= i21 4))
(assert (= i22 2))
(assert (= i32 6))
(assert (= i33 1))
(check-sat)
(echo "Results:")
(eval (str.++ (int.to.str a11) " " (int.to.str a12) " " (int.to.str a13) " | " (int.to.str b11) " " (int.to.str b12) " " (int.to.str b13) " | " (int.to.str c11) " " (int.to.str c12) " " (int.to.str c13)))
(eval (str.++ (int.to.str a21) " " (int.to.str a22) " " (int.to.str a23) " | " (int.to.str b21) " " (int.to.str b22) " " (int.to.str b23) " | " (int.to.str c21) " " (int.to.str c22) " " (int.to.str c23)))
(eval (str.++ (int.to.str a31) " " (int.to.str a32) " " (int.to.str a33) " | " (int.to.str b31) " " (int.to.str b32) " " (int.to.str b33) " | " (int.to.str c31) " " (int.to.str c32) " " (int.to.str c33)))
(echo "-------+-------+-------")
(eval (str.++ (int.to.str d11) " " (int.to.str d12) " " (int.to.str d13) " | " (int.to.str e11) " " (int.to.str e12) " " (int.to.str e13) " | " (int.to.str f11) " " (int.to.str f12) " " (int.to.str f13)))
(eval (str.++ (int.to.str d21) " " (int.to.str d22) " " (int.to.str d23) " | " (int.to.str e21) " " (int.to.str e22) " " (int.to.str e23) " | " (int.to.str f21) " " (int.to.str f22) " " (int.to.str f23)))
(eval (str.++ (int.to.str d31) " " (int.to.str d32) " " (int.to.str d33) " | " (int.to.str e31) " " (int.to.str e32) " " (int.to.str e33) " | " (int.to.str f31) " " (int.to.str f32) " " (int.to.str f33)))
(echo "-------+-------+-------")
(eval (str.++ (int.to.str g11) " " (int.to.str g12) " " (int.to.str g13) " | " (int.to.str h11) " " (int.to.str h12) " " (int.to.str h13) " | " (int.to.str i11) " " (int.to.str i12) " " (int.to.str i13)))
(eval (str.++ (int.to.str g21) " " (int.to.str g22) " " (int.to.str g23) " | " (int.to.str h21) " " (int.to.str h22) " " (int.to.str h23) " | " (int.to.str i21) " " (int.to.str i22) " " (int.to.str i23)))
(eval (str.++ (int.to.str g31) " " (int.to.str g32) " " (int.to.str g33) " | " (int.to.str h31) " " (int.to.str h32) " " (int.to.str h33) " | " (int.to.str i31) " " (int.to.str i32) " " (int.to.str i33)))
(echo "")
(get-model)
sat
Results:
"7 5 1 | 9 4 6 | 8 3 2"
"6 9 3 | 1 2 8 | 7 4 5"
"4 8 2 | 5 7 3 | 1 9 6"
-------+-------+-------
"9 4 5 | 2 8 7 | 6 1 3"
"1 3 8 | 4 6 9 | 2 5 7"
"2 7 6 | 3 5 1 | 9 8 4"
-------+-------+-------
"5 1 4 | 6 9 2 | 3 7 8"
"3 6 7 | 8 1 5 | 4 2 9"
"8 2 9 | 7 3 4 | 5 6 1"
(model
(define-fun c23 () Int
5)
(define-fun b12 () Int
4)
(define-fun h23 () Int
5)
(define-fun c22 () Int
4)
(define-fun g21 () Int
3)
(define-fun c21 () Int
7)
(define-fun f12 () Int
1)
(define-fun i23 () Int
9)
(define-fun d23 () Int
8)
(define-fun a31 () Int
4)
(define-fun a12 () Int
5)
(define-fun a32 () Int
8)
(define-fun b33 () Int
3)
(define-fun d33 () Int
6)
(define-fun g31 () Int
8)
(define-fun g23 () Int
7)
(define-fun i13 () Int
8)
(define-fun b23 () Int
8)
(define-fun i31 () Int
5)
(define-fun c12 () Int
3)
(define-fun a13 () Int
1)
(define-fun e32 () Int
5)
(define-fun f31 () Int
9)
(define-fun c32 () Int
9)
(define-fun d12 () Int
4)
(define-fun g12 () Int
1)
(define-fun h22 () Int
1)
(define-fun h33 () Int
4)
(define-fun i33 () Int
1)
(define-fun e13 () Int
7)
(define-fun b11 () Int
9)
(define-fun g33 () Int
9)
(define-fun a22 () Int
9)
(define-fun a33 () Int
2)
(define-fun h32 () Int
3)
(define-fun b22 () Int
2)
(define-fun h11 () Int
6)
(define-fun i21 () Int
4)
(define-fun d31 () Int
2)
(define-fun b13 () Int
6)
(define-fun e12 () Int
8)
(define-fun e21 () Int
4)
(define-fun f11 () Int
6)
(define-fun h21 () Int
8)
(define-fun i12 () Int
7)
(define-fun b32 () Int
7)
(define-fun i22 () Int
2)
(define-fun d21 () Int
1)
(define-fun d11 () Int
9)
(define-fun d32 () Int
7)
(define-fun b21 () Int
1)
(define-fun f21 () Int
2)
(define-fun e31 () Int
3)
(define-fun f23 () Int
7)
(define-fun g32 () Int
2)
(define-fun a21 () Int
6)
(define-fun d13 () Int
5)
(define-fun h13 () Int
2)
(define-fun i32 () Int
6)
(define-fun c11 () Int
8)
(define-fun a23 () Int
3)
(define-fun c31 () Int
1)
(define-fun f33 () Int
4)
(define-fun e23 () Int
9)
(define-fun f22 () Int
5)
(define-fun h31 () Int
7)
(define-fun d22 () Int
3)
(define-fun c13 () Int
2)
(define-fun e33 () Int
1)
(define-fun g13 () Int
4)
(define-fun h12 () Int
9)
(define-fun c33 () Int
6)
(define-fun b31 () Int
5)
(define-fun e22 () Int
6)
(define-fun f13 () Int
3)
(define-fun g11 () Int
5)
(define-fun a11 () Int
7)
(define-fun f32 () Int
8)
(define-fun e11 () Int
2)
(define-fun g22 () Int
6)
(define-fun i11 () Int
3)
)