我怎样才能最好地解决这个优化问题？
How can I best tackle this optimization problem?
上下文
作为了解更多关于 SMT 求解和优化的方法，我正在尝试使用 Z3 解决一个具体问题。我已经成功地模拟了这个问题（它编译并 运行s），但我认为我可能做错了什么，因为即使在小实例中也需要几秒钟来解决，而在现实场景中需要几分钟。我觉得我一定是错过了什么。
我的问题是：
- 这个问题花那么多时间解决正常吗？我以前没有经验，所以也许就是这样。
- Z3 是完成这项工作的正确工具吗？如果没有，您还会推荐我尝试什么？
优化问题的描述
假设您正在组织一个烹饪工作坊。有 i 名教师、j 名学生和 k 项实际作业。对于每个实际作业，学生需要分成 i 组，这样他们就可以在老师的监督下完成作业。还有两个附加要求：
- 每个老师必须至少教每个学生一次
- 我们希望最大化在作业期间相互了解的学生数量（即至少在一项作业中合作的学生对数）
例如，有 2 名教师、6 名学生和 2 项实验作业，您可以得到以下划分：
作业 1：
- 老师1：学生1、学生2、学生3
- 老师2：学生4、学生5、学生6
作业 2：
- 老师1：学生4、学生5、学生6
- 老师2：学生1、学生2、学生3
在这里，每一位老师都教过每一位学生。然而，这必然意味着相互了解的学生数量很少。事实上，作业 1 和作业 2 之间的小组并没有发生变化，只有老师发生了变化。
向Z3说明问题
我编写了一个程序来生成一堆 SMT-LIB 语句，然后将其输入 Z3。对于前面有6个学生，2个老师和2个作业的例子，我们得到如下代码（如果你愿意也可以查看here）：
定义一个辅助函数来将布尔值转换为整数：
(define-fun bool2int ((x Bool)) Int (ite x 1 0))
以 s{x}_a{y}_t{z} 形式声明常量，指示学生 x 是否正在与老师 z 一起做作业 y:
(declare-const s1_a1_t1 Bool)
(declare-const s1_a1_t2 Bool)
(declare-const s1_a2_t1 Bool)
(declare-const s1_a2_t2 Bool)
(declare-const s2_a1_t1 Bool)
(declare-const s2_a1_t2 Bool)
(declare-const s2_a2_t1 Bool)
(declare-const s2_a2_t2 Bool)
(declare-const s3_a1_t1 Bool)
(declare-const s3_a1_t2 Bool)
(declare-const s3_a2_t1 Bool)
(declare-const s3_a2_t2 Bool)
(declare-const s4_a1_t1 Bool)
(declare-const s4_a1_t2 Bool)
(declare-const s4_a2_t1 Bool)
(declare-const s4_a2_t2 Bool)
(declare-const s5_a1_t1 Bool)
(declare-const s5_a1_t2 Bool)
(declare-const s5_a2_t1 Bool)
(declare-const s5_a2_t2 Bool)
(declare-const s6_a1_t1 Bool)
(declare-const s6_a1_t2 Bool)
(declare-const s6_a2_t1 Bool)
(declare-const s6_a2_t2 Bool)
声明约束以确保对于每项作业，学生都应该在一位老师的监督下完成：
(assert (= 1 (+ (bool2int s1_a1_t1) (bool2int s1_a1_t2) )))
(assert (= 1 (+ (bool2int s1_a2_t1) (bool2int s1_a2_t2) )))
(assert (= 1 (+ (bool2int s2_a1_t1) (bool2int s2_a1_t2) )))
(assert (= 1 (+ (bool2int s2_a2_t1) (bool2int s2_a2_t2) )))
(assert (= 1 (+ (bool2int s3_a1_t1) (bool2int s3_a1_t2) )))
(assert (= 1 (+ (bool2int s3_a2_t1) (bool2int s3_a2_t2) )))
(assert (= 1 (+ (bool2int s4_a1_t1) (bool2int s4_a1_t2) )))
(assert (= 1 (+ (bool2int s4_a2_t1) (bool2int s4_a2_t2) )))
(assert (= 1 (+ (bool2int s5_a1_t1) (bool2int s5_a1_t2) )))
(assert (= 1 (+ (bool2int s5_a2_t1) (bool2int s5_a2_t2) )))
(assert (= 1 (+ (bool2int s6_a1_t1) (bool2int s6_a1_t2) )))
(assert (= 1 (+ (bool2int s6_a2_t1) (bool2int s6_a2_t2) )))
声明约束以确保每位教师必须至少教每位学生一次：
(assert (or s1_a1_t1 s1_a2_t1 ))
(assert (or s2_a1_t1 s2_a2_t1 ))
(assert (or s3_a1_t1 s3_a2_t1 ))
(assert (or s4_a1_t1 s4_a2_t1 ))
(assert (or s5_a1_t1 s5_a2_t1 ))
(assert (or s6_a1_t1 s6_a2_t1 ))
(assert (or s1_a1_t2 s1_a2_t2 ))
(assert (or s2_a1_t2 s2_a2_t2 ))
(assert (or s3_a1_t2 s3_a2_t2 ))
(assert (or s4_a1_t2 s4_a2_t2 ))
(assert (or s5_a1_t2 s5_a2_t2 ))
(assert (or s6_a1_t2 s6_a2_t2 ))
声明约束以确保对于每项作业，一位教师必须恰好教授 3 名学生。我们将 >= 与 <= 结合使用，因为该问题的某些实例允许最小和最大学生数量（即当 j % i != 0 时）。
(define-fun t1_a1 () Int (+ (bool2int s1_a1_t1) (bool2int s2_a1_t1) (bool2int s3_a1_t1) (bool2int s4_a1_t1) (bool2int s5_a1_t1) (bool2int s6_a1_t1) ))
(assert (>= 3 t1_a1))
(assert (<= 3 t1_a1))
(define-fun t1_a2 () Int (+ (bool2int s1_a2_t1) (bool2int s2_a2_t1) (bool2int s3_a2_t1) (bool2int s4_a2_t1) (bool2int s5_a2_t1) (bool2int s6_a2_t1) ))
(assert (>= 3 t1_a2))
(assert (<= 3 t1_a2))
(define-fun t2_a1 () Int (+ (bool2int s1_a1_t2) (bool2int s2_a1_t2) (bool2int s3_a1_t2) (bool2int s4_a1_t2) (bool2int s5_a1_t2) (bool2int s6_a1_t2) ))
(assert (>= 3 t2_a1))
(assert (<= 3 t2_a1))
(define-fun t2_a2 () Int (+ (bool2int s1_a2_t2) (bool2int s2_a2_t2) (bool2int s3_a2_t2) (bool2int s4_a2_t2) (bool2int s5_a2_t2) (bool2int s6_a2_t2) ))
(assert (>= 3 t2_a2))
(assert (<= 3 t2_a2))
声明函数以跟踪哪些学生一起完成作业：
(define-fun s1_has_met_s2 () Bool (or (and s1_a1_t1 s2_a1_t1) (and s1_a2_t1 s2_a2_t1) (and s1_a1_t2 s2_a1_t2) (and s1_a2_t2 s2_a2_t2) ))
(define-fun s1_has_met_s3 () Bool (or (and s1_a1_t1 s3_a1_t1) (and s1_a2_t1 s3_a2_t1) (and s1_a1_t2 s3_a1_t2) (and s1_a2_t2 s3_a2_t2) ))
(define-fun s1_has_met_s4 () Bool (or (and s1_a1_t1 s4_a1_t1) (and s1_a2_t1 s4_a2_t1) (and s1_a1_t2 s4_a1_t2) (and s1_a2_t2 s4_a2_t2) ))
(define-fun s1_has_met_s5 () Bool (or (and s1_a1_t1 s5_a1_t1) (and s1_a2_t1 s5_a2_t1) (and s1_a1_t2 s5_a1_t2) (and s1_a2_t2 s5_a2_t2) ))
(define-fun s1_has_met_s6 () Bool (or (and s1_a1_t1 s6_a1_t1) (and s1_a2_t1 s6_a2_t1) (and s1_a1_t2 s6_a1_t2) (and s1_a2_t2 s6_a2_t2) ))
(define-fun s2_has_met_s3 () Bool (or (and s2_a1_t1 s3_a1_t1) (and s2_a2_t1 s3_a2_t1) (and s2_a1_t2 s3_a1_t2) (and s2_a2_t2 s3_a2_t2) ))
(define-fun s2_has_met_s4 () Bool (or (and s2_a1_t1 s4_a1_t1) (and s2_a2_t1 s4_a2_t1) (and s2_a1_t2 s4_a1_t2) (and s2_a2_t2 s4_a2_t2) ))
(define-fun s2_has_met_s5 () Bool (or (and s2_a1_t1 s5_a1_t1) (and s2_a2_t1 s5_a2_t1) (and s2_a1_t2 s5_a1_t2) (and s2_a2_t2 s5_a2_t2) ))
(define-fun s2_has_met_s6 () Bool (or (and s2_a1_t1 s6_a1_t1) (and s2_a2_t1 s6_a2_t1) (and s2_a1_t2 s6_a1_t2) (and s2_a2_t2 s6_a2_t2) ))
(define-fun s3_has_met_s4 () Bool (or (and s3_a1_t1 s4_a1_t1) (and s3_a2_t1 s4_a2_t1) (and s3_a1_t2 s4_a1_t2) (and s3_a2_t2 s4_a2_t2) ))
(define-fun s3_has_met_s5 () Bool (or (and s3_a1_t1 s5_a1_t1) (and s3_a2_t1 s5_a2_t1) (and s3_a1_t2 s5_a1_t2) (and s3_a2_t2 s5_a2_t2) ))
(define-fun s3_has_met_s6 () Bool (or (and s3_a1_t1 s6_a1_t1) (and s3_a2_t1 s6_a2_t1) (and s3_a1_t2 s6_a1_t2) (and s3_a2_t2 s6_a2_t2) ))
(define-fun s4_has_met_s5 () Bool (or (and s4_a1_t1 s5_a1_t1) (and s4_a2_t1 s5_a2_t1) (and s4_a1_t2 s5_a1_t2) (and s4_a2_t2 s5_a2_t2) ))
(define-fun s4_has_met_s6 () Bool (or (and s4_a1_t1 s6_a1_t1) (and s4_a2_t1 s6_a2_t1) (and s4_a1_t2 s6_a1_t2) (and s4_a2_t2 s6_a2_t2) ))
(define-fun s5_has_met_s6 () Bool (or (and s5_a1_t1 s6_a1_t1) (and s5_a2_t1 s6_a2_t1) (and s5_a1_t2 s6_a1_t2) (and s5_a2_t2 s6_a2_t2) ))
最大限度地增加会面人数：
(maximize (+ (bool2int s1_has_met_s2)(bool2int s1_has_met_s3)(bool2int s1_has_met_s4)(bool2int s1_has_met_s5)(bool2int s1_has_met_s6)(bool2int s2_has_met_s3)(bool2int s2_has_met_s4)(bool2int s2_has_met_s5)(bool2int s2_has_met_s6)(bool2int s3_has_met_s4)(bool2int s3_has_met_s5)(bool2int s3_has_met_s6)(bool2int s4_has_met_s5)(bool2int s4_has_met_s6)(bool2int s5_has_met_s6)))
限制
我 运行 反对的主要限制是 运行 模型所花费的时间。它只是无法扩展：
- 6 名学生、2 名教师、2 项作业：100 毫秒
- 7 名学生，3 名教师，3 份作业：10 秒
- 9 个学生，3 个老师，3 个作业：一分钟后被杀死（谁知道要花多长时间...）
我的目标是 运行 大约有 20 名学生、3 名教师和 5 项作业...不过，根据目前的设置，我怀疑 Z3 是否会完成计算。
This gist 包含具有 9 个学生、3 个教师和 3 个作业的实例的 SMT-LIB 代码。在某种程度上，看到它花了这么长时间我并不感到惊讶......我想要最大化的功能确实在规模上爆炸了。
结束语
如您所见，我卡住了。据我所知，没有更简单的方法来表达这个问题的约束和 objective 函数。在我看来，我已经达到了一个基本的限制。所以我的问题又来了：
- 这个问题花那么多时间解决正常吗？我以前没有经验，所以也许就是这样。
- Z3 是完成这项工作的正确工具吗？如果没有，您还会推荐我尝试什么？
尽量避免使用 bool2int.
例如，而不是：
(assert (= 1 (+ (bool2int s1_a1_t1) (bool2int s1_a1_t2) )))
写入：
(assert (distinct s1_a1_t1 s1_a1_t2))
对于将它们求和的其他约束 up-to 3，看看您是否也可以在不涉及算术的情况下用纯 boolean-reasoning 来表达它。
这里的技巧是避免混合使用布尔值和整数运算。如果能避免后者，z3的日子会好过很多。
对于一般情况，即当有两个以上的赋值时，您应该使用pbeq函数。例如，如果你有 3 个布尔值并且想说其中一个为真，你应该写：
(assert ((_ pbeq 1 1 1 1) b1 b2 b3))
这允许 z3 留在 SAT 求解器中，而不是分支到算术推理，通常会使事情变得更简单。
上下文
作为了解更多关于 SMT 求解和优化的方法，我正在尝试使用 Z3 解决一个具体问题。我已经成功地模拟了这个问题（它编译并 运行s），但我认为我可能做错了什么，因为即使在小实例中也需要几秒钟来解决，而在现实场景中需要几分钟。我觉得我一定是错过了什么。
我的问题是：
- 这个问题花那么多时间解决正常吗？我以前没有经验，所以也许就是这样。
- Z3 是完成这项工作的正确工具吗？如果没有，您还会推荐我尝试什么？
优化问题的描述
假设您正在组织一个烹饪工作坊。有 i 名教师、j 名学生和 k 项实际作业。对于每个实际作业，学生需要分成 i 组，这样他们就可以在老师的监督下完成作业。还有两个附加要求：
- 每个老师必须至少教每个学生一次
- 我们希望最大化在作业期间相互了解的学生数量（即至少在一项作业中合作的学生对数）
例如，有 2 名教师、6 名学生和 2 项实验作业，您可以得到以下划分：
作业 1：
- 老师1：学生1、学生2、学生3
- 老师2：学生4、学生5、学生6
作业 2：
- 老师1：学生4、学生5、学生6
- 老师2：学生1、学生2、学生3
在这里，每一位老师都教过每一位学生。然而，这必然意味着相互了解的学生数量很少。事实上，作业 1 和作业 2 之间的小组并没有发生变化，只有老师发生了变化。
向Z3说明问题
我编写了一个程序来生成一堆 SMT-LIB 语句，然后将其输入 Z3。对于前面有6个学生，2个老师和2个作业的例子，我们得到如下代码（如果你愿意也可以查看here）：
定义一个辅助函数来将布尔值转换为整数：
(define-fun bool2int ((x Bool)) Int (ite x 1 0))
以 s{x}_a{y}_t{z} 形式声明常量，指示学生 x 是否正在与老师 z 一起做作业 y:
(declare-const s1_a1_t1 Bool)
(declare-const s1_a1_t2 Bool)
(declare-const s1_a2_t1 Bool)
(declare-const s1_a2_t2 Bool)
(declare-const s2_a1_t1 Bool)
(declare-const s2_a1_t2 Bool)
(declare-const s2_a2_t1 Bool)
(declare-const s2_a2_t2 Bool)
(declare-const s3_a1_t1 Bool)
(declare-const s3_a1_t2 Bool)
(declare-const s3_a2_t1 Bool)
(declare-const s3_a2_t2 Bool)
(declare-const s4_a1_t1 Bool)
(declare-const s4_a1_t2 Bool)
(declare-const s4_a2_t1 Bool)
(declare-const s4_a2_t2 Bool)
(declare-const s5_a1_t1 Bool)
(declare-const s5_a1_t2 Bool)
(declare-const s5_a2_t1 Bool)
(declare-const s5_a2_t2 Bool)
(declare-const s6_a1_t1 Bool)
(declare-const s6_a1_t2 Bool)
(declare-const s6_a2_t1 Bool)
(declare-const s6_a2_t2 Bool)
声明约束以确保对于每项作业，学生都应该在一位老师的监督下完成：
(assert (= 1 (+ (bool2int s1_a1_t1) (bool2int s1_a1_t2) )))
(assert (= 1 (+ (bool2int s1_a2_t1) (bool2int s1_a2_t2) )))
(assert (= 1 (+ (bool2int s2_a1_t1) (bool2int s2_a1_t2) )))
(assert (= 1 (+ (bool2int s2_a2_t1) (bool2int s2_a2_t2) )))
(assert (= 1 (+ (bool2int s3_a1_t1) (bool2int s3_a1_t2) )))
(assert (= 1 (+ (bool2int s3_a2_t1) (bool2int s3_a2_t2) )))
(assert (= 1 (+ (bool2int s4_a1_t1) (bool2int s4_a1_t2) )))
(assert (= 1 (+ (bool2int s4_a2_t1) (bool2int s4_a2_t2) )))
(assert (= 1 (+ (bool2int s5_a1_t1) (bool2int s5_a1_t2) )))
(assert (= 1 (+ (bool2int s5_a2_t1) (bool2int s5_a2_t2) )))
(assert (= 1 (+ (bool2int s6_a1_t1) (bool2int s6_a1_t2) )))
(assert (= 1 (+ (bool2int s6_a2_t1) (bool2int s6_a2_t2) )))
声明约束以确保每位教师必须至少教每位学生一次：
(assert (or s1_a1_t1 s1_a2_t1 ))
(assert (or s2_a1_t1 s2_a2_t1 ))
(assert (or s3_a1_t1 s3_a2_t1 ))
(assert (or s4_a1_t1 s4_a2_t1 ))
(assert (or s5_a1_t1 s5_a2_t1 ))
(assert (or s6_a1_t1 s6_a2_t1 ))
(assert (or s1_a1_t2 s1_a2_t2 ))
(assert (or s2_a1_t2 s2_a2_t2 ))
(assert (or s3_a1_t2 s3_a2_t2 ))
(assert (or s4_a1_t2 s4_a2_t2 ))
(assert (or s5_a1_t2 s5_a2_t2 ))
(assert (or s6_a1_t2 s6_a2_t2 ))
声明约束以确保对于每项作业，一位教师必须恰好教授 3 名学生。我们将 >= 与 <= 结合使用，因为该问题的某些实例允许最小和最大学生数量（即当 j % i != 0 时）。
(define-fun t1_a1 () Int (+ (bool2int s1_a1_t1) (bool2int s2_a1_t1) (bool2int s3_a1_t1) (bool2int s4_a1_t1) (bool2int s5_a1_t1) (bool2int s6_a1_t1) ))
(assert (>= 3 t1_a1))
(assert (<= 3 t1_a1))
(define-fun t1_a2 () Int (+ (bool2int s1_a2_t1) (bool2int s2_a2_t1) (bool2int s3_a2_t1) (bool2int s4_a2_t1) (bool2int s5_a2_t1) (bool2int s6_a2_t1) ))
(assert (>= 3 t1_a2))
(assert (<= 3 t1_a2))
(define-fun t2_a1 () Int (+ (bool2int s1_a1_t2) (bool2int s2_a1_t2) (bool2int s3_a1_t2) (bool2int s4_a1_t2) (bool2int s5_a1_t2) (bool2int s6_a1_t2) ))
(assert (>= 3 t2_a1))
(assert (<= 3 t2_a1))
(define-fun t2_a2 () Int (+ (bool2int s1_a2_t2) (bool2int s2_a2_t2) (bool2int s3_a2_t2) (bool2int s4_a2_t2) (bool2int s5_a2_t2) (bool2int s6_a2_t2) ))
(assert (>= 3 t2_a2))
(assert (<= 3 t2_a2))
声明函数以跟踪哪些学生一起完成作业：
(define-fun s1_has_met_s2 () Bool (or (and s1_a1_t1 s2_a1_t1) (and s1_a2_t1 s2_a2_t1) (and s1_a1_t2 s2_a1_t2) (and s1_a2_t2 s2_a2_t2) ))
(define-fun s1_has_met_s3 () Bool (or (and s1_a1_t1 s3_a1_t1) (and s1_a2_t1 s3_a2_t1) (and s1_a1_t2 s3_a1_t2) (and s1_a2_t2 s3_a2_t2) ))
(define-fun s1_has_met_s4 () Bool (or (and s1_a1_t1 s4_a1_t1) (and s1_a2_t1 s4_a2_t1) (and s1_a1_t2 s4_a1_t2) (and s1_a2_t2 s4_a2_t2) ))
(define-fun s1_has_met_s5 () Bool (or (and s1_a1_t1 s5_a1_t1) (and s1_a2_t1 s5_a2_t1) (and s1_a1_t2 s5_a1_t2) (and s1_a2_t2 s5_a2_t2) ))
(define-fun s1_has_met_s6 () Bool (or (and s1_a1_t1 s6_a1_t1) (and s1_a2_t1 s6_a2_t1) (and s1_a1_t2 s6_a1_t2) (and s1_a2_t2 s6_a2_t2) ))
(define-fun s2_has_met_s3 () Bool (or (and s2_a1_t1 s3_a1_t1) (and s2_a2_t1 s3_a2_t1) (and s2_a1_t2 s3_a1_t2) (and s2_a2_t2 s3_a2_t2) ))
(define-fun s2_has_met_s4 () Bool (or (and s2_a1_t1 s4_a1_t1) (and s2_a2_t1 s4_a2_t1) (and s2_a1_t2 s4_a1_t2) (and s2_a2_t2 s4_a2_t2) ))
(define-fun s2_has_met_s5 () Bool (or (and s2_a1_t1 s5_a1_t1) (and s2_a2_t1 s5_a2_t1) (and s2_a1_t2 s5_a1_t2) (and s2_a2_t2 s5_a2_t2) ))
(define-fun s2_has_met_s6 () Bool (or (and s2_a1_t1 s6_a1_t1) (and s2_a2_t1 s6_a2_t1) (and s2_a1_t2 s6_a1_t2) (and s2_a2_t2 s6_a2_t2) ))
(define-fun s3_has_met_s4 () Bool (or (and s3_a1_t1 s4_a1_t1) (and s3_a2_t1 s4_a2_t1) (and s3_a1_t2 s4_a1_t2) (and s3_a2_t2 s4_a2_t2) ))
(define-fun s3_has_met_s5 () Bool (or (and s3_a1_t1 s5_a1_t1) (and s3_a2_t1 s5_a2_t1) (and s3_a1_t2 s5_a1_t2) (and s3_a2_t2 s5_a2_t2) ))
(define-fun s3_has_met_s6 () Bool (or (and s3_a1_t1 s6_a1_t1) (and s3_a2_t1 s6_a2_t1) (and s3_a1_t2 s6_a1_t2) (and s3_a2_t2 s6_a2_t2) ))
(define-fun s4_has_met_s5 () Bool (or (and s4_a1_t1 s5_a1_t1) (and s4_a2_t1 s5_a2_t1) (and s4_a1_t2 s5_a1_t2) (and s4_a2_t2 s5_a2_t2) ))
(define-fun s4_has_met_s6 () Bool (or (and s4_a1_t1 s6_a1_t1) (and s4_a2_t1 s6_a2_t1) (and s4_a1_t2 s6_a1_t2) (and s4_a2_t2 s6_a2_t2) ))
(define-fun s5_has_met_s6 () Bool (or (and s5_a1_t1 s6_a1_t1) (and s5_a2_t1 s6_a2_t1) (and s5_a1_t2 s6_a1_t2) (and s5_a2_t2 s6_a2_t2) ))
最大限度地增加会面人数：
(maximize (+ (bool2int s1_has_met_s2)(bool2int s1_has_met_s3)(bool2int s1_has_met_s4)(bool2int s1_has_met_s5)(bool2int s1_has_met_s6)(bool2int s2_has_met_s3)(bool2int s2_has_met_s4)(bool2int s2_has_met_s5)(bool2int s2_has_met_s6)(bool2int s3_has_met_s4)(bool2int s3_has_met_s5)(bool2int s3_has_met_s6)(bool2int s4_has_met_s5)(bool2int s4_has_met_s6)(bool2int s5_has_met_s6)))
限制
我 运行 反对的主要限制是 运行 模型所花费的时间。它只是无法扩展：
- 6 名学生、2 名教师、2 项作业：100 毫秒
- 7 名学生，3 名教师，3 份作业：10 秒
- 9 个学生，3 个老师，3 个作业：一分钟后被杀死（谁知道要花多长时间...）
我的目标是 运行 大约有 20 名学生、3 名教师和 5 项作业...不过，根据目前的设置，我怀疑 Z3 是否会完成计算。
This gist 包含具有 9 个学生、3 个教师和 3 个作业的实例的 SMT-LIB 代码。在某种程度上，看到它花了这么长时间我并不感到惊讶......我想要最大化的功能确实在规模上爆炸了。
结束语
如您所见，我卡住了。据我所知，没有更简单的方法来表达这个问题的约束和 objective 函数。在我看来，我已经达到了一个基本的限制。所以我的问题又来了：
- 这个问题花那么多时间解决正常吗？我以前没有经验，所以也许就是这样。
- Z3 是完成这项工作的正确工具吗？如果没有，您还会推荐我尝试什么？
尽量避免使用 bool2int.
例如，而不是：
(assert (= 1 (+ (bool2int s1_a1_t1) (bool2int s1_a1_t2) )))
写入：
(assert (distinct s1_a1_t1 s1_a1_t2))
对于将它们求和的其他约束 up-to 3，看看您是否也可以在不涉及算术的情况下用纯 boolean-reasoning 来表达它。
这里的技巧是避免混合使用布尔值和整数运算。如果能避免后者，z3的日子会好过很多。
对于一般情况，即当有两个以上的赋值时，您应该使用pbeq函数。例如，如果你有 3 个布尔值并且想说其中一个为真，你应该写：
(assert ((_ pbeq 1 1 1 1) b1 b2 b3))
这允许 z3 留在 SAT 求解器中，而不是分支到算术推理，通常会使事情变得更简单。