使用 jsmtlib 返回未知的未饱和/未饱和答案

【问题标题】：Returning unknown not sat/unsat with jsmtlib使用 jsmtlib 返回未知的未饱和/未饱和
【发布时间】：2012-09-21 17:49:01
【问题描述】：

按照this tutorial，我尝试了教程中的第一个示例。

(set-option :print-success false)
(set-logic QF_UF)
(declare-fun p () Bool)
(assert (and p (not p)))
(check-sat)
(exit)

我执行了这个命令

java -jar jsmtlib.jar test1.smt

获取unknown 而不是教程中的unsat。

这可能有什么问题？

【问题讨论】：

标签： smt

【解决方案1】：

我需要指定我使用什么求解器。我选择yices 作为服务器，使用java -jar jsmtlib.jar --solver yices --exec ./yices test1.smt，一切正常。

【讨论】：

【解决方案2】：

我相信jsmtlib.jar 是 SMT 求解器的某种包装器。 “未知”的答案与 Z3 无关。您应该就这个问题联系jsmtlib.jar作者。

你试过直接用Z3吗？它为此脚本返回 unsat。您可以在线试用 Z3： http://rise4fun.com/Z3/chyM

【讨论】：