2
$\begingroup$

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?

$\endgroup$
  • 1
    $\begingroup$ What is the equality graph of a 2-SAT instance? ​ ​ $\endgroup$ – user12859 Jun 13 '17 at 2:53
  • $\begingroup$ @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)$. $\endgroup$ – rus9384 Jun 13 '17 at 9:47
  • 1
    $\begingroup$ 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? ​ ​ ​ ​ $\endgroup$ – user12859 Jun 13 '17 at 10:07
  • $\begingroup$ @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. $\endgroup$ – rus9384 Jun 13 '17 at 10:16
  • 1
    $\begingroup$ How do you determine when you can put ​ x = y ? ​ ​ ​ (If your answer involves solving 2-SAT instances, then your "reduction" doesn't help.) ​ ​ ​ ​ ​ ​ ​ ​ $\endgroup$ – user12859 Jun 13 '17 at 10:30
1
$\begingroup$

This method doesn't work since you can't always pair clauses as in your example.

According to Wikipedia, 2SAT is NL-complete. In particular, this means that it is not in logspace unless L=NL, which is considered unlikely.

$\endgroup$
  • 1
    $\begingroup$ I said first pair of clauses. $(x \lor y) \land (\overline x \lor \overline y)$ implies $x = \overline y$. $\endgroup$ – rus9384 Jun 13 '17 at 8:35
  • $\begingroup$ I know that such clauses can be anywhere in the formula. All you need in this case is to apply search each time you take a clause. Runtime will be quadratic, such kind of space-time tradeoff. $\endgroup$ – rus9384 Jun 13 '17 at 21:51

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.