I'm not sure on how to express that in a very formal and absolutly correct way so I hope it is still understandable. I have found this algorithm and been struggling for a while proving it does or doesn't solve 3-SAT, maybe one of you can help find an example where it fails. It is inspired by this 2-SAT algorithm and is, I believe, polynomial time in the amount of variables, hence there probably exists a example where it fails. The idea is to represent higher order relations in the graph to be able to represent clauses that are made of a combination of 3 variables.
Suppose we have $m$ clauses and $n$ variables $\{x_1,\dots,x_n\}$ in the usual setting, without loss of generality we can assume all the closes are made of exactly $3$ variables, that may not be distinct. A close $a\lor b\lor c$ where $a$, $b$, $c$ can be any variable or a variable negation can be rewritten in equivalent ways as \begin{align*} &\lnot a\rightarrow (\lnot b\rightarrow c)&&\lnot (\lnot b\rightarrow c)\rightarrow a\\ &\lnot b\rightarrow (\lnot a\rightarrow c)&&\lnot (\lnot a\rightarrow c)\rightarrow b\\ &\lnot c\rightarrow (\lnot a\rightarrow b)&&\lnot (\lnot a\rightarrow b)\rightarrow c\\ \end{align*} using only implications and negation. From all the variables and clauses we construct a graph. For any variables $x_i$ and $x_j$ with $i<j$, then we have all the vertex labeled
$x_i$, $x_j$, $\lnot x_i$ and $\lnot x_j$
$x_i\rightarrow x_j$, $\lnot x_i\rightarrow x_j$, $x_i\rightarrow \lnot x_j$ and $\lnot x_i\rightarrow \lnot x_j$
$\lnot(x_i\rightarrow x_j)$, $\lnot(\lnot x_i\rightarrow x_j)$, $\lnot(x_i\rightarrow \lnot x_j)$ and $\lnot(\lnot x_i\rightarrow \lnot x_j)$
We also add the vertex labeled $0$ and $1$, they represent false and true and if there is an edge $1\rightarrow a$ or $\lnot a \rightarrow 0$, then $a$ needs to be true. The total amount of vertices is $2+2n+8{n\choose 2}=4n^2+6n+1$. Regarding edges, they represent logical implication and so before taking a look at clauses the graph should contain some edges such as $\lnot (a\rightarrow b) \rightarrow \lnot b$, $\lnot a \rightarrow (a\rightarrow b)$ but it turns out that only the edge from $0$ to $1$ and those from $a$ to $a$ (for any vertex $a$) are needed when taking into account the algorithm. The $m$ clauses all add exactly $6$ edges mentioned above to the graph and this is the initial graph.
The algorithm try to see if there exists a vertex (that may be the composition of $2$ variables) that is strongly connected to it's negation but for now it is not possible since edges only goes from vertex of the form $\lnot(a\rightarrow b)$ to $\lnot a$ and from $a$ to $\lnot a \rightarrow b$ but we can combine two edges into an other one to expend knowledge that can be deduced. Suppose we have that for some vertex $a$, $b$, $c$ and $d$ the edges from $a$ to $b$ and from $c$ to $d$, then we can deduce the two implications
- $(a\land c)\rightarrow(b\land d)$
- $(a\lor c)\rightarrow(b\lor d)$
where the $\land$ and $\lor$ operator are the usual logical and and or. If the logical values of $(a\land c)$ and of $(b\land d)$ both matches with the logical value of two vertices then we add the corresponding edge to the graph, the same happen for the second line. $a\land b$ is the combination of at most $4$ variables and so we can extends the tables of values it can take (as a function of the variables it is made of) which is at most $16$ different possibilities, then we can compare those the one we would obtain with any vertex of the graph that involve the same variables ($2$ by $2$, $1$ by $1$ or even the vertex $0$ or $1$). This operation can be done in constant time.
The algorithm is just an iterative application of these edges deductions, suppose we have the directed graph $G=(V,E)$ in input then a pseudo code for the algorithm is
- $S\leftarrow \emptyset$
- $R\leftarrow \{\{e,e'\} | (e,e')\in E\times E, e\neq e'\}$
- while $R\neq \emptyset$
- $E'\leftarrow \emptyset$
- for all $\{(a,b),(c,d) \}\in R$
- if $a\land c\in G$ and $b\land d\in G$ : $E'\leftarrow E' \cup \{(a\land c,b\land d)\}$
- if $a\lor c\in G$ and $b\lor d\in G$ : $E'\leftarrow E' \cup \{(a\lor c,b\lor d)\}$
- $S\leftarrow S\cup R$
- $E\leftarrow E\cup E'$
- run BFS on $G=(V,E)$ and add all deduced edges that correspond to paths in $E'$
- $R\leftarrow \{\{e,e'\} | (e,e')\in E\times E', e\neq e'\}\setminus S$
- return true if $(1,0)\in E$ and false otherwise
The BFS line is just running BFS and adding to $E'$ an edge from $a$ to $b$ if there exists a path from $a$ to $b$, this can be optimized by remembering all visited edges from iterations to iterations of this BFS but it doesn't matter since BFS is polynomial in the number of vertex and hence of variable.
The set $S$ contains the pair of edges we have already tried to combine and $R$ is the set of new pair of edges we could combine, since we iterate until we don't have anything else to combine, the cardinality of $S$ is strictly increasing at each iterations and so the worst case is an increase by one at each steps. The amount of edges of the graph is at most $|V|(|V|-1)=O(n^4)$ and so the amount of combination of two different edge we can have is $O(n^8)$ and this is the complexity of the number of time we do any of the line inside the inner and outer loop, hence I think that this algorithm runs in polynomial time.
The return condition is equivalent to the one of having a vertex and its logical negation strongly connected, indeed if for some vertex $a$ we have $a\rightarrow \lnot a$ then we combine it with the edge $\lnot a\rightarrow \lnot a$ to get $1=a\lor \lnot a \rightarrow \lnot a \lor \lnot a = \lnot a$, if we also have $\lnot a \rightarrow a$, we can combine it with $\lnot a\rightarrow \lnot a$ to get $\lnot a = \lnot a \land \lnot a \rightarrow \lnot a\land 0 = 0$ and hence, combining the two we can deduce a path from $1$ to $0$.
Here I list some of the things the algorithm does or preserves. First observe that there should be a lot of edges in the graph in the beginning such as $a\rightarrow (\lnot a\rightarrow b)$ since they are tautologies, those edges are always deduced at the first iteration of the algorithm since we can combine the two edges $b \rightarrow b$ and $0\rightarrow 1$ with $\land$ to get that $0\rightarrow b$ and then we can combine this one with $a\rightarrow a$ using $\lor$ to get that $a\rightarrow (\lnot a\rightarrow b)= a\lor b$.
If there is an edge from $1$ to $a\rightarrow b$ then the later is considered true and we would like to add an edge from $a$ to $b$ (which are in the graph), this is done combining the edge with $a\rightarrow (\lnot a\rightarrow b)$ using $\land$ to get that $a\land 1 = a\rightarrow b=(\lnot a\rightarrow b)\land (a\rightarrow b)$, the converse is also true, if we have an edge from $a$ to $b$ and they are either variable or negation of variable, then combining them using $\lor$ gets us $1\rightarrow (a\rightarrow b)$.
At the end of the while loop (or begining) it is always true that if we have an edge from any vertex $a$ to $b$, then we also have an edge from $\lnot b$ to $\lnot a$, indeed this property is true in the begining of the algorithm and if we combine $a\rightarrow b$ and $c\rightarrow d$, then we also combine $\lnot b\rightarrow \lnot a$ and $\lnot d\rightarrow \lnot c$ to get the two wanted edges.
If we have the two clauses $(a\lor b\lor c)\land(\lnot a\lor d \lor e)$, then there will be an edge from $(\lnot b\rightarrow c)$ to $(\lnot d\rightarrow e)$, this is seen easily from the initial edges plus the BFS. In particular $(a\lor b\lor c)\land(\lnot a\lor b \lor c)$ will add an edge from $\lnot b$ to $c$.
Since we don't add any implication that may be false, then of course if the algorithm returns false, then the 3-SAT was not satisfiable so the only thing to prove or disprove is that if the algorithm return true, then the 3-SAT has solution. My guess is that there is probably a example of 3-SAT that is not satisfiable where my algorithm return true but I failed to find one.