Homework 4 Optional Problems

In the 2SAT problem, you are given a set of clauses, where each clause is the disjunction of two literals (a literal is a Boolean variable or the negation of a Boolean variable). You are looking for a way to assign a value “true” or “false” to each of the variables so that all clauses are satisfied — that is, there is at least one true literal in each clause. For this problem, design an algorithm that determines whether or not a given 2SAT instance has a satisfying assignment. (Your algorithm does not need to exhibit a satisfying assignment, just decide whether or not one exists.) Your algorithm should run in 𝑂⁢(𝑚 +𝑛) time, where 𝑚 and 𝑛 are the number of clauses and variables, respectively. [Hint: strongly connected components.]

ANSWER: Quoting Wikipedia:

In computer science, 2-satisfiability, 2-SAT or just 2SAT is a computational problem of assigning values to variables, each of which has two possible values, in order to satisfy a system of constraints on pairs of variables. It is a special case of the general Boolean satisfiability problem, which can involve constraints on more than two variables, and of constraint satisfaction problems, which can allow more than two choices for the value of each variable. But in contrast to those more general problems, which are NP-complete, 2-satisfiability can be solved in polynomial time.

From the given formula, we construct a digraph 𝐺 where each vertex is a literal and each edge an implication between two literals. Each clause can be equivalently expressed as two implications: (𝑥 ∨𝑦) ≡(¬𝑥 ⟹ 𝑦) ≡(¬𝑦 ⟹ 𝑥)

The above implications should be intuitive; Given 𝑥 is 𝑓⁡𝑎⁢𝑙⁢𝑠⁢𝑒 (not 𝑡⁢𝑟⁢𝑢⁢𝑒), if the clause is to be 𝑡⁢𝑟⁢𝑢⁢𝑒, 𝑦 must be 𝑡⁢𝑟⁢𝑢⁢𝑒 (since the clause is a Boolean OR). Similarly, given 𝑦 is 𝑓⁡𝑎⁢𝑙⁢𝑠⁢𝑒, 𝑥 must be 𝑡⁢𝑟⁢𝑢⁢𝑒. Of course, we can also deduce the same from a truth table.

So, whenever there is a clause (𝑥 ∨𝑦) is the formula, we add two edges to 𝐺 corresponding to the equivalent implications. Then we run Kosaraju’s algorithm for finding strongly connected components (SCC). The algorithms runs in 𝑂⁢(𝑚 +𝑛) time. If a literal and its negation are in the same SCC, there is no possible assignment that can make both 𝑡⁢𝑟⁢𝑢⁢𝑒, thus, the formula is not satisfiable. We need to do a linear scan of each SCC to see if a literal and its negation are both in it; this can be done in 𝑂⁢(𝑚 +𝑛) time. Thus, the overall time complexity for determining satisfiability is 𝑂⁢(𝑚 +𝑛).

Having determined satisfiability, we can go further and find assignments that satisfy the formula. In order to do that, we take advantage of a property of Kosaraju’s algorithm: the SCCs are returned in topological order. That is, if a node 𝑢 is in the ith SCC, 𝑣 is in the jth one, with 𝑖 <𝑗, 𝑢 appears before 𝑣.

That tells us that, if we take those 𝑥 and ¬𝑥, the original formula can have the implication 𝑥 ⟹ ¬𝑥, but not in the other direction, otherwise, they wouldn’t be in separate SCCs.

Following the truth table for the implication operation, we want to avoid the case where 𝑡⁢𝑟⁢𝑢⁢𝑒 ⟹ 𝑓⁡𝑎⁢𝑙⁢𝑠⁢𝑒; the only case where the implication evaluates to 𝑓⁡𝑎⁢𝑙⁢𝑠⁢𝑒.

Therefore, if 𝑥 comes before ¬𝑥, we choose 𝑥 =𝑓⁡𝑎⁢𝑙⁢𝑠⁢𝑒, thus making (𝑥 ⟹ ¬𝑥) =𝑡⁢𝑟⁢𝑢⁢𝑒. On the other hand, if ¬𝑥 comes before 𝑥, we choose 𝑥 =𝑡⁢𝑟⁢𝑢⁢𝑒, thus making (¬𝑥 ⟹ 𝑥) =𝑡⁢𝑟⁢𝑢⁢𝑒.