mathematical-optimization - 我如何最好地解决此优化问题？

Question

语境

作为更多了解SMT解决和优化的方法，我试图使用Z3解决一个具体问题。我已经成功地对问题进行了建模（它可以编译并运行），但是我想我可能做错了，因为即使在很小的情况下，解决问题也要花几秒钟，而在实际情况下要花几分钟。我觉得我一定很想念东西。

我的问题是：


这个问题花很多时间解决是正常现象吗？我以前没有经验，所以也许就是这样。
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是否正在与老师 y做作业 z：

(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个作业：100ms
7位学生，3位老师，3个作业：10s
9位学生，3位老师，3个作业：一分钟后被杀（谁知道要花多长时间...）


我的目标是与大约20名学生，3名老师和5项作业一起运行此程序……不过，按照目前的设置，我怀疑Z3能否完成计算。

This gist包含实例的SMT-LIB代码，其中包含9位学生，3位老师和3个作业。从某种程度上来说，这么长的时间并没有让我感到惊讶...我想要最大化的功能的确在规模上爆炸了。

结束语

如您所见，我被困住了。据我所知，没有更简单的方法来表达此问题的约束和目标函数。在我看来，我已经达到了基本的限制。因此，在这里再次提出我的问题：


这个问题花很多时间解决是正常现象吗？我以前没有经验，所以也许就是这样。
Z3是适合该工作的工具吗？如果没有，您还建议我尝试什么？

Answer 1

尝试避免使用bool2int。

例如，代替：

(assert (= 1 (+ (bool2int s1_a1_t1) (bool2int s1_a1_t2) )))

写：

(assert (distinct s1_a1_t1 s1_a1_t2))

对于将它们加起来最多为3的其他约束，请查看是否还可以用纯布尔推理来表示，而不涉及算术运算。

这里的技巧是避免将布尔值和整数算术混合。如果可以避免后者，则z3的时间会轻松得多。

对于一般情况，即，当分配有两个以上时，应使用 pbeq函数。例如，如果您有3个布尔值，并且想准确地说出其中之一是正确的，则应输入：

(assert ((_ pbeq 1 1 1 1) b1 b2 b3))

这使得z3可以保留在SAT求解器中，而不必分支到算术推理上，通常可以使事情变得更简单。