z3 - MaxSAT/MaxSMT 示例

Question

我在以下链接 http://research.microsoft.com/en-us/um/redmond/projects/z3/group_maxsat_ex.html找到了“ MaxSAT / MaxSMT示例”， 但它只提供 C 代码。

我对如何直接使用 Z3 编码感兴趣？有人可以给我一个例子吗？谢谢！

Answer 1

Z3 文档中的 MaxSAT/MaxSMT 示例的主要目的是演示如何使用 APIZ3_check_assumptions为 MaxSAT 实现两个不同的过程。该示例包含几条解释基本思想的注释和对 Fu 和 Malik 的论文的参考。该论文详细描述了fu_malik_maxsat本示例中的过程中使用的算法。还有其他 MaxSAT 算法可以在 Z3 API 的顶部实现。

Z3 SMT 2.0 前端（即 z3 可执行文件）不直接支持 MaxSAT/MaxSMT。然而，可以为check-sat命令提供假设。对 MaxSAT 感兴趣的用户应该使用 MaxSAT 示例作为起点。