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

Posted 2023-02-25

【中文标题】Z3：如何办理协会或会员资格？

【英文标题】：Z3: How to handle association or membership?

【发布时间】：2021-12-04 16:05:04

【问题描述】：

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

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

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

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

【参考方案1】：

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

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

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

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