我在以下链接http://research.microsoft.com/en-us/um/redmond/projects/z3/group_ maxsat _ex.html中找到了"MaxSAT/MaxSMT示例", 但它只提供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示例作为起点.