Computing the existence of a path in a code execution graph

Question

I have a need for an algorithm which I can express as a reachability problem in a graph.

Note that I'd appreciate any advices with respect to better wording this question. Also please tell me if this question does not fit this site (I considered posting it to "Computer Science" instead).

Problem Statement

Consider an directed, connected, possibly cyclic graph $G=(V,E)$.

Consider also a finite set of "indicators" $I$, of a finite size. They are numbered $I_0 .. I_n$.

Each indicator $I_i$ can take an integer value in the range $[0..v(i)]$.

Each vertex can be labelled with one or more "assignations" of the form $I_i := v$, with $v \in [0..v(i)]$.

Exactly one vertex $V_0 \in V$ is distinguished as the "graph entry".

It is also considered that $V_0$ is labelled by $I_j := 0, \forall j \in [0..n]$ (i.e. the "value" of all indicators is $0$ at the graph entry).

Some vertices are such that all outbound edges from them are labelled by a "guard" of the form $I_k = v_p$, for a fixed value $k$ and all possible $p \in [0..m(k)]$ (i.e. there are "switches" at some vertexes where an edge is "chosen" based on the "current" value of an indicator).

We define (somewhat informally) a "valid" path in the graph as:

• being finite,
• respecting the topology constraints in the graph,
• and being such that, if is is crossed from its beginning to its end, while collecting the "current" (i.e., latest encountered) value of indicators in the process, then the equality associated to each guard is verified.

Informally, the graph represents all possible execution flows in a piece of code, with indicator variables being set and branching decisions being taken with respect to those indicators.

Now my problem is the following: given a vertex $V_q \in V$, does a valid path (in the sense defined above) exists from $V_0$ to $V_q$?

Note that I only need an algorithm efficiently answering if such path exists; I do not need it to construct one.

What I Did so Far

Empirically, I had quite good results so far with a brute-force execution simulation strategy enumerating all possible paths (with some memoization to limit memory consumption and ensure termination in the presence of cycles). But some larger graphs are proving a challenge, since most probably my current enumeration approach is of an exponential complexity.

Mostly I'd like to express my problem in a domain where I could benefit from existing complexity proofs and (hopefully!) solvers. I tried my hands at classical graph theory problems, considered SAT and Petri Nets too, but did not see a match so far. I also tried some classic and more recent data flow algorithms at first, but they fail short since I need an exact result.

Answer 1

As such, your problem seems to be NP-complete. To see the membership in NP, you can first guess a path, and then check that this path ends with $V_q$ and is valid. For the hardness part, we can directly reduce from the Boolean satisfiability problem (SAT), which itself is NP-hard. The problem SAT takes as input a formula in conjunctive normal form (CNF), and outputs YES if the formula is satisfiable, and NO otherwise. Let $F = C_1 \land \ldots \land C_m$ be a CNF over variables $\{x_1,\ldots,x_n\}$, where each clause $C_i$ is a disjunction of literals. We will construct an instance graph $G_F$ of your problem with distinguished nodes $V_0$ and $V_\top$ such that there exists a valid path from $V_0$ to $V_\top$ if and only if $F$ is satisfiable. For every variable $x_i$, $1 \leq i \leq n$, $G_F$ has a node $V_{x_i}$ and a node $V_{\overline{x_i}}$, and you have one “indicator” $I_{x_i}$, with possible values being $\{\text{TRUE}, \text{FALSE}\}$. The node $V_{x_i}$ assigns $I_{x_i}$ to TRUE (i.e., you have $I_{x_i} := \text{TRUE}$), while the node $V_{\overline{x_i}}$ assigns $I_{x_i}$ to FALSE. Now, we have an (directed) edge between the node $V_0$ and the node $V_{x_1}$, as well as between $V_0$ and $V_{\overline{x_i}}$. For $1 \leq i < n$ we have the edges $(V_{x_i},V_{x_{i+1}})$, $(V_{x_i},V_{\overline{x_{i+1}}})$, $(V_{\overline{x_i}},V_{x_{i+1}})$, and $(V_{\overline{x_i}},V_{\overline{x_{i+1}}})$. For now, a path in the graph simply assigns a Boolean value to each variable, so we now need to construct the part that “checks” that this assignment satisfies $F$. For every clause $C_i$, $1 \leq i \leq m$, we construct a graph gadget $G_{C_i}$ encoding that $C_i$ is satisfied. For instance, suppose that $C_i$ is the clause $x_4 \lor \overline{x_2} \lor x_3$. Then $G_{c_i}$ has an entry node $V_{C_i,x_4}$, and nodes $V_{C_i,\overline{x_2}}$ and $V_{C_i,x_3}$. You have a “switching” edge from $V_{C_i,x_4}$ to the entry node of $G_{C_{i+1}}$ that checks that $I_{x_4} = \text{TRUE}$, and a switching edge from $V_{C_i,x_4}$ to $V_{C_i,\overline{x_2}}$ that checks that $I_{x_4} = \text{FALSE}$, and so on. You then chain these gadgets in series and plug that chain to the already partially constructed graph $G_F$ (that guesses an assignment), and construct the node $V_\top$ in the expected way (I'll leave the missing details), and voilà: there is a path from $V_0$ to $V_\top$ in $G_F$ if and only if $F$ is satisfiable.

Now, the fact that your problem is NP-hard is not necessarily the end of the world, since, as you said yourself, you can still get good results with a simple brute-force strategy. There are two things that you could investigate:

• maybe your graphs have a particular structure that actually makes the problem solvable in polynomial time;
• if not, you could consider using a SAT solver (such as Glucose), with an encoding similar to this question, for instance. Sometimes this gives really good results and you don't even need to optimize the thing.