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.

| cite | improve this answer | |
  • $\begingroup$ Thank you so much. This solution seems so simple, I feel so dumb right now. Anyways, thanks, I appreciate it a lot. $\endgroup$ – Eden Hassard Jan 14 '18 at 15:43
  • $\begingroup$ 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. $\endgroup$ – Yuval Filmus Jan 14 '18 at 16:48
  • $\begingroup$ Don't forget to upvote (if possible) and accept the answer if you think that it is useful and answers your question. $\endgroup$ – Yuval Filmus Jan 14 '18 at 16:48
  • $\begingroup$ 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. $\endgroup$ – GMA May 9 '19 at 17:55
  • $\begingroup$ (Other than that your explanation is fine though.) $\endgroup$ – GMA May 9 '19 at 17:55

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.