3
$\begingroup$

I want a SAT instance (in CNF) whose set of satisfying assignments are the connected induced subgraphs of a given input graph. A general solution would be helpful, but I really only need this when the input is a subgraph of a 2D grid graph.

Of course, I want the size of the SAT instance to be polynomial in the size of the input graph, so that rules out ideas like encoding every path between each pair of vertices.

Edit: The answer I needed and accepted allows the use of extra variables to formulate a SAT instance. Interestingly, @DavidEppstein shows that if no new variables are allowed, the required SAT instance cannot, in general, be found.

$\endgroup$
  • $\begingroup$ When you say "use a set of variable" what do you mean? The question is asking for a formula in which the set of variables is already specified: there must be one variable per vertex. $\endgroup$ – David Eppstein Jan 7 '16 at 19:49
4
$\begingroup$

Constructions are easier in the uniform setting. When doing reductions to SAT express the problem you want to reduce to SAT as a SO$\exists$ formula (by Fagin's theorem in descriptive complexity SO$\exists$ captures all queries computable in NP). Then convert it into a propositional formula using propositional translation. Then convert that to a CNF using Tseytin transformation:

Let the input $G$ be given by the number of vertices $n$ and the edge relation $E$. To simplify things let's assume that each vertex has an edge to itself, i.e. $E(v,v)$ for all $v$. Let $S$ be a unary predicate that determines the set of selected vertices. SO$\exists$ formula for your problem: $\varphi(G,S)$ is $$\forall s,t \in S \ \exists P \text{ ``$P$ is a path from $s$ to $t$ in $G[S]$''}$$ To express that $P$ is a path from $v$ to $u$ in $G[S]$ we think of $P$ as an ordered list of size $n$ of vertices, i.e. $P$ is a function from $[n]$ to set of selected vertices: $$\forall i \in [n] \ \exists v \in S \ P(i,v) \land \forall i \in [n] \forall v\neq u \in [n] (\lnot P(i,v) \lor \lnot P(i,u))$$ and it is a path from $s$ to $t$: $$P(1,s) \land P(n,t) \land \forall i \in [n-1] \ \forall v,u \left( P(i,v) \land P(i+1,u) \to E(v,u) \right)$$

Now we turn it into a propositional formula using the propositional translation. We use $q_v$ to express vertex $v$ is in $S$, i.e. $v \in S$. We use $p_{iv}$ to express $P(i,v)$. Note that when translating we need to use different variables for expressing the path between each pair. It is really $p_{iv}^{st}$.

$$\bigwedge_{s,t \in [n]} \left(q_s \land q_t \to ... \right)$$

where $...$ is the conjunction of

$$\bigwedge_{i\in [n]} \bigvee_{v \in [n]} (q_v \land p_{iv}^{st}) \land \bigwedge_{i\in[n]} \bigwedge_{v\neq u \in [n]} (\lnot p_{iv}^{st} \lor \lnot p_{iu}^{st})$$ and $$p_{1s}^{st} \land p_{nt}^{st} \land\bigwedge_{i \in [n-1]} \bigwedge_{v,u \in [n]}\left( p_{iv}^{st} \land p_{i+1u}^{st} \to e_{vu} \right)$$

This has polynomial size in $n$. To make it CNF perform the reduction from SAT to CNF-SAT using Tseytin transformation: use new variables (called extension variables) for each subformula and expressing the relationship between the variable for each subformula and the variables for its intimidate children in the formula tree and that the variable for the root subformula is true.

The result is a polynomial-size CNF formula $\psi(\vec{e}, \vec{q}, \vec{p}, \vec{z})$ with variables $\vec{e}$, $\vec{q}$, $\vec{p}$, and a bunch of extension variables $\vec{z}$ (for subformulas).

Fix $\vec{e}$ based on the given $G$. Any assignment $\tau$ to $\vec{q}$, $\vec{p}$, $\vec{z}$ that satisfies $\psi$ gives a connected subgraph $S = \{v \mid \tau(q_v) = \top \}$ of $G$ and for any connected subgraph of $G$ there is such an assignment.

$\endgroup$
  • $\begingroup$ looks great. I am a bit hazy on the part after "extension variables". Is there a type-O at "intimidate"? immediate? Also, complete induced subgraph in last par. It's late here, but you answer looks useful. $\endgroup$ – Alejandro Jan 7 '16 at 21:28
  • $\begingroup$ @Alejandro, yes, look at the Wikipedia article for Tseytin transformation. It explains how to turn a formula into a CNF in more detail (or any textbook that explain why CNF-SAT (or 3-SAT) is NP-complete). $\endgroup$ – Kaveh Jan 7 '16 at 21:29
  • 1
    $\begingroup$ If the problem is being interpreted this way, as allowing extra variables, then it's definitely not research level: it's a basic and well-known fact that every NP problem instance can be transformed into a polynomial-sized CNF formula such that the yes-instance to the instance are the ones for which the extra variables can be given a satisfying assignment. $\endgroup$ – David Eppstein Jan 7 '16 at 22:47
  • $\begingroup$ @David, yes. I think it also follow from constant depth circuit lower bounds that it cannot be done with polysize constant depth circuits without extra variables. $\endgroup$ – Kaveh Jan 7 '16 at 23:36
  • 1
    $\begingroup$ I can see that the answer is obtained by straightforward methods, but whether or not it is research-level depends on your perspective. I need this solution for a SAT-solver-aided construction of gadgets for an entirely different reduction, and for whatever reason I was blinded to it until @Kaveh explained it. So thanks! (I realise it ended up being pretty "textbook"...) $\endgroup$ – Alejandro Jan 8 '16 at 9:47
5
$\begingroup$

It's not possible if the variables are restricted to be only the given ones for the graph vertices. Consider a graph $G$ that has $2n+2$ vertices: $x$, $u_i$, $v_i$, and $y$ for $1\le i\le n$, formed by the union of $n$ edge-disjoint paths $x$--$u_i$--$v_i$--$y$. Also consider only the subgraphs that include both $x$ and $y$: if the whole graph has a small CNF formula for connected subgraphs, then so does this subset of subgraphs, obtained by setting the variables for $x$ and $y$ to true and then simplifying the formula.

The connected subgraphs that include both $x$ and $y$ do have a very simple $2$-DNF formula: $$\bigvee\limits_{i=1}^n(u_i\wedge v_i).$$ However, when you convert this to its (unique) CNF form, it has $2^n$ terms (one for each way of excluding either $u_i$ or $v_i$ from the subgraph, for each $i$). So no polynomial-size CNF formula exists.

$G$ is not a grid graph but the same construction can easily be embedded into a grid by expanding $x$ and $y$ into larger connected subsets of grid points. As above, the whole graph can't have a small CNF formula, because if it did then you'd also have a small CNF formula for the connected subgraphs that include all the grid points representing $x$ and $y$, but we can write down the formula for this subset of the subgraphs and it does not have polynomial size.

$\endgroup$
  • $\begingroup$ I may have accepted prematurely. @Kaveh's earlier suggestion to look at HamPath (e.g., math.stackexchange.com/questions/1138105/…) suggests we might use auxiliary variables to build $wz$-paths for $w,z\in V$, or another structure like a spanning tree. I agree that if you limit yourself to the variables in your answer, above, you get a large formula... Anyway, these are good leads. $\endgroup$ – Alejandro Jan 7 '16 at 20:17

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.