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)$)?

  • 1
    $\begingroup$ 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. $\endgroup$ Sep 19, 2020 at 22:12
  • $\begingroup$ You might be interested in the Resolution proof system. $\endgroup$ Sep 19, 2020 at 22:12

1 Answer 1


I think you are trying to build the 2-SAT implication graph for 3-SAT.

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.

  • $\begingroup$ 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)... $\endgroup$ Dec 21, 2020 at 10:51
  • $\begingroup$ 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}$. $\endgroup$ Dec 21, 2020 at 10:53
  • $\begingroup$ @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. $\endgroup$
    – Optidad
    Jan 6, 2021 at 7:59

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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