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$
8
  • 1
    $\begingroup$ What is the equality graph of a 2-SAT instance? ​ ​ $\endgroup$
    – user12859
    Jun 13, 2017 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, 2017 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, 2017 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, 2017 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, 2017 at 10:30

1 Answer 1

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$
4
  • 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, 2017 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, 2017 at 21:51
  • $\begingroup$ @Yuval Filmus Do you mean it is not in L unless L=NL? I don't see the relation between LSPACE and NL-completeness. $\endgroup$
    – Sid Meyers
    Jul 9, 2021 at 8:10
  • 1
    $\begingroup$ L stands for logspace. $\endgroup$ Jul 9, 2021 at 9:37

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.