根据求解器的决定执行 get-model 或 unsat-core

Question

我想知道，在 SMT-LIB 2.0 脚本中是否有可能访问求解器的最后可满足性决策（sat、unsat、...）。例如下面的代码：

(set-option :produce-unsat-cores true)
(set-option :produce-models true)
(set-logic QF_UF)
(declare-fun p () Bool)
(declare-fun q () Bool)
(declare-fun r () Bool)

(assert (! (=> p q) :named PQ))
(assert (! (=> q r) :named QR))
(assert (! (not (=> p r)) :named nPR))

(check-sat)
(get-model)
(get-unsat-core)

运行在 Z3 returns:

unsat
(error "line 15 column 10: model is not available")
(PQ QR nPR)

和运行在 MathSAT returns:

unsat
(error "model generation not enabled")

在 MathSAT 5 中，它只是在 (get-model) 上中断，甚至没有达到 (get-unsat-core)。如果决定是 SAT，SMT-LIB 2.0 语言是否有任何方法可以获取模型，如果决定是 UNSAT，是否可以获取 unsat-core？例如，解决方案可能如下所示：

(check-sat)
(ite (= (was-sat) true) (get-model) (get-unsat-core))

我搜索了 SMT-LIB 2.0 语言文档，但没有找到任何提示。

编辑：我也尝试了下面的代码，不幸的是它没有用。

(ite (= (check-sat) "sat") (get-model) (get-unsat-core))

Answer 1

SMT 语言不允许您这样编写命令。 Boogie 等工具处理此问题的方法是使用双向文本管道：它从 (check-sat) 读回结果。如果结果字符串是 "unsat" 型号不可用，但是如果检查使用假设，核心将是。如果由此产生字符串是 "sat" 该工具可以期待一个 (get-model) 命令成功。

Answer 2

正如 Nikolaj 在他的回答中所说，正确的方法是解析求解器输出并有条件地生成 (get-model) 或 (get-unsat-core) 语句。

但是，对于 mathsat，您可以使用没有 (get-model) 语句的代码，并使用 -model 选项调用 mathsat。例如：

$ cat demo_sat.smt2 
(set-option :produce-unsat-cores true)
(set-option :produce-models true)
(set-logic QF_UF)
(declare-fun p () Bool)
(declare-fun q () Bool)
(declare-fun r () Bool)

(assert (! (=> p q) :named PQ))
(assert (! (=> q r) :named QR))
; (assert (! (not (=> p r)) :named nPR))

(check-sat)
(get-unsat-core)

$ mathsat -model demo_sat.smt2 
sat
( (p false)
  (q false)
  (r false) )
(error "no unsatisfiability proof, impossible to compute unsat core")

在不饱和的情况下：

$ cat demo_unsat.smt2 
(set-option :produce-unsat-cores true)
(set-option :produce-models true)
(set-logic QF_UF)
(declare-fun p () Bool)
(declare-fun q () Bool)
(declare-fun r () Bool)

(assert (! (=> p q) :named PQ))
(assert (! (=> q r) :named QR))
(assert (! (not (=> p r)) :named nPR))

(check-sat)
(get-unsat-core)

$ mathsat -model demo_unsat.smt2 
unsat
( PQ
  QR
  nPR )

不幸的是，似乎不存在像 -model 这样的选项来生产不饱和核心。因此，如果您想将它用于增量问题，则此 hack 将不起作用，除非您同意求解器在第一个 sat 结果后终止。（因为在第一个 sat 结果中，求解器将因 (get-unsat-core) 的错误而退出。）

根据求解器的决定执行 get-model 或 unsat-core

Executing get-model or unsat-core depending on solver's decision

smt

z3

mathsat