<p>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:</p>
<ul>
<li><p>Remove clauses containing both a literal and its negation.</p>
</li>
<li><p>If some variable occurs only positively or only negatively, remove the corresponding clauses (i.e., set the occurring literal to true).</p>
</li>
<li><p>Pick any variable that occurs both positively and negatively, and resolve the two clauses where it occurs (i.e., remove <span class="math-container">$C\cup\{x\}$</span> and <span class="math-container">$D\cup\{\neg x\}$</span>, and replace them with <span class="math-container">$C\cup D$</span>).</p>
</li>
</ul>
<p>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).</p>

CC BY-SA 4.0
2022-02-11T11:13:34.820Z
Thank you very much.
Yuhang Bai
CC BY-SA 4.0
2022-02-11T16:48:51.303Z
Just for the references, it is known as Davis-Putnam algorithm (https://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.
holf
CC BY-SA 4.0
2022-02-11T17:15:41.057Z
@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.
Emil Jeřábek
CC BY-SA 4.0
2022-02-11T18:30:09.230Z
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.
holf
CC BY-SA 4.0
2022-02-11T18:54:49.867Z
@holf Ah ok, that makes sense.
Emil Jeřábek
CC BY-SA 4.0
2022-02-11T10:46:22.330Z
2022-02-11T11:03:14.553Z
2022-02-11T11:03:14.553Z
Emil Jeřábek
<p>It is well known that 3SAT remains NP-complete if every variable occurs exactly twice positively, exactly once negated.</p>
<p>then, does 3SAT remain NP-complete if every variable occurs exactly once positively, exactly once negated?</p>

<np-hardness><sat>
The complexity of 3SAT
Yuhang Bai
# The complexity of 3SAT

(Asked by: username_0 on 2022-02-11)

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?

**Tags:** np-hardness, sat

---

## 1 answers

### Answer by username_1 on 2022-02-11. Score: 8 | Accepted answer

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).

> **Comments:**
> **username_0**: Thank you very much.  
> **username_2**: Just for the references, it is known as Davis-Putnam algorithm (https://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.  
> **username_1**: @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.  
> **username_2**: 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.  
> **username_1**: @holf Ah ok, that makes sense.  

---

