Z3Py 中的模型计数答案

【问题标题】：Model counting in Z3PyZ3Py 中的模型计数
【发布时间】：2015-03-14 13:23:39
【问题描述】：

我正在尝试计算 Z3 令人满意的作业数量。我想知道Z3是否提供了这样的信息。如果是这样，我如何计算 Z3 中的模型，尤其是 Z3Py 中的模型？

【问题讨论】：

标签： z3 z3py

【解决方案1】：

虽然 Taylor 的答案会给您提供令人满意的作业数量，但它会遍历所有作业。原则上，无需如此昂贵的迭代也可以做到，但 Z3 不提供。

命题逻辑有高效的模型计数器，与 SAT 中使用的语言相同（搜索 sharpSAT 以找到这样的系统），但据我所知，没有可用的模型计数器模理论。

【讨论】：

【解决方案2】：

不，默认情况下此类信息不可用。但是，您可以通过将模型生成功能与添加断言相结合，在任何 API 中轻松实现这一点（假设模型数量有限），以防止未来的分配被分配与过去模型相同的值。有关完成此操作的 Z3py 脚本，请参阅以下答案：

要计算模型，只需在循环中添加一个计数器，直到它变为 unsat，这将为您提供模型的数量。

【讨论】：