How to prove that a constrained version of 3SAT in which no literal can occur more than once, is solvable in polynomial time?

Problem Detail: 

I'm trying to work out an assignment (taken from the book Algorithms - by S. Dasgupta, C.H. Papadimitriou, and U.V. Vazirani, Chap 8, problem 8.6a), and I'm paraphrasing what it states:

Given that 3SAT remains NP-complete even when restricted to formulas in which each literal appears at most twice, show that if each literal appears at most once, then the problem is solvable in polynomial time.

I attempted to solve this by separating the clauses into multiple groups:

1. Clauses which did not have any variable in common with the rest of the clauses
2. Clauses which had only 1 variable in common
3. Clauses which had 2 variables in common
4. Clauses which had all 3 variables in common

My reasoning was attempted along the lines that the # of such groups is finite (due to the imposed restriction of no literal being present more than once), and we could try to satisfy the most restricted group first (group 4) and then substitute the result in the lesser restricted groups (3, 2 and then 1), but I realized that this wasn't quite getting me anywhere, as this doesn't differ much from the case for the constrained version of 3SAT in which each literal can appear at most twice, which has been proven to be NP-complete.

I tried searching online for any hints/solutions, but all I could get was this link, in which the stated hint didn't make sufficient sense to me, which I'm reproducing verbatim here:

Hint: Since each literal appears at most once, convert this problem to 2SAT problem - hence polynomial time, if a literal $x_i$ appears in clause $C_j$ and complement of $x_i$ (i.e., $\overline{x_i}$) in clause $C_k$, construct a new clause clause $C_j \lor \overline{C_k}$.

Both $C_j$ and $C_k$ have three literals each - I didn't get how I should go about converting it into 2SAT by doing $C_j \lor \overline{C_k}$ (or $\overline{C_j \lor C_k}$ if I read it incorrectly).

Any help in either decrypting the hint, or providing a path I can explore would be really appreciated.

Asked By : TCSGrad

Answered By : Kaveh

Without loss of generality, we can assume that each variables appears exactly once positively and exactly once negatively (if a variable only appears once set its value to satisfy the clause and remove the clause). We can also assume that a variable does not appear in a clause more than once (if a variable appears both positively and negatively in a clause, then the clause is satisfied and can be removed). These will not alter the satisfiability.

Now use the resolution rule to eliminate the variables one by one (since each variable appears exactly once positively and once negatively this is a deterministic process). If at any point we obtain the empty clause the set of clauses is unsatisfiable, otherwise it is satisfiable. This is because:

• resolution is a complete propositional proof system (i.e. if a clause is logically implied by the set of clauses then it is derivable from the set of clauses using only the resolution rule),

• a set of clauses is unsatisfiable iff it logically implies the empty clause.

This algorithm will take polynomial time since each variable is resolved exactly once. In particular, each application of resolution will reduce the total number of clauses by one, so the number of clauses does not increase. For example, applying resolution to $(x \lor B) \land (\overline{x} \lor C) \land \dots)$ yields $(B \lor C) \land \dots$, which has one fewer clause than before resolution. In contrast, if you applied this to a 3SAT formula with no restriction on the number of appearances of each literal, applying resolution could cause the number of clauses to increase exponentially.

Best Answer from StackOverflow

Question Source : http://cs.stackexchange.com/questions/1852