Z3：如何办理协会或会员资格？

Question

我对解决 Z3 中的调度问题很感兴趣，这需要：

• 有多个类：C1、C2、C3...
• 和多名学生：S1、S2、S3...
• 每个学生都必须在一个班级里
• 每个班级不得超过 K 名学生

我认为这些是集合，但它们可以被认为是关联、2-adic 函数 (isin(student, class)、1-adic 函数 (class1(student)、student1(class))、位向量、数组...

在 Z3 中对这些进行建模并解决有关它们的问题的最简单、最简单的方法是什么？

Answer 1

显而易见的事情是从您为班级和学生声明的自定义排序（作为枚举）中创建一个数组。该数组会将这些映射到布尔值，从而为您提供成员资格。

但是，请注意，SMT 求解器很难击败自定义调度算法；如果您有过多的约束，特别是如果您还试图最大化/最小化某种成本函数。话虽如此，这类事情以前也做过。这里有两个例子：

• 车间调度：https://www.cs.toronto.edu/~victorn/tutorials/z3/SMT.html
• 更严肃的学术文章：https://www.sciencedirect.com/science/article/pii/S000437021930195X

（附带说明.. 如果您尝试某些事情并遇到问题，Stack-overflow 效果最好；发布您尝试过的代码。不幸的是，这些“一般”指导问题并不是这个论坛的最佳选择. 见这里：https://stackoverflow.com/help/how-to-ask)