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

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


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.

• I guess a is simply an integer: you did not constrain it to be a vertex, so it can be chosen as 0 by the solver. Define a vertex predicate , and require (vertex a) somewhere. E.g. (assert (not (and (vertex a) (path a a))))
– chi
Commented Sep 4, 2018 at 15:48
• Here is the program after modifying it with you proposal: (set-option :fixedpoint.engine datalog) (define-sort s () Int) (declare-rel edge (s s)) (declare-rel path (s s)) (declare-rel vertex (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 (and (vertex a) (path a a)))) (check-sat) (get-model) Commented Sep 4, 2018 at 16:40
• it returns the result: z3 tesss.txt sat (model (define-fun a () Int 0) (define-fun vertex ((x!0 Int)) Bool false) (define-fun path ((x!0 Int) (x!1 Int)) Bool false) ) Commented Sep 4, 2018 at 16:42
• it still uses the value 0 Commented Sep 4, 2018 at 16:43
• What does "for reasons of complexity" mean? Are you assuming that using Datalog is going to be the most efficient way to solve this? That might not be the case.
– D.W.
Commented Sep 4, 2018 at 17:42

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.

• Yes i already did this. The problem now is how can i reverse the problem (an instance that is satisfiable iff there is no cycle) without using negation, because the complexity of Datalog with negation is not P. Commented Sep 6, 2018 at 12:04
• @JosepNg, see the first sentence of my answer, for the answer to that question. My particular algorithm is in P: you first find whether $\exists x . R(x,x)$ is true (this is Datalog so it can be done in P); then reverse the answer (this is in P). Or, you can more easily see that it is in P by directly solving the problem without Datalog, e.g., by separating the graph into connected components and checking whether each component is a tree or not.
– D.W.
Commented Sep 6, 2018 at 15:40