Detect non existence of a cycle in a graph using Datalog : SMTLIB Format for Z3

Question

I want to detect the non existence of a cycle in a graph using Datalog (which is a declarative logic programming language).

The proposed solution was:

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

But my question is how can i get SAT when there is no cycle in the graph and UNSAT when there exists a cycle.

One suggestion (but that does not meet my need) is:

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

which returns as result:

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

I don't understand why z3 assign 0 to the variables while I only have 1, 2 and 3 as vertices?

Another suggestion was :

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

Which returns the result:

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

Any idea to resolve this problem?

Note: I need to use Datalog for reasons of complexity.

Answer 1

I don't think you can do it in plain Datalog, but you can do it in Datalog plus negation.

I suggest you define a relation $R$, so that $R(x,y)$ is true if vertex $y$ is reachable from vertex $x$ in one or more steps. You can define $R$ recursively, namely,

$$R(x,y) = E(x,y) \lor \exists w . E(x,w) \land R(w,y),$$

where $E$ is a relation that represents the edges in the graph ($E(x,y)$ is true iff $(x,y)$ is an edge in the graph). Now the graph has a cycle iff $\exists x . R(x,x)$ is true. I think you should be able to translate this in Datalog.

From this you can get a Datalog instance that is satisfiable if there is a cycle in the graph, or unsatisfiable if there is no cycle.

If you want the reverse (an instance that is satisfiable iff there is no cycle), I think you need negation.

The details of how to express that in Z3 code seem off-topic here.