0
$\begingroup$

Is Tarjan's algorithm capable of finding satisfying assignment to any digraph consists of variables (vertices) and implications (edges)? I know that it solves implication graphs constructed by 2SAT clauses, but I wonder if the algorithm can handle the digraphs which cannot be expressed as 2SAT clauses. Let me clarify this by the following examples:

(a+b)(~b+c) translates to the following (~a -> b), (~b -> a), (b -> c), (~c -> ~b) It is OK. But how about the following implications: (a -> b), (b -> ~c) There is obviously no corresponding set of 2SAT instances. Does Tarjan's algorithm find a satisfying assignment to this?

|cite|improve this question
$\endgroup$
  • $\begingroup$ The clauses $(a \to b), (b \to \lnot c)$ are Horn Clauses. $\endgroup$ – hengxin Jun 20 '15 at 14:29
  • $\begingroup$ They are, but they also might not be. Does it make any difference? $\endgroup$ – Husrev Jun 20 '15 at 15:28
1
$\begingroup$

You have a faulty premise. There is a 2SAT instance corresponding to $(a \implies b) \land (b \implies \neg c)$. Just note that $x \implies y$ is equivalent to $\neg x \lor y$. Then you can transform the original formula to $(\neg a \lor b) \land (\neg b \lor \neg c)$, which is obviously a 2SAT instance.

That algorithm you refer to can solve 2SAT, but it can't solve anything stronger as is. However, there are related graph-based algorithms to test satisfiability of arbitrary conjunctions of Horn clauses.

|cite|improve this answer
$\endgroup$
  • $\begingroup$ Your 2SAT instance has extra implications, $(\neg b \implies \neg a)$ and $(c \implies \neg b)$. $\endgroup$ – Kyle Jones Jun 20 '15 at 18:06
  • $\begingroup$ As Kyle Jones says, (~a+b)(~b+~c) has additional implications. I'm talking about the case where only half of the implications produced by 2SAT instances are given. $\endgroup$ – Husrev Jun 20 '15 at 18:51
  • $\begingroup$ @KyleJones, no, those are not "extra" implications. $(\neg b \implies \neg a)$ is implied by (in fact, equivalent to) $(a \implies b)$ -- it is the contrapositive. Same for $(c \implies \neg b)$. My 2SAT instance is exactly equivalent to the formula Husrev provided. Try finding an assignment that makes my 2SAT instance true for Husrev's formula false, or vice versa -- I think you'll see what I mean. $\endgroup$ – D.W.♦ Jun 20 '15 at 19:18
  • $\begingroup$ @Husrev, I suspect you might have misunderstood how boolean formula work. See my comment to Kyle Jones. $\endgroup$ – D.W.♦ Jun 20 '15 at 19:20
  • 1
    $\begingroup$ @Husrev, I think your basic confusion is over what problem the algorithm solves. Your question suggests you are thinking about this the wrong way. The phrase "satisfying assignment of a digraph" has no meaning; that isn't defined. Instead, we talk about the satisfying assignment of a formula. The graph and the algorithm is only the means to an end. So, you need to be clear in your mind about what formula you are testing the satisfiability of. There is no way to have a boolean formula that includes $a \implies b$ without also implying the contrapositive. $\endgroup$ – D.W.♦ Jun 21 '15 at 1:06

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.