通过 Z3 生成随机数独不是随机的，而且很慢
Generating random Sudoku via Z3 isn't random and is slow
我编写了以下 SMT 代码来生成随机数独。更具体地说，它会在给定一个空的 9x9 矩阵的情况下生成一个填充的数独。这是我想出的最简单的示例，可以在 Z3 上试用它以了解它的工作原理。
sudoku.smt:
; 9x9 cells 1 to 9
(declare-const cell_1_1 Int)(assert (<= 1 cell_1_1))(assert (<= cell_1_1 9))
(declare-const cell_1_2 Int)(assert (<= 1 cell_1_2))(assert (<= cell_1_2 9))
(declare-const cell_1_3 Int)(assert (<= 1 cell_1_3))(assert (<= cell_1_3 9))
(declare-const cell_1_4 Int)(assert (<= 1 cell_1_4))(assert (<= cell_1_4 9))
(declare-const cell_1_5 Int)(assert (<= 1 cell_1_5))(assert (<= cell_1_5 9))
(declare-const cell_1_6 Int)(assert (<= 1 cell_1_6))(assert (<= cell_1_6 9))
(declare-const cell_1_7 Int)(assert (<= 1 cell_1_7))(assert (<= cell_1_7 9))
(declare-const cell_1_8 Int)(assert (<= 1 cell_1_8))(assert (<= cell_1_8 9))
(declare-const cell_1_9 Int)(assert (<= 1 cell_1_9))(assert (<= cell_1_9 9))
(declare-const cell_2_1 Int)(assert (<= 1 cell_2_1))(assert (<= cell_2_1 9))
(declare-const cell_2_2 Int)(assert (<= 1 cell_2_2))(assert (<= cell_2_2 9))
(declare-const cell_2_3 Int)(assert (<= 1 cell_2_3))(assert (<= cell_2_3 9))
(declare-const cell_2_4 Int)(assert (<= 1 cell_2_4))(assert (<= cell_2_4 9))
(declare-const cell_2_5 Int)(assert (<= 1 cell_2_5))(assert (<= cell_2_5 9))
(declare-const cell_2_6 Int)(assert (<= 1 cell_2_6))(assert (<= cell_2_6 9))
(declare-const cell_2_7 Int)(assert (<= 1 cell_2_7))(assert (<= cell_2_7 9))
(declare-const cell_2_8 Int)(assert (<= 1 cell_2_8))(assert (<= cell_2_8 9))
(declare-const cell_2_9 Int)(assert (<= 1 cell_2_9))(assert (<= cell_2_9 9))
(declare-const cell_3_1 Int)(assert (<= 1 cell_3_1))(assert (<= cell_3_1 9))
(declare-const cell_3_2 Int)(assert (<= 1 cell_3_2))(assert (<= cell_3_2 9))
(declare-const cell_3_3 Int)(assert (<= 1 cell_3_3))(assert (<= cell_3_3 9))
(declare-const cell_3_4 Int)(assert (<= 1 cell_3_4))(assert (<= cell_3_4 9))
(declare-const cell_3_5 Int)(assert (<= 1 cell_3_5))(assert (<= cell_3_5 9))
(declare-const cell_3_6 Int)(assert (<= 1 cell_3_6))(assert (<= cell_3_6 9))
(declare-const cell_3_7 Int)(assert (<= 1 cell_3_7))(assert (<= cell_3_7 9))
(declare-const cell_3_8 Int)(assert (<= 1 cell_3_8))(assert (<= cell_3_8 9))
(declare-const cell_3_9 Int)(assert (<= 1 cell_3_9))(assert (<= cell_3_9 9))
(declare-const cell_4_1 Int)(assert (<= 1 cell_4_1))(assert (<= cell_4_1 9))
(declare-const cell_4_2 Int)(assert (<= 1 cell_4_2))(assert (<= cell_4_2 9))
(declare-const cell_4_3 Int)(assert (<= 1 cell_4_3))(assert (<= cell_4_3 9))
(declare-const cell_4_4 Int)(assert (<= 1 cell_4_4))(assert (<= cell_4_4 9))
(declare-const cell_4_5 Int)(assert (<= 1 cell_4_5))(assert (<= cell_4_5 9))
(declare-const cell_4_6 Int)(assert (<= 1 cell_4_6))(assert (<= cell_4_6 9))
(declare-const cell_4_7 Int)(assert (<= 1 cell_4_7))(assert (<= cell_4_7 9))
(declare-const cell_4_8 Int)(assert (<= 1 cell_4_8))(assert (<= cell_4_8 9))
(declare-const cell_4_9 Int)(assert (<= 1 cell_4_9))(assert (<= cell_4_9 9))
(declare-const cell_5_1 Int)(assert (<= 1 cell_5_1))(assert (<= cell_5_1 9))
(declare-const cell_5_2 Int)(assert (<= 1 cell_5_2))(assert (<= cell_5_2 9))
(declare-const cell_5_3 Int)(assert (<= 1 cell_5_3))(assert (<= cell_5_3 9))
(declare-const cell_5_4 Int)(assert (<= 1 cell_5_4))(assert (<= cell_5_4 9))
(declare-const cell_5_5 Int)(assert (<= 1 cell_5_5))(assert (<= cell_5_5 9))
(declare-const cell_5_6 Int)(assert (<= 1 cell_5_6))(assert (<= cell_5_6 9))
(declare-const cell_5_7 Int)(assert (<= 1 cell_5_7))(assert (<= cell_5_7 9))
(declare-const cell_5_8 Int)(assert (<= 1 cell_5_8))(assert (<= cell_5_8 9))
(declare-const cell_5_9 Int)(assert (<= 1 cell_5_9))(assert (<= cell_5_9 9))
(declare-const cell_6_1 Int)(assert (<= 1 cell_6_1))(assert (<= cell_6_1 9))
(declare-const cell_6_2 Int)(assert (<= 1 cell_6_2))(assert (<= cell_6_2 9))
(declare-const cell_6_3 Int)(assert (<= 1 cell_6_3))(assert (<= cell_6_3 9))
(declare-const cell_6_4 Int)(assert (<= 1 cell_6_4))(assert (<= cell_6_4 9))
(declare-const cell_6_5 Int)(assert (<= 1 cell_6_5))(assert (<= cell_6_5 9))
(declare-const cell_6_6 Int)(assert (<= 1 cell_6_6))(assert (<= cell_6_6 9))
(declare-const cell_6_7 Int)(assert (<= 1 cell_6_7))(assert (<= cell_6_7 9))
(declare-const cell_6_8 Int)(assert (<= 1 cell_6_8))(assert (<= cell_6_8 9))
(declare-const cell_6_9 Int)(assert (<= 1 cell_6_9))(assert (<= cell_6_9 9))
(declare-const cell_7_1 Int)(assert (<= 1 cell_7_1))(assert (<= cell_7_1 9))
(declare-const cell_7_2 Int)(assert (<= 1 cell_7_2))(assert (<= cell_7_2 9))
(declare-const cell_7_3 Int)(assert (<= 1 cell_7_3))(assert (<= cell_7_3 9))
(declare-const cell_7_4 Int)(assert (<= 1 cell_7_4))(assert (<= cell_7_4 9))
(declare-const cell_7_5 Int)(assert (<= 1 cell_7_5))(assert (<= cell_7_5 9))
(declare-const cell_7_6 Int)(assert (<= 1 cell_7_6))(assert (<= cell_7_6 9))
(declare-const cell_7_7 Int)(assert (<= 1 cell_7_7))(assert (<= cell_7_7 9))
(declare-const cell_7_8 Int)(assert (<= 1 cell_7_8))(assert (<= cell_7_8 9))
(declare-const cell_7_9 Int)(assert (<= 1 cell_7_9))(assert (<= cell_7_9 9))
(declare-const cell_8_1 Int)(assert (<= 1 cell_8_1))(assert (<= cell_8_1 9))
(declare-const cell_8_2 Int)(assert (<= 1 cell_8_2))(assert (<= cell_8_2 9))
(declare-const cell_8_3 Int)(assert (<= 1 cell_8_3))(assert (<= cell_8_3 9))
(declare-const cell_8_4 Int)(assert (<= 1 cell_8_4))(assert (<= cell_8_4 9))
(declare-const cell_8_5 Int)(assert (<= 1 cell_8_5))(assert (<= cell_8_5 9))
(declare-const cell_8_6 Int)(assert (<= 1 cell_8_6))(assert (<= cell_8_6 9))
(declare-const cell_8_7 Int)(assert (<= 1 cell_8_7))(assert (<= cell_8_7 9))
(declare-const cell_8_8 Int)(assert (<= 1 cell_8_8))(assert (<= cell_8_8 9))
(declare-const cell_8_9 Int)(assert (<= 1 cell_8_9))(assert (<= cell_8_9 9))
(declare-const cell_9_1 Int)(assert (<= 1 cell_9_1))(assert (<= cell_9_1 9))
(declare-const cell_9_2 Int)(assert (<= 1 cell_9_2))(assert (<= cell_9_2 9))
(declare-const cell_9_3 Int)(assert (<= 1 cell_9_3))(assert (<= cell_9_3 9))
(declare-const cell_9_4 Int)(assert (<= 1 cell_9_4))(assert (<= cell_9_4 9))
(declare-const cell_9_5 Int)(assert (<= 1 cell_9_5))(assert (<= cell_9_5 9))
(declare-const cell_9_6 Int)(assert (<= 1 cell_9_6))(assert (<= cell_9_6 9))
(declare-const cell_9_7 Int)(assert (<= 1 cell_9_7))(assert (<= cell_9_7 9))
(declare-const cell_9_8 Int)(assert (<= 1 cell_9_8))(assert (<= cell_9_8 9))
(declare-const cell_9_9 Int)(assert (<= 1 cell_9_9))(assert (<= cell_9_9 9))
; distinct values in rows
(assert (distinct cell_1_1 cell_1_2 cell_1_3 cell_1_4 cell_1_5 cell_1_6 cell_1_7 cell_1_8 cell_1_9))
(assert (distinct cell_2_1 cell_2_2 cell_2_3 cell_2_4 cell_2_5 cell_2_6 cell_2_7 cell_2_8 cell_2_9))
(assert (distinct cell_3_1 cell_3_2 cell_3_3 cell_3_4 cell_3_5 cell_3_6 cell_3_7 cell_3_8 cell_3_9))
(assert (distinct cell_4_1 cell_4_2 cell_4_3 cell_4_4 cell_4_5 cell_4_6 cell_4_7 cell_4_8 cell_4_9))
(assert (distinct cell_5_1 cell_5_2 cell_5_3 cell_5_4 cell_5_5 cell_5_6 cell_5_7 cell_5_8 cell_5_9))
(assert (distinct cell_6_1 cell_6_2 cell_6_3 cell_6_4 cell_6_5 cell_6_6 cell_6_7 cell_6_8 cell_6_9))
(assert (distinct cell_7_1 cell_7_2 cell_7_3 cell_7_4 cell_7_5 cell_7_6 cell_7_7 cell_7_8 cell_7_9))
(assert (distinct cell_8_1 cell_8_2 cell_8_3 cell_8_4 cell_8_5 cell_8_6 cell_8_7 cell_8_8 cell_8_9))
(assert (distinct cell_9_1 cell_9_2 cell_9_3 cell_9_4 cell_9_5 cell_9_6 cell_9_7 cell_9_8 cell_9_9))
; distinct values in cells
(assert (distinct cell_1_1 cell_2_1 cell_3_1 cell_4_1 cell_5_1 cell_6_1 cell_7_1 cell_8_1 cell_9_1))
(assert (distinct cell_1_2 cell_2_2 cell_3_2 cell_4_2 cell_5_2 cell_6_2 cell_7_2 cell_8_2 cell_9_2))
(assert (distinct cell_1_3 cell_2_3 cell_3_3 cell_4_3 cell_5_3 cell_6_3 cell_7_3 cell_8_3 cell_9_3))
(assert (distinct cell_1_4 cell_2_4 cell_3_4 cell_4_4 cell_5_4 cell_6_4 cell_7_4 cell_8_4 cell_9_4))
(assert (distinct cell_1_5 cell_2_5 cell_3_5 cell_4_5 cell_5_5 cell_6_5 cell_7_5 cell_8_5 cell_9_5))
(assert (distinct cell_1_6 cell_2_6 cell_3_6 cell_4_6 cell_5_6 cell_6_6 cell_7_6 cell_8_6 cell_9_6))
(assert (distinct cell_1_7 cell_2_7 cell_3_7 cell_4_7 cell_5_7 cell_6_7 cell_7_7 cell_8_7 cell_9_7))
(assert (distinct cell_1_8 cell_2_8 cell_3_8 cell_4_8 cell_5_8 cell_6_8 cell_7_8 cell_8_8 cell_9_8))
(assert (distinct cell_1_9 cell_2_9 cell_3_9 cell_4_9 cell_5_9 cell_6_9 cell_7_9 cell_8_9 cell_9_9))
; distinct values in squares
(assert (distinct cell_1_1 cell_1_2 cell_1_3 cell_2_1 cell_2_2 cell_2_3 cell_3_1 cell_3_2 cell_3_3))
(assert (distinct cell_1_4 cell_1_5 cell_1_6 cell_2_4 cell_2_5 cell_2_6 cell_3_4 cell_3_5 cell_3_6))
(assert (distinct cell_1_7 cell_1_8 cell_1_9 cell_2_7 cell_2_8 cell_2_9 cell_3_7 cell_3_8 cell_3_9))
(assert (distinct cell_4_1 cell_4_2 cell_4_3 cell_5_1 cell_5_2 cell_5_3 cell_6_1 cell_6_2 cell_6_3))
(assert (distinct cell_4_4 cell_4_5 cell_4_6 cell_5_4 cell_5_5 cell_5_6 cell_6_4 cell_6_5 cell_6_6))
(assert (distinct cell_4_7 cell_4_8 cell_4_9 cell_5_7 cell_5_8 cell_5_9 cell_6_7 cell_6_8 cell_6_9))
(assert (distinct cell_7_1 cell_7_2 cell_7_3 cell_8_1 cell_8_2 cell_8_3 cell_9_1 cell_9_2 cell_9_3))
(assert (distinct cell_7_4 cell_7_5 cell_7_6 cell_8_4 cell_8_5 cell_8_6 cell_9_4 cell_9_5 cell_9_6))
(assert (distinct cell_7_7 cell_7_8 cell_7_9 cell_8_7 cell_8_8 cell_8_9 cell_9_7 cell_9_8 cell_9_9))
; generate one for me, please
(check-sat)
(get-model)
我通过以下方式执行它：
z3 sudoku.smt
结果，我得到了一个生成的数独：
(model
(define-fun cell_2_9 () Int
8)
(define-fun cell_3_9 () Int
9)
(define-fun cell_7_6 () Int
7)
(define-fun cell_7_7 () Int
1)
(define-fun cell_7_4 () Int
5)
(define-fun cell_5_3 () Int
1)
(define-fun cell_3_7 () Int
2)
(define-fun cell_9_7 () Int
9)
(define-fun cell_1_8 () Int
3)
(define-fun cell_4_4 () Int
8)
(define-fun cell_9_4 () Int
1)
(define-fun cell_2_1 () Int
9)
(define-fun cell_2_2 () Int
1)
(define-fun cell_4_1 () Int
6)
(define-fun cell_5_5 () Int
3)
(define-fun cell_1_2 () Int
6)
(define-fun cell_3_5 () Int
1)
(define-fun cell_1_3 () Int
4)
(define-fun cell_1_4 () Int
7)
(define-fun cell_9_8 () Int
7)
(define-fun cell_8_8 () Int
8)
(define-fun cell_3_3 () Int
5)
(define-fun cell_2_3 () Int
2)
(define-fun cell_6_8 () Int
9)
(define-fun cell_7_3 () Int
6)
(define-fun cell_9_1 () Int
2)
(define-fun cell_5_7 () Int
8)
(define-fun cell_5_9 () Int
4)
(define-fun cell_3_4 () Int
6)
(define-fun cell_6_7 () Int
6)
(define-fun cell_2_5 () Int
5)
(define-fun cell_6_2 () Int
3)
(define-fun cell_8_2 () Int
9)
(define-fun cell_6_4 () Int
2)
(define-fun cell_2_4 () Int
4)
(define-fun cell_2_7 () Int
7)
(define-fun cell_4_5 () Int
7)
(define-fun cell_3_2 () Int
7)
(define-fun cell_4_9 () Int
2)
(define-fun cell_9_2 () Int
5)
(define-fun cell_6_9 () Int
7)
(define-fun cell_1_9 () Int
1)
(define-fun cell_7_5 () Int
9)
(define-fun cell_9_5 () Int
8)
(define-fun cell_9_3 () Int
3)
(define-fun cell_8_7 () Int
4)
(define-fun cell_5_1 () Int
7)
(define-fun cell_4_7 () Int
3)
(define-fun cell_3_8 () Int
4)
(define-fun cell_9_9 () Int
6)
(define-fun cell_8_1 () Int
1)
(define-fun cell_4_2 () Int
4)
(define-fun cell_4_3 () Int
9)
(define-fun cell_7_2 () Int
8)
(define-fun cell_8_9 () Int
5)
(define-fun cell_1_5 () Int
2)
(define-fun cell_1_1 () Int
8)
(define-fun cell_2_6 () Int
3)
(define-fun cell_6_6 () Int
1)
(define-fun cell_5_8 () Int
5)
(define-fun cell_5_4 () Int
9)
(define-fun cell_9_6 () Int
4)
(define-fun cell_6_1 () Int
5)
(define-fun cell_3_6 () Int
8)
(define-fun cell_6_3 () Int
8)
(define-fun cell_8_6 () Int
2)
(define-fun cell_7_9 () Int
3)
(define-fun cell_5_2 () Int
2)
(define-fun cell_4_6 () Int
5)
(define-fun cell_7_1 () Int
4)
(define-fun cell_8_4 () Int
3)
(define-fun cell_4_8 () Int
1)
(define-fun cell_1_7 () Int
5)
(define-fun cell_6_5 () Int
4)
(define-fun cell_7_8 () Int
2)
(define-fun cell_1_6 () Int
9)
(define-fun cell_2_8 () Int
6)
(define-fun cell_8_3 () Int
7)
(define-fun cell_3_1 () Int
3)
(define-fun cell_8_5 () Int
6)
(define-fun cell_5_6 () Int
6)
)
但是，我有两个问题：
- 完成需要很长时间，在我的机器上大约需要 25 秒。
- 每次我 运行 它都会生成相同的数独。
这让我想知道我做错了什么。我期望的是每次都不同的非常快的结果。我怎样才能做到这一点？
老实说，关于 Z3 的文档资源让我有些吃力。我正在尝试遵循 https://rise4fun.com/Z3/tutorial/guide，但所有内容的解释都非常简短，而且我找不到任何详细的手册。所以欢迎任何 resources/recommendations/links。谢谢。
Int 是为这个问题选择的错误域。相反，请改用位向量。也就是说，将您的声明替换为：
(declare-const cell_1_1 (_ BitVec 4))
(assert (bvule #x1 cell_1_1))
(assert (bvule cell_1_1 #x9))
对所有变量进行此更改后，您会发现 z3 可以更快地解决问题。 （在我的测试中，几乎是瞬间。）
关于随机性：您可以使用随机种子设置，但 SMT 求解器不太可能为您生成不同的解决方案；它们是为解决约束而调整的，而不是以任何有意义的方式（随机或其他方式）探索可能的搜索 space。一个实用的解决方案是随机生成一些单元格值（使用其他程序）和 hard-对它们进行编码：也就是说，断言 cell_3_4 是 5，而其他一些单元格是 9 等。只要你随机断言其中的一些（~10 左右），你应该得到好的数独实例。 （当然除非变成unsat。）
在进一步研究了 z3 策略之后，我想出了一个可能比@alias 的答案更好的解决方案（无论如何谢谢你的答案，它引导我朝着正确的方向前进）。
性能
不在我的代码中使用 (check-sat)，而是可以使用 (check-sat-using ...) 并进一步指定要应用的策略。
默认策略是smt，这对我来说很慢。研究了(help-tactics)的帮助，发现有一个nla2bv的战术可以使用
引自(help-tactics)：
nla2bv converts a nonlinear arithmetic problem into a bit-vector problem, in most cases, the resultant goal is an under approximation and is useful for finding models.
在代码中，这意味着：
(check-sat-using (then nla2bv smt))
随机性
关于随机性，可以通过 :random-seed 参数为 smt 策略提供随机种子。如果我提供不同的种子，我会得到不同的输出模型。
在代码中，这看起来像：
(check-sat-using (then nla2bv (using-params smt :random-seed 999)))
虽然，正如@alias 在回答中指出的那样，这只提供了非常有限的选项来控制输出。
进行这些更改后，我可以将大约 25 秒缩短到不到 1 秒。为了获得更多性能提升，我相信可以进一步调整使用的策略。
我编写了以下 SMT 代码来生成随机数独。更具体地说，它会在给定一个空的 9x9 矩阵的情况下生成一个填充的数独。这是我想出的最简单的示例，可以在 Z3 上试用它以了解它的工作原理。
sudoku.smt:
; 9x9 cells 1 to 9
(declare-const cell_1_1 Int)(assert (<= 1 cell_1_1))(assert (<= cell_1_1 9))
(declare-const cell_1_2 Int)(assert (<= 1 cell_1_2))(assert (<= cell_1_2 9))
(declare-const cell_1_3 Int)(assert (<= 1 cell_1_3))(assert (<= cell_1_3 9))
(declare-const cell_1_4 Int)(assert (<= 1 cell_1_4))(assert (<= cell_1_4 9))
(declare-const cell_1_5 Int)(assert (<= 1 cell_1_5))(assert (<= cell_1_5 9))
(declare-const cell_1_6 Int)(assert (<= 1 cell_1_6))(assert (<= cell_1_6 9))
(declare-const cell_1_7 Int)(assert (<= 1 cell_1_7))(assert (<= cell_1_7 9))
(declare-const cell_1_8 Int)(assert (<= 1 cell_1_8))(assert (<= cell_1_8 9))
(declare-const cell_1_9 Int)(assert (<= 1 cell_1_9))(assert (<= cell_1_9 9))
(declare-const cell_2_1 Int)(assert (<= 1 cell_2_1))(assert (<= cell_2_1 9))
(declare-const cell_2_2 Int)(assert (<= 1 cell_2_2))(assert (<= cell_2_2 9))
(declare-const cell_2_3 Int)(assert (<= 1 cell_2_3))(assert (<= cell_2_3 9))
(declare-const cell_2_4 Int)(assert (<= 1 cell_2_4))(assert (<= cell_2_4 9))
(declare-const cell_2_5 Int)(assert (<= 1 cell_2_5))(assert (<= cell_2_5 9))
(declare-const cell_2_6 Int)(assert (<= 1 cell_2_6))(assert (<= cell_2_6 9))
(declare-const cell_2_7 Int)(assert (<= 1 cell_2_7))(assert (<= cell_2_7 9))
(declare-const cell_2_8 Int)(assert (<= 1 cell_2_8))(assert (<= cell_2_8 9))
(declare-const cell_2_9 Int)(assert (<= 1 cell_2_9))(assert (<= cell_2_9 9))
(declare-const cell_3_1 Int)(assert (<= 1 cell_3_1))(assert (<= cell_3_1 9))
(declare-const cell_3_2 Int)(assert (<= 1 cell_3_2))(assert (<= cell_3_2 9))
(declare-const cell_3_3 Int)(assert (<= 1 cell_3_3))(assert (<= cell_3_3 9))
(declare-const cell_3_4 Int)(assert (<= 1 cell_3_4))(assert (<= cell_3_4 9))
(declare-const cell_3_5 Int)(assert (<= 1 cell_3_5))(assert (<= cell_3_5 9))
(declare-const cell_3_6 Int)(assert (<= 1 cell_3_6))(assert (<= cell_3_6 9))
(declare-const cell_3_7 Int)(assert (<= 1 cell_3_7))(assert (<= cell_3_7 9))
(declare-const cell_3_8 Int)(assert (<= 1 cell_3_8))(assert (<= cell_3_8 9))
(declare-const cell_3_9 Int)(assert (<= 1 cell_3_9))(assert (<= cell_3_9 9))
(declare-const cell_4_1 Int)(assert (<= 1 cell_4_1))(assert (<= cell_4_1 9))
(declare-const cell_4_2 Int)(assert (<= 1 cell_4_2))(assert (<= cell_4_2 9))
(declare-const cell_4_3 Int)(assert (<= 1 cell_4_3))(assert (<= cell_4_3 9))
(declare-const cell_4_4 Int)(assert (<= 1 cell_4_4))(assert (<= cell_4_4 9))
(declare-const cell_4_5 Int)(assert (<= 1 cell_4_5))(assert (<= cell_4_5 9))
(declare-const cell_4_6 Int)(assert (<= 1 cell_4_6))(assert (<= cell_4_6 9))
(declare-const cell_4_7 Int)(assert (<= 1 cell_4_7))(assert (<= cell_4_7 9))
(declare-const cell_4_8 Int)(assert (<= 1 cell_4_8))(assert (<= cell_4_8 9))
(declare-const cell_4_9 Int)(assert (<= 1 cell_4_9))(assert (<= cell_4_9 9))
(declare-const cell_5_1 Int)(assert (<= 1 cell_5_1))(assert (<= cell_5_1 9))
(declare-const cell_5_2 Int)(assert (<= 1 cell_5_2))(assert (<= cell_5_2 9))
(declare-const cell_5_3 Int)(assert (<= 1 cell_5_3))(assert (<= cell_5_3 9))
(declare-const cell_5_4 Int)(assert (<= 1 cell_5_4))(assert (<= cell_5_4 9))
(declare-const cell_5_5 Int)(assert (<= 1 cell_5_5))(assert (<= cell_5_5 9))
(declare-const cell_5_6 Int)(assert (<= 1 cell_5_6))(assert (<= cell_5_6 9))
(declare-const cell_5_7 Int)(assert (<= 1 cell_5_7))(assert (<= cell_5_7 9))
(declare-const cell_5_8 Int)(assert (<= 1 cell_5_8))(assert (<= cell_5_8 9))
(declare-const cell_5_9 Int)(assert (<= 1 cell_5_9))(assert (<= cell_5_9 9))
(declare-const cell_6_1 Int)(assert (<= 1 cell_6_1))(assert (<= cell_6_1 9))
(declare-const cell_6_2 Int)(assert (<= 1 cell_6_2))(assert (<= cell_6_2 9))
(declare-const cell_6_3 Int)(assert (<= 1 cell_6_3))(assert (<= cell_6_3 9))
(declare-const cell_6_4 Int)(assert (<= 1 cell_6_4))(assert (<= cell_6_4 9))
(declare-const cell_6_5 Int)(assert (<= 1 cell_6_5))(assert (<= cell_6_5 9))
(declare-const cell_6_6 Int)(assert (<= 1 cell_6_6))(assert (<= cell_6_6 9))
(declare-const cell_6_7 Int)(assert (<= 1 cell_6_7))(assert (<= cell_6_7 9))
(declare-const cell_6_8 Int)(assert (<= 1 cell_6_8))(assert (<= cell_6_8 9))
(declare-const cell_6_9 Int)(assert (<= 1 cell_6_9))(assert (<= cell_6_9 9))
(declare-const cell_7_1 Int)(assert (<= 1 cell_7_1))(assert (<= cell_7_1 9))
(declare-const cell_7_2 Int)(assert (<= 1 cell_7_2))(assert (<= cell_7_2 9))
(declare-const cell_7_3 Int)(assert (<= 1 cell_7_3))(assert (<= cell_7_3 9))
(declare-const cell_7_4 Int)(assert (<= 1 cell_7_4))(assert (<= cell_7_4 9))
(declare-const cell_7_5 Int)(assert (<= 1 cell_7_5))(assert (<= cell_7_5 9))
(declare-const cell_7_6 Int)(assert (<= 1 cell_7_6))(assert (<= cell_7_6 9))
(declare-const cell_7_7 Int)(assert (<= 1 cell_7_7))(assert (<= cell_7_7 9))
(declare-const cell_7_8 Int)(assert (<= 1 cell_7_8))(assert (<= cell_7_8 9))
(declare-const cell_7_9 Int)(assert (<= 1 cell_7_9))(assert (<= cell_7_9 9))
(declare-const cell_8_1 Int)(assert (<= 1 cell_8_1))(assert (<= cell_8_1 9))
(declare-const cell_8_2 Int)(assert (<= 1 cell_8_2))(assert (<= cell_8_2 9))
(declare-const cell_8_3 Int)(assert (<= 1 cell_8_3))(assert (<= cell_8_3 9))
(declare-const cell_8_4 Int)(assert (<= 1 cell_8_4))(assert (<= cell_8_4 9))
(declare-const cell_8_5 Int)(assert (<= 1 cell_8_5))(assert (<= cell_8_5 9))
(declare-const cell_8_6 Int)(assert (<= 1 cell_8_6))(assert (<= cell_8_6 9))
(declare-const cell_8_7 Int)(assert (<= 1 cell_8_7))(assert (<= cell_8_7 9))
(declare-const cell_8_8 Int)(assert (<= 1 cell_8_8))(assert (<= cell_8_8 9))
(declare-const cell_8_9 Int)(assert (<= 1 cell_8_9))(assert (<= cell_8_9 9))
(declare-const cell_9_1 Int)(assert (<= 1 cell_9_1))(assert (<= cell_9_1 9))
(declare-const cell_9_2 Int)(assert (<= 1 cell_9_2))(assert (<= cell_9_2 9))
(declare-const cell_9_3 Int)(assert (<= 1 cell_9_3))(assert (<= cell_9_3 9))
(declare-const cell_9_4 Int)(assert (<= 1 cell_9_4))(assert (<= cell_9_4 9))
(declare-const cell_9_5 Int)(assert (<= 1 cell_9_5))(assert (<= cell_9_5 9))
(declare-const cell_9_6 Int)(assert (<= 1 cell_9_6))(assert (<= cell_9_6 9))
(declare-const cell_9_7 Int)(assert (<= 1 cell_9_7))(assert (<= cell_9_7 9))
(declare-const cell_9_8 Int)(assert (<= 1 cell_9_8))(assert (<= cell_9_8 9))
(declare-const cell_9_9 Int)(assert (<= 1 cell_9_9))(assert (<= cell_9_9 9))
; distinct values in rows
(assert (distinct cell_1_1 cell_1_2 cell_1_3 cell_1_4 cell_1_5 cell_1_6 cell_1_7 cell_1_8 cell_1_9))
(assert (distinct cell_2_1 cell_2_2 cell_2_3 cell_2_4 cell_2_5 cell_2_6 cell_2_7 cell_2_8 cell_2_9))
(assert (distinct cell_3_1 cell_3_2 cell_3_3 cell_3_4 cell_3_5 cell_3_6 cell_3_7 cell_3_8 cell_3_9))
(assert (distinct cell_4_1 cell_4_2 cell_4_3 cell_4_4 cell_4_5 cell_4_6 cell_4_7 cell_4_8 cell_4_9))
(assert (distinct cell_5_1 cell_5_2 cell_5_3 cell_5_4 cell_5_5 cell_5_6 cell_5_7 cell_5_8 cell_5_9))
(assert (distinct cell_6_1 cell_6_2 cell_6_3 cell_6_4 cell_6_5 cell_6_6 cell_6_7 cell_6_8 cell_6_9))
(assert (distinct cell_7_1 cell_7_2 cell_7_3 cell_7_4 cell_7_5 cell_7_6 cell_7_7 cell_7_8 cell_7_9))
(assert (distinct cell_8_1 cell_8_2 cell_8_3 cell_8_4 cell_8_5 cell_8_6 cell_8_7 cell_8_8 cell_8_9))
(assert (distinct cell_9_1 cell_9_2 cell_9_3 cell_9_4 cell_9_5 cell_9_6 cell_9_7 cell_9_8 cell_9_9))
; distinct values in cells
(assert (distinct cell_1_1 cell_2_1 cell_3_1 cell_4_1 cell_5_1 cell_6_1 cell_7_1 cell_8_1 cell_9_1))
(assert (distinct cell_1_2 cell_2_2 cell_3_2 cell_4_2 cell_5_2 cell_6_2 cell_7_2 cell_8_2 cell_9_2))
(assert (distinct cell_1_3 cell_2_3 cell_3_3 cell_4_3 cell_5_3 cell_6_3 cell_7_3 cell_8_3 cell_9_3))
(assert (distinct cell_1_4 cell_2_4 cell_3_4 cell_4_4 cell_5_4 cell_6_4 cell_7_4 cell_8_4 cell_9_4))
(assert (distinct cell_1_5 cell_2_5 cell_3_5 cell_4_5 cell_5_5 cell_6_5 cell_7_5 cell_8_5 cell_9_5))
(assert (distinct cell_1_6 cell_2_6 cell_3_6 cell_4_6 cell_5_6 cell_6_6 cell_7_6 cell_8_6 cell_9_6))
(assert (distinct cell_1_7 cell_2_7 cell_3_7 cell_4_7 cell_5_7 cell_6_7 cell_7_7 cell_8_7 cell_9_7))
(assert (distinct cell_1_8 cell_2_8 cell_3_8 cell_4_8 cell_5_8 cell_6_8 cell_7_8 cell_8_8 cell_9_8))
(assert (distinct cell_1_9 cell_2_9 cell_3_9 cell_4_9 cell_5_9 cell_6_9 cell_7_9 cell_8_9 cell_9_9))
; distinct values in squares
(assert (distinct cell_1_1 cell_1_2 cell_1_3 cell_2_1 cell_2_2 cell_2_3 cell_3_1 cell_3_2 cell_3_3))
(assert (distinct cell_1_4 cell_1_5 cell_1_6 cell_2_4 cell_2_5 cell_2_6 cell_3_4 cell_3_5 cell_3_6))
(assert (distinct cell_1_7 cell_1_8 cell_1_9 cell_2_7 cell_2_8 cell_2_9 cell_3_7 cell_3_8 cell_3_9))
(assert (distinct cell_4_1 cell_4_2 cell_4_3 cell_5_1 cell_5_2 cell_5_3 cell_6_1 cell_6_2 cell_6_3))
(assert (distinct cell_4_4 cell_4_5 cell_4_6 cell_5_4 cell_5_5 cell_5_6 cell_6_4 cell_6_5 cell_6_6))
(assert (distinct cell_4_7 cell_4_8 cell_4_9 cell_5_7 cell_5_8 cell_5_9 cell_6_7 cell_6_8 cell_6_9))
(assert (distinct cell_7_1 cell_7_2 cell_7_3 cell_8_1 cell_8_2 cell_8_3 cell_9_1 cell_9_2 cell_9_3))
(assert (distinct cell_7_4 cell_7_5 cell_7_6 cell_8_4 cell_8_5 cell_8_6 cell_9_4 cell_9_5 cell_9_6))
(assert (distinct cell_7_7 cell_7_8 cell_7_9 cell_8_7 cell_8_8 cell_8_9 cell_9_7 cell_9_8 cell_9_9))
; generate one for me, please
(check-sat)
(get-model)
我通过以下方式执行它：
z3 sudoku.smt
结果，我得到了一个生成的数独：
(model
(define-fun cell_2_9 () Int
8)
(define-fun cell_3_9 () Int
9)
(define-fun cell_7_6 () Int
7)
(define-fun cell_7_7 () Int
1)
(define-fun cell_7_4 () Int
5)
(define-fun cell_5_3 () Int
1)
(define-fun cell_3_7 () Int
2)
(define-fun cell_9_7 () Int
9)
(define-fun cell_1_8 () Int
3)
(define-fun cell_4_4 () Int
8)
(define-fun cell_9_4 () Int
1)
(define-fun cell_2_1 () Int
9)
(define-fun cell_2_2 () Int
1)
(define-fun cell_4_1 () Int
6)
(define-fun cell_5_5 () Int
3)
(define-fun cell_1_2 () Int
6)
(define-fun cell_3_5 () Int
1)
(define-fun cell_1_3 () Int
4)
(define-fun cell_1_4 () Int
7)
(define-fun cell_9_8 () Int
7)
(define-fun cell_8_8 () Int
8)
(define-fun cell_3_3 () Int
5)
(define-fun cell_2_3 () Int
2)
(define-fun cell_6_8 () Int
9)
(define-fun cell_7_3 () Int
6)
(define-fun cell_9_1 () Int
2)
(define-fun cell_5_7 () Int
8)
(define-fun cell_5_9 () Int
4)
(define-fun cell_3_4 () Int
6)
(define-fun cell_6_7 () Int
6)
(define-fun cell_2_5 () Int
5)
(define-fun cell_6_2 () Int
3)
(define-fun cell_8_2 () Int
9)
(define-fun cell_6_4 () Int
2)
(define-fun cell_2_4 () Int
4)
(define-fun cell_2_7 () Int
7)
(define-fun cell_4_5 () Int
7)
(define-fun cell_3_2 () Int
7)
(define-fun cell_4_9 () Int
2)
(define-fun cell_9_2 () Int
5)
(define-fun cell_6_9 () Int
7)
(define-fun cell_1_9 () Int
1)
(define-fun cell_7_5 () Int
9)
(define-fun cell_9_5 () Int
8)
(define-fun cell_9_3 () Int
3)
(define-fun cell_8_7 () Int
4)
(define-fun cell_5_1 () Int
7)
(define-fun cell_4_7 () Int
3)
(define-fun cell_3_8 () Int
4)
(define-fun cell_9_9 () Int
6)
(define-fun cell_8_1 () Int
1)
(define-fun cell_4_2 () Int
4)
(define-fun cell_4_3 () Int
9)
(define-fun cell_7_2 () Int
8)
(define-fun cell_8_9 () Int
5)
(define-fun cell_1_5 () Int
2)
(define-fun cell_1_1 () Int
8)
(define-fun cell_2_6 () Int
3)
(define-fun cell_6_6 () Int
1)
(define-fun cell_5_8 () Int
5)
(define-fun cell_5_4 () Int
9)
(define-fun cell_9_6 () Int
4)
(define-fun cell_6_1 () Int
5)
(define-fun cell_3_6 () Int
8)
(define-fun cell_6_3 () Int
8)
(define-fun cell_8_6 () Int
2)
(define-fun cell_7_9 () Int
3)
(define-fun cell_5_2 () Int
2)
(define-fun cell_4_6 () Int
5)
(define-fun cell_7_1 () Int
4)
(define-fun cell_8_4 () Int
3)
(define-fun cell_4_8 () Int
1)
(define-fun cell_1_7 () Int
5)
(define-fun cell_6_5 () Int
4)
(define-fun cell_7_8 () Int
2)
(define-fun cell_1_6 () Int
9)
(define-fun cell_2_8 () Int
6)
(define-fun cell_8_3 () Int
7)
(define-fun cell_3_1 () Int
3)
(define-fun cell_8_5 () Int
6)
(define-fun cell_5_6 () Int
6)
)
但是，我有两个问题：
- 完成需要很长时间，在我的机器上大约需要 25 秒。
- 每次我 运行 它都会生成相同的数独。
这让我想知道我做错了什么。我期望的是每次都不同的非常快的结果。我怎样才能做到这一点？
老实说，关于 Z3 的文档资源让我有些吃力。我正在尝试遵循 https://rise4fun.com/Z3/tutorial/guide，但所有内容的解释都非常简短，而且我找不到任何详细的手册。所以欢迎任何 resources/recommendations/links。谢谢。
Int 是为这个问题选择的错误域。相反，请改用位向量。也就是说，将您的声明替换为：
(declare-const cell_1_1 (_ BitVec 4))
(assert (bvule #x1 cell_1_1))
(assert (bvule cell_1_1 #x9))
对所有变量进行此更改后，您会发现 z3 可以更快地解决问题。 （在我的测试中，几乎是瞬间。）
关于随机性：您可以使用随机种子设置，但 SMT 求解器不太可能为您生成不同的解决方案；它们是为解决约束而调整的，而不是以任何有意义的方式（随机或其他方式）探索可能的搜索 space。一个实用的解决方案是随机生成一些单元格值（使用其他程序）和 hard-对它们进行编码：也就是说，断言 cell_3_4 是 5，而其他一些单元格是 9 等。只要你随机断言其中的一些（~10 左右），你应该得到好的数独实例。 （当然除非变成unsat。）
在进一步研究了 z3 策略之后，我想出了一个可能比@alias 的答案更好的解决方案（无论如何谢谢你的答案，它引导我朝着正确的方向前进）。
性能
不在我的代码中使用 (check-sat)，而是可以使用 (check-sat-using ...) 并进一步指定要应用的策略。
默认策略是smt，这对我来说很慢。研究了(help-tactics)的帮助，发现有一个nla2bv的战术可以使用
引自(help-tactics)：
nla2bv converts a nonlinear arithmetic problem into a bit-vector problem, in most cases, the resultant goal is an under approximation and is useful for finding models.
在代码中，这意味着：
(check-sat-using (then nla2bv smt))
随机性
关于随机性，可以通过 :random-seed 参数为 smt 策略提供随机种子。如果我提供不同的种子，我会得到不同的输出模型。
在代码中，这看起来像：
(check-sat-using (then nla2bv (using-params smt :random-seed 999)))
虽然，正如@alias 在回答中指出的那样，这只提供了非常有限的选项来控制输出。
进行这些更改后，我可以将大约 25 秒缩短到不到 1 秒。为了获得更多性能提升，我相信可以进一步调整使用的策略。