It is well known that 3SAT remains NP-complete if every variable occurs exactly twice positively, exactly once negated.
then, does 3SAT remain NP-complete if every variable occurs exactly once positively, exactly once negated?
Add a comment
|
1 Answer
$\begingroup$
$\endgroup$
5
Satisfiability of CNFs where each variable occurs at most twice is easily seen to be computable in P. Repeat in any order the following steps, each of which decreases the number of variables, and preserves satisfiability:
Remove clauses containing both a literal and its negation.
If some variable occurs only positively or only negatively, remove the corresponding clauses (i.e., set the occurring literal to true).
Pick any variable that occurs both positively and negatively, and resolve the two clauses where it occurs (i.e., remove $C\cup\{x\}$ and $D\cup\{\neg x\}$, and replace them with $C\cup D$).
If neither step is no longer applicable, no variable can occur in the CNF any longer, which means that either the CNF is empty (whence true, i.e., satisfiable), or it consists of the empty clause (whence it is false, i.e., unsatisfiable).
answered Feb 11, 2022 at 10:46
-
-
2$\begingroup$ Just for the references, it is known as Davis-Putnam algorithm (en.wikipedia.org/wiki/Davis%E2%80%93Putnam_algorithm) and is one of the first proposed algorithm to solve SAT. It works even if the formula does not have the property mentioned in the question, but then it may take exponential time to terminate. $\endgroup$– holfCommented Feb 11, 2022 at 16:48
-
$\begingroup$ @holf In a general SAT algorithm, you cannot immediately remove the two clauses being resolved (which is what makes the algorithm here terminate in a linear number of steps), as this does not preserve (un)satifiability if $x$ may be present in other clauses: e.g., $\{\{x,y\},\{\neg x,\neg y\},\{x,\neg y\},\{\neg x,y\}\}$ is unsatisfiable, but after resolving the first two clauses, $\{\{y,\neg y\},\{x,\neg y\},\{\neg x,y\}\}$ is satisfiable. $\endgroup$ Commented Feb 11, 2022 at 17:15
-
1$\begingroup$ Yes, I was referring to the real Davis-Putnam algorithm where you indeed have to compute the resolvent for every pair $C,D$ of clauses containing $x$ and $\neg x$ respectively before removing clauses containing variable $x$. Your algorithm is exactly Davis-Putnam on this particular instances since there is at most one such pair but it is true that the general algorithm is a bit more involved. $\endgroup$– holfCommented Feb 11, 2022 at 18:30
-
$\begingroup$ @holf Ah ok, that makes sense. $\endgroup$ Commented Feb 11, 2022 at 18:54