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 Sep 4 '18 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) – Josep Ng Sep 4 '18 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) ) – Josep Ng Sep 4 '18 at 16:42
• it still uses the value 0 – Josep Ng Sep 4 '18 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. Sep 4 '18 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. – Josep Ng Sep 6 '18 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. Sep 6 '18 at 15:40