Show that the SAT Problem for CNF formulas with at most two occurences of each variable can be solved in polynomial time

Assuming, I have an arbitrary CNF Formula in which each variable has at most two occurences, how can I proof/show that this can be solved in polynomial time?

My first thoughts so far:

because each variable has at most two occurences, the formula contains at most 2*n literals, where n is the amount of different variables, and so the amount of clauses are also at most 2*n.

Not much, that's all I have so far :/

Consider a variable $x_i$. If it appears once, or if it appears twice but in the same polarity (i.e., both times as a positive literal or both times as a negative literal), then we can set it accordingly and satisfy all the clauses that contain it (more formally, any satisfying assignment can be converted into a satisfying assignment in which $x_i$ has this value).

The remaining case is the in which $x_i$ appears once positively and once negatively, that is, there are clauses $x_i \lor C$ and $\lnot x_i \lor D$. These two clauses are logically equivalent to the single clause $C \lor D$, which no longer contains $x_i$.

In this way, we keep eliminating the variables one by one, until we either eliminate all of them (in which case the formula is satisfiable), or we reach an empty clause (in which case the formula is unsatisfiable), which happens when both $C$ and $D$ are empty in the second case.

• Thank you so much. This solution seems so simple, I feel so dumb right now. Anyways, thanks, I appreciate it a lot. Jan 14 '18 at 15:43
• It's a pretty standard exercise - these things usually look simple in hindsight, though they can be hard to think of if you've never seen them before. Jan 14 '18 at 16:48
• Don't forget to upvote (if possible) and accept the answer if you think that it is useful and answers your question. Jan 14 '18 at 16:48
• It's not true that "x or C" and "not-x or D" are logically equivalent to "C or D". E.g. the assignment x=true, C=false, D=true makes the first pair of formulas true, but the second false. It's more accurate to say that the two are equisatisfiable, i.e. "(x or C) and (not-x or D)" is satisfiable iff "C or D" is.
– GMA
May 9 '19 at 17:55
• (Other than that your explanation is fine though.)
– GMA
May 9 '19 at 17:55