【发布时间】：2017-01-01 11:41:17
【问题描述】：
我是使用 Z3py 的新手，我的任务是为两种解决方案（sat 和 unsat）生成反例。
有什么函数可以生成unsat解的反例吗？
【问题讨论】：
标签： boolean counter z3 solver z3py
【发布时间】：2017-01-01 11:41:17
【问题描述】：
unsat 表示没有满足给定断言的模型。只能在问题为sat 时提取模型。因此，要回答您提出的问题，您不能从 unsat 解决方案创建模型：它根本不存在。
一个典型的方法是断言你试图证明的公式的negation；如果该公式是可满足的，那么您的原始公式是可证伪的；即，有一个反例。也许这就是你想要做的？即：如果公式的否定有一个令人满意的模型，那么这个模型就是原公式的反例。这就是大多数建立在 SMT 求解器之上的证明者的工作方式，通过发送对他们试图证明的内容的否定并返回 unsat. 如果证明者返回一个模型，那么它就是一个反例。
【讨论】：