1

这是我的程序，当图中存在循环时返回 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 :produce-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")
4

2 回答 2

4

在unsat案例中获取模型没有意义。Unsatisfiable 字面意思是没有模型可以满足您的约束。请发布一个更明确的问题，确切说明您要达到的目标。

未饱和核心是冲突断言的子集。根据定义，该集合是不可满足的，并且不构成您正在寻找的模型。此外，我非常怀疑定点引擎是否支持 unsat-cores，因此您收到的错误消息只是意味着它们没有被计算。

于 2018-09-07T16:56:00.517 回答
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。

于 2018-09-08T07:08:28.567 回答