我在以下链接中找到了“ 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过程中使用的算法。 Z3 API的顶部还可以实现其他MaxSAT算法。
Z3 SMT 2.0前端（即z3可执行文件）不直接支持MaxSAT / MaxSMT。
但是，可以为check-sat命令提供假设。
对MaxSAT感兴趣的用户应以MaxSAT示例为起点。