# 3SAT and directed graph

Given a 3SAT instance (a Boolean expression in three conjunctural normal form), we draw a directed graph, where for each Boolean variable $$x_{i}$$ we have the nodes $$x_{i}$$ and $$!x_{i}$$; for each clause, for example $$\left(x_{a} \vee x_{b} \vee x_{c}\right)$$, we draw the following arrows $$!x_{a}x_{b}$$, $$!x_{a}x_{c}$$, $$!x_{b}x_{a}$$, $$!x_{b}x_{c}$$, $$!x_{c}x_{a}$$, $$!x_{c}x_{b}$$.

Is it possible understand from the graph if there is a variable $$x_{i}$$ such that $$x_{i}\Leftrightarrow !x_{i}$$ ($$!x_{i}$$ is $$not\left(x_{i}\right)$$)?

• Your instance implies $x_i \Leftrightarrow \overline{x_i}$ iff it is unsatisfiable. Given that SAT is NP-complete, there is probably no easy way to tell. – Yuval Filmus Sep 19 '20 at 22:12
• You might be interested in the Resolution proof system. – Yuval Filmus Sep 19 '20 at 22:12

In 2-SAT, $$(x_a \vee x_b)$$ may indeed be considered as 2 implications, $$\neg x_a \Rightarrow x_b$$ and $$\neg x_b \Rightarrow x_a$$.
The problem is that $$(x_a \vee x_b \vee x_c)$$ is not equivalent to any of the 6 implications like $$\neg x_b \Rightarrow x_a$$, as $$x_c$$ is sufficient to satisfy the clause. You may eventually have $$(\neg x_a \wedge \neg x_b) \Rightarrow x_c$$ or $$\neg x_a \Rightarrow (x_b \vee x_c)$$, but neither let you build such implication graph.
• Optidad, you are right, but, in my opinion, we can write the implication $\neg x_{a} \Rightarrow \left(x_{b}\vee x_{c}\right)$ in the directed graph as follow. We add to the graph a double node db, that is a node with one ingoing arrow and two outgoing arrows. Then we draw the arrow from $\neg x_{a}$ to db, the arrow from db to $x_{b}$ and the arrow from db to $x_{c}$. After we have added to the graph all the implications of the given 3SAT, we can find the implication $x_{a} \Rightarrow \neg x_{a}$, if it exists, as follow: (see next comment)... – Mario Giambarioli Dec 21 '20 at 10:51
• We make a back breadth first search in the graph from $\neg x_{a}$, where back means that the search goes from the node $a$ to the node $b$ if and only if there is an arrow from $b$ to $a$. If the search meets a double node dn, the search must visit dn from both outgoing arrows of dn before visit the node that is on the ingoing arrow of dn. In such a way, if the search from $\neg x_{a}$ reaches $x_{a}$, this means that $x_{a} \Rightarrow \neg x_{a}$. In the same way we can find if $\neg x_{a} \Rightarrow x_{a}$ and therefore if $x_{a} \Leftrightarrow \neg x_{a}$. – Mario Giambarioli Dec 21 '20 at 10:53
• @Mario_Giambarioli Just try it on a simple case of 3-SAT, you will realise quickly that it does not work. First, there is no mean to go reversly in an implication graph as $a \Rightarrow b$ is independant of $b \Rightarrow a$. Also, you are not able to treat the statement "OR" to use such double nodes. – Optidad Jan 6 at 7:59