3
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ 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)))) $\endgroup$ – chi Sep 4 '18 at 15:48
  • $\begingroup$ 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) $\endgroup$ – Josep Ng Sep 4 '18 at 16:40
  • $\begingroup$ 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) ) $\endgroup$ – Josep Ng Sep 4 '18 at 16:42
  • $\begingroup$ it still uses the value 0 $\endgroup$ – Josep Ng Sep 4 '18 at 16:43
  • $\begingroup$ 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. $\endgroup$ – D.W. Sep 4 '18 at 17:42
1
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ 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. $\endgroup$ – Josep Ng Sep 6 '18 at 12:04
  • $\begingroup$ @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. $\endgroup$ – D.W. Sep 6 '18 at 15:40

Your Answer

By clicking "Post Your Answer", you acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.

Not the answer you're looking for? Browse other questions tagged or ask your own question.