我在以下链接中找到了“MaxSAT/MaxSMT 示例” http://research.microsoft.com/en-us/um/redmond/projects/z3/group_maxsat_ex.html 但它只提供 C 代码。
我感兴趣的是它是如何直接使用 Z3 编码的？有人可以给我举个例子吗？谢谢!
最佳答案
Z3 文档中的 MaxSAT/MaxSMT 示例的主要目的是演示如何使用 API Z3_check_assumptions 为 MaxSAT 实现两个不同的程序。该示例包含几条解释基本思想的注释以及对 Fu 和 Malik 的论文的引用。论文对本例中fu_malik_maxsat过程中使用的算法进行了详细描述。还有其他 MaxSAT 算法可以在 Z3 API 的顶部实现。
Z3 SMT 2.0 前端(即 z3 可执行文件)不直接支持 MaxSAT/MaxSMT。
但是，可以为 check-sat 命令提供假设。
对 MaxSAT 感兴趣的用户应该使用 MaxSAT 示例作为起点。
关于z3 - MaxSAT/MaxSMT 示例，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/12236873/