patternMinor
Show that the SAT Problem for CNF formulas with at most two occurences of each variable can be solved in polynomial time
Viewed 0 times
satshowproblemthecaneachpolynomialwithcnfoccurences
Problem
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 2n literals, where n is the amount of different variables, and so the amount of clauses are also at most 2n.
Not much, that's all I have so far :/
My first thoughts so far:
because each variable has at most two occurences, the formula contains at most 2n literals, where n is the amount of different variables, and so the amount of clauses are also at most 2n.
Not much, that's all I have so far :/
Solution
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.
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.
Context
StackExchange Computer Science Q#86730, answer score: 5
Revisions (0)
No revisions yet.