Reduction from 2-SAT to 2-XOR-SAT?

2-SAT is unsatisfiable iff it contains unsatisfiable XOR-2-SAT.

So, first, we just need to combine every clause that contains share same variables (both of them). Then, all of those which remain uncombined are "uninteresting" (don't affect satisfiability).

Example:

$\Phi = (x \lor y) \land (\overline x \lor \overline y) \land (x \lor \overline z)\land(\overline x \lor z)\land (\overline y \lor z)\land (y \lor \overline z)\land (z \lor t)$

Now I can replace this formula by equisatisfiable (under log-space reduction):

$\Phi' = (x \oplus y)\land(x \oplus \overline z)\land(y \oplus \overline z)$

As you can see, clause $(z\lor t)$ was removed as "uninteresting".

Ah, well, I need to see if there are cycles in implication graph. So, finding a cycle in directed graph that contains two given vertices is $\mathsf{NL}$-complete problem, right?

• What is the equality graph of a 2-SAT instance? ​ ​ – user12859 Jun 13 '17 at 2:53
• @RickyDemer, if two literals are equal, then they are connected to each other in undirected equality graph. In my example there are edges $(x, \ \overline y), (x,\ z), (y,\ z)$. – rus9384 Jun 13 '17 at 9:47
• That means you get an equality graph from an assignment, not from a 2-SAT instance. ​ Accordingly, what is your reduction from 2-SAT to USTCONN? ​ ​ ​ ​ – user12859 Jun 13 '17 at 10:07
• @RickyDemer, but you can't put $x = y$. Otherwise one of two clauses will be unsatisfied. If you solve it with implication graph, you can solve it in $\mathcal{O}(\log^2 n)$ memory due to Savitch's theorem. But equality graph is undirected and I think it should imply that it's possible to solve 2-sat $\mathcal{O}(\log n)$ memory. – rus9384 Jun 13 '17 at 10:16
• How do you determine when you can put ​ x = y ? ​ ​ ​ (If your answer involves solving 2-SAT instances, then your "reduction" doesn't help.) ​ ​ ​ ​ ​ ​ ​ ​ – user12859 Jun 13 '17 at 10:30

• I said first pair of clauses. $(x \lor y) \land (\overline x \lor \overline y)$ implies $x = \overline y$. – rus9384 Jun 13 '17 at 8:35