检测图中不存在循环：Z3 的 SMTLIB 格式

Question

此问题与：Cyclic relation in Datalog using SMTLib for z3

我想扭转上面链接中描述的问题。我的意思是我想检测图中不存在循环。

建议的解决方案是：

(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)) 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)

但我的问题是，如果图表中没有循环，我如何获得 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) r-1)
(rule (edge 2 3) r-2)
(rule (edge 3 1) r-3)


(assert (not (path a a)))

(check-sat)
(get-model)

作为结果返回：

> z3 test.txt
sat
(model
  (define-fun a () Int
    0)
  (define-fun path ((x!0 Int) (x!1 Int)) Bool
    (ite (and (= x!0 0) (= x!1 0)) false
      false))
)

我不明白为什么 z3 将 0 分配给变量，而我只有 1、2 和 3 作为顶点？

另一个建议是：

(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) r-1)
(rule (edge 2 3) r-2)
(rule (edge 3 1) r-3)


(assert
         (=> (path a a)
            false
            )  

 )


(check-sat)
(get-model)

返回结果：

> z3 test2.txt
sat
(model
  (define-fun a () Int
    0)
  (define-fun path ((x!0 Int) (x!1 Int)) Bool
    (ite (and (= x!0 0) (= x!1 0)) false
      false))
)

有解决这个问题的办法吗？

（使用量词会增加问题的复杂性，这就是我正在寻找一些替代解决方案的原因）。

Answer 1

我不熟悉 z3 的这一部分，但总的来说，结果对我来说似乎是合理的。 Z3 正在尝试为您的问题寻找模型。 您从未说过 1 2 3 是所有顶点，而只是说它们是一些顶点。您可以通过为顶点引入谓词并说其他任何东西都不是顶点来解决此问题。

在最坏的情况下你可能需要一个量词