检测图中不存在循环：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。

一个建议（但不符合我的需要）是：

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

有什么想法解决这个问题吗？

（使用Quantifiers会增加问题的复杂性，这就是为什么我在寻找一些替代解决方案）。

Answer 1

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

在最坏的情况下，您可能需要量词