# Can Tarjan's SCC algorithm find satisfying assignment to just 'any' digraph?

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?

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

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.
• Your 2SAT instance has extra implications, $(\neg b \implies \neg a)$ and $(c \implies \neg b)$. – Kyle Jones Jun 20 '15 at 18:06
• @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. – D.W. Jun 20 '15 at 19:18
• @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. – D.W. Jun 21 '15 at 1:06