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

Question

我对解决 Z3 中的调度问题感兴趣，这需要以下内容：

我将它们视为集合，但它们可以被视为关联、2-adic 函数 (

isin(student, class

)、1-adic 函数 (

class1(student)

、

student1(class)

)、位向量、数组...

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

Answer 1

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

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