Z3Py 中的模型计数 [英] Model counting in Z3Py

问题描述

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

I am trying to count the number of satisfying assignments by Z3. I am wondering if Z3 provides such information. If so, how can I count models in Z3 and particularly in Z3Py?

推荐答案

虽然 Taylor 的回答会给出令人满意的作业数量，但它会遍历所有作业.原则上，没有如此昂贵的迭代是可以做到的，但 Z3 没有提供.

While Taylor's answer will give you the number of satisfying assignments, it will iterate over all of them. In principle, it is possible to do it without such an expensive iteration, but Z3 does not offer it.

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

There are efficient model counters for propositional logic, the same language used in SAT (search for sharpSAT to find such a system), but as far as I know there is no available model counter modulo theories.

这篇关于Z3Py 中的模型计数的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！