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

<p>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:</p>

<ul>
<li>maybe your graphs have a particular structure that actually makes the problem solvable in polynomial time;</li>
<li>if not, you could consider using a SAT solver (such as <a href="https://www.labri.fr/perso/lsimon/glucose/" rel="nofollow noreferrer">Glucose</a>), with an encoding similar to <a href="https://cs.stackexchange.com/questions/111410/sat-algorithm-for-determining-if-a-graph-is-disjoint">this question</a>, for instance. Sometimes this gives really good results and you don't even need to optimize the thing.</li>
</ul>

CC BY-SA 4.0
2019-07-03T21:24:39.813Z
2019-07-03T21:24:39.813Z
M.Monet
<p>I have a need for an algorithm which I can express as a reachability problem in a graph.</p>

<p>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).</p>

<h2>Problem Statement</h2>

<p>Consider an directed, connected, possibly cyclic graph <span class="math-container">$G=(V,E)$</span>.</p>

<p>Consider also a finite set of "indicators" <span class="math-container">$I$</span>, of a finite size. They are numbered <span class="math-container">$I_0 .. I_n$</span>.</p>

<p>Each indicator <span class="math-container">$I_i$</span> can take an integer value in the range <span class="math-container">$[0..v(i)]$</span>.</p>

<p>Each vertex can be labelled with one or more "assignations" of the form <span class="math-container">$I_i := v$</span>, with <span class="math-container">$v \in [0..v(i)]$</span>.</p>

<p>Exactly one vertex <span class="math-container">$V_0 \in V$</span> is distinguished as the "graph entry".</p>

<p>It is also considered that <span class="math-container">$V_0$</span> is labelled by <span class="math-container">$I_j := 0, \forall j \in [0..n]$</span> (<em>i.e. the "value" of all indicators is <span class="math-container">$0$</span> at the graph entry</em>).</p>

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

<p>We define (somewhat informally) a "valid" path in the graph as:</p>

<ul>
<li>being finite,</li>
<li>respecting the topology constraints in the graph,</li>
<li>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.</li>
</ul>

<p><em>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.</em></p>

<p><strong>Now my problem is the following:</strong> given a vertex <span class="math-container">$V_q \in V$</span>, does a valid path (in the sense defined above) exists from <span class="math-container">$V_0$</span> to <span class="math-container">$V_q$</span>?</p>

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

<h2>What I Did so Far</h2>

<p>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.</p>

<p>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.</p>

<graph-theory><graph-algorithms><program-analysis><flow-problems>
Computing the existence of a path in a code execution graph
oparisy
# Computing the existence of a path in a code execution graph

(Asked by: username_0 on 2019-07-03)

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.

**Tags:** graph-theory, graph-algorithms, program-analysis, flow-problems

---

## 1 answers

### Answer by username_1 on 2019-07-03. Score: 2

As such, your problem seems to be [NP-complete](https://en.wikipedia.org/wiki/NP-completeness). 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](https://en.wikipedia.org/wiki/Polynomial-time_reduction) from the [Boolean satisfiability problem](https://en.wikipedia.org/wiki/Boolean_satisfiability_problem) (SAT), which itself is NP-hard. The problem SAT takes as input a formula in [conjunctive normal form](https://en.wikipedia.org/wiki/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](https://en.wikipedia.org/wiki/Gadget_(computer_science)) $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](https://www.labri.fr/perso/lsimon/glucose/)), with an encoding similar to [this question](https://cs.stackexchange.com/questions/111410/sat-algorithm-for-determining-if-a-graph-is-disjoint), for instance. Sometimes this gives really good results and you don't even need to optimize the thing.


---

