I have a DAG. I want to construct a boolean formula $\varphi$ that represents all paths from a source node to a sink node.

In particular, I have a variable for each vertex. A path $v_1 \to v_2 \to \dots \to v_k$ is represented as the subformula $v_2 \lor \dots \lor v_{k-1}$. I want a formula $\varphi$ that is a conjunction of all of these subformulas (one subformula per path from a source node to a sink node).

How can I construct $\varphi$ in CNF form?

Input example:

    ^  (r1 and r2 both reach w)
R1    R2

 X    X (this signifies a connection to R1 and R2)

b1    b2
^     ^
|     |
c1    c2

Desired output in CNF format:

(b1 or R1)
(b1 or R2)
(b2 or R1)
(b2 or R2)

The output represents all paths from c1 or c2 to w.

  • $\begingroup$ @D.W. does the last paragraph helps to specify the output? $\endgroup$
    – Klaus
    Jul 12 '17 at 20:38
  • $\begingroup$ I edited your question based on your comments. Please check whether it accurately reflects what you want. You still need to answer my question: Can we introduce additional temporary variables into the formula, if that helps make it shorter/smaller? This has a significant affect on the best solution to your problem. Also, in your example, shouldn't it be c1 or b1 or R1 or W instead of b1 or R1, etc.? $\endgroup$
    – D.W.
    Jul 12 '17 at 21:44
  • $\begingroup$ Thanks for the edit, @D.W. to answer your question regarding temporary values, making the formula smaller is not necessary but I guess it is a step that would be welcome. Regarding why b1 or R1 is the answer for the first path. The reasoning is that within each path (from a leaf to root), the invalidation of any node along invalidates the whole path. The algorithm needs to find the set of nodes (excluding the leaf and root) which invalidates the path. $\endgroup$
    – Klaus
    Jul 12 '17 at 22:13

If you don't want to allow introduction of any temporary values, then you just need to enumerate all paths in the graph. There are many ways to do that. A simple method is a recursive algorithm, where at each step you move one step forward to a vertex $w$, then recursively find all paths from $w$.

However, the running time and size of the output is proportional to the number of paths, which might be exponentially large. Therefore, this cannot be said to be efficient in practice.

If you are willing to allow introduction of temporary variables into the formula, then you can solve this problem without needing exponential time or space. Suppose the variables are $v_1,\dots,v_n$. I'll describe an algorithm that outputs a boolean formula $\varphi(v_1,\dots,v_n,t_1,\dots,t_k)$ in CNF form, where $t_1,\dots,v_k$ are temporary variables, with the following property: if $\varphi(v_1,\dots,v_n,t_1,\dots,t_k)$ is true, then there is a path that goes through the vertices $v_i$ such that $v_i=\text{True}$); and if there's a path that goes through a set of vertices, then there exists $t_1,\dots,t_k$ such that $\varphi(v_1,\dots,v_n,t_1,\dots,t_k)$ (where $v_i$ is true if the path goes through $v_i$, and false otherwise).

In particular, we construct a boolean circuit $C$ that accepts boolean inputs $v_1,\dots,v_n$ and $n^3$ bits representing a sequence of edges $e_1,e_2,\dots,e_m$ (with $m < n$). The circuit outputs true if $e_1,e_2,\dots,e_m$ represents a path (i.e., the destination of $e_i$ matches the source of $e_{i+1}$) from source to sink, and if $v_i$ is true if and only if $v_i$ appears somewhere in that path. It's possible to build a polynomial-size circuit to check this.

Now we convert this circuit to CNF, using the Tseitin transform. This introduces some additional temporary variables. We let $\varphi$ denote this formula. It depends on the variables $v_1,\dots,v_n$, and on some temporary variables; the temporary variables include the $n^3$ input bits that represent the path, plus all temporary variables introduced by the Tseitin transform. The Tseitin transform outputs a CNF formula that is satisfiable just when the circuit outputs true, so this gives us a CNF formula of the desired form.

If you don't want to work through the details of the Boolean circuit, here is an explicit construction of such a formula. The variables will be named $x_v$ where $v \in V$ is a vertex. I'll also use temporary variables named $y_{v,i}$ where $v$ ranges over vertices and $i \in \{1,2,\dots,n\}$. The intuition is that $y_{v,i}=\text{True}$ will indicate that the $i$th step of the path is at vertex $v$. For convenience, add a self-loop (a self-edge) $v \to v$ to the graph for each sink vertex $v$.

The formula is a conjunction of several different types of clauses, each with a different purpose:

  • The path starts at a source vertex: $\bigvee_v y_{v,1}$ where in this clause $v$ ranges over the source vertices.

  • At each step, the path is at a single vertex: for each $i$ we have $\bigvee_v y_{v,i}$ ("at least one"), and for each $i$ and each pair of different vertices $v,w$ we have $(\neg y_{v,i} \lor \neg y_{w,i})$ ("at most one").

  • The path ends at a sink vertex: $\bigvee_v y_{v,n}$ where in this clause $v$ ranges over the sink vertices.

  • Each step traverses an edge: for each $i$ and each non-edge $(v,w) \notin E$, we have the clause $(\neg y_{v,i} \lor \neg y_{w,i+1})$.

  • A vertex $v$ is visited ($x_v=\text{True}$) iff it appears at some step of the path: for each non-source non-sink vertex $v$, we have a clause $(\neg x_v \lor y_{v,1} \lor y_{v,2} \lor \dots \lor y_{v,n})$; and for each $i$ we have a clause $(\neg y_{v,i} \lor x_v)$.

Taking the conjunction of all of those clauses gives a boolean formula in CNF form.

  • $\begingroup$ I actually was thinking on the first solution, I don't have it fully automated yet but it does work. As you said the problem is indeed when you deal with bigger and bigger graphs, I think that's a NP-hard problem. Your second solution is quite good, could you give me any pointers on how to go and implement this kind Boolean circuit, I haven't had any experience with this. I know asking for implementation is off topic here, but still I would like to try it. $\endgroup$
    – Klaus
    Jul 13 '17 at 9:50
  • $\begingroup$ @Klaus, OK, I edited my answer to give an explicit construction. See the end of the answer for a description of a CNF formula. (I used different notation there; I hope that's not too confusing.) $\endgroup$
    – D.W.
    Jul 14 '17 at 5:55
  • $\begingroup$ is the explicit construction edit, a solution without the circuit? Do I have to traverse the graph in this case? Do you have any resources like a book I can look into to study these boolean circuits and representations in programming languages? thanks a lot $\endgroup$
    – Klaus
    Jul 14 '17 at 13:02
  • $\begingroup$ @Klaus, it's a solution without the circuit. I don't know of any good books to recommend.. $\endgroup$
    – D.W.
    Jul 14 '17 at 13:25
  • $\begingroup$ What would happen if the graph is not acyclic? Is your solution still good? $\endgroup$
    – Klaus
    Jul 14 '17 at 16:46

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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