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

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.

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.
• Summary of the wikipedia article: $a\lor B$ and $\lnot a\lor C$ imply $B\lor C$. (OK, not really a summary.) – rgrig May 15 '12 at 19:30