(get-unsat-core) Z3: unsat core is not available

Question

这是我的程序，当图中存在循环时返回SAT，当没有周期时返回UNSAT：

(set-option :fixedpoint.engine datalog) 
(define-sort s () Int) 
(declare-rel edge (s s)) 
(declare-rel path (s s)) 
(declare-var a s) 
(declare-var b s) 
(declare-var c s) 
(rule (=> (edge a b) (path a b)))
(rule (=> (and (path a b) (path b c)) (path a c)))
(rule (edge 1 2))
(rule (edge 2 3))

(declare-rel cycle (s))
(rule (=> (path a a) (cycle a)))
(query cycle :print-answer true)

我想在没有周期时获得模型(UNSAT(。我意识到我应该使用命令(get-unsat-core(并将选项设置为(set-option :p roduce-unsat-cores true(：

(set-option :fixedpoint.engine datalog) 
(set-option :produce-unsat-cores true)
(define-sort s () Int) 
(declare-rel edge (s s)) 
(declare-rel path (s s)) 
(declare-var a s) 
(declare-var b s) 
(declare-var c s) 
(rule (=> (edge a b) (path a b)) P-1)
(rule (=> (and (path a b) (path b c)) (path a c)) P-2)
(rule (edge 1 2) E-1)
(rule (edge 2 3) E-2)
(rule (edge 3 1) E-3)
(declare-rel cycle (s))
(rule (=> (path a a) (cycle a)))
(query cycle :print-answer true)

(get-unsat-core)

我收到此错误：

unsat
(error "line 24 column 15: unsat core is not available")

Answer 1

在unsat的情况下获取模型没有意义。不满足字面意思是没有模型可以满足你的约束。请发布一个更明确的问题，说明您要实现的目标。

未卫星核心是冲突断言的子集。根据定义，此集合是不满足的，并且不构成您所寻求的模型。此外，我非常怀疑定点引擎是否支持unsat内核，因此您收到的错误消息只是意味着它们未计算。

Answer 2

如果我可以打扰，AFAIK在想要检索unsat core时需要命名约束。

smtlib 网站提供了以下示例：

; Getting unsatisfiable cores
(set-option :produce-unsat-cores true)
(set-logic QF_UF)
(declare-const p Bool) (declare-const q Bool) (declare-const r Bool)
(declare-const s Bool) (declare-const t Bool)
(assert (! (=> p q) :named PQ))
(assert (! (=> q r) :named QR))
(assert (! (=> r s) :named RS))
(assert (! (=> s t) :named ST))
(assert (! (not (=> q s)) :named NQS))
(check-sat)
; unsat
(get-unsat-core)
; (QR RS NQS)
(exit)

正如@LeventErkok所指出的，模型仅在公式sat时可用，而unsat core仅在公式unsat时可用。