# 3-SAT with 3 variable occurences

3-SAT with at most 3 occurences per variable is $\mathsf{NP}$-hard.

Now I'll try to solve it using these:

1. Theorem: SAT where all clauses have length 3 and variables occur 3 times, is satisfiable.
2. Double propagation. If there is a clause $(a\lor b)$ and no clause $(\overline a\lor\overline b)$: change all occurences of $\overline a$ by $b$ and $\overline b$ by $a$. Also, remove clause $(a\lor b)$. This will result in two occurences for $a$ and $b$.
3. If there is a pair of clauses $(a\lor b)\land(\overline a\lor\overline b)$, replace occurence (there will be only one) of $b$ to $\overline a$. Remove that pair of clauses. This will result in two occurences of $a$ and no occurences of $b$.

Using this technique we either must get an empty clause or all clauses will have length 3 and formula will be satisfiable. It is also possible that formula will become 2-SAT.

Can this even work?

• When you come up with an idea, I encourage you to try to implement your idea and run it on lots of test cases (compare its output to a known-good SAT solver) and see if it seems to work, before asking people here to check whether your idea is correct.
– D.W.
Sep 5, 2017 at 21:21

Take any unsatisfiable $3$-SAT formula (without restriction on the number of variable appearances) and perform the standard reduction to a formula where each variable occurs at most three times. That is, for each variable $X$ that occurs $k>3$ times, replaces the occurrences respectively with $X_1, \dots, X_k$ and add the new clauses

$$(\overline{X_1}\lor X_2) \land(\overline{X_2}\lor X_3) \land \dots \land (\overline{X_{k-1}} \lor X_k) \land (\overline{X_k}\lor X_1)$$

to ensure that $X_1, \dots, X_k$ have the same value in any satisfying assignment.

Now, we have the clause $\overline{X_1}\lor X_2$ but not $X_1\lor\overline{X_2}$ so we can use your second step, taking $A=\overline{X_1}$ and $B=X_2$. So we must delete the first clause and replace any instance of $X_1$ with $X_2$ and any instance of $\overline{X_2}$ with $\overline{X_1}$. This replaces the clauses above with

$$(\overline{X_1}\lor X_3) \land (\overline{X_3}\lor X_4) \land \dots \land (\overline{X_{k-1}} \lor X_k) \land (\overline{X_k}\lor X_2)\,,$$ i.e., $$(X_1\rightarrow X_3)\land (X_3\rightarrow X_4) \land \dots \land (X_{k-1}\rightarrow X_k)\land (X_k\rightarrow X_2)\,.$$

This no longer requires all the the $X_i$ variables to have the same value. There are formulas that will become satisfiable when you make this transformation.

But, further, we can now apply the transformation again to the clause $\overline{X_1}\lor X_3$, resulting in $$(\overline{X_1}\lor X_4) \land (\overline{X_4}\lor X_5)\land\dots\land (\overline{X_{k-1}} \lor X_k) \land (\overline{X_k}\lor X_2)\,.$$ Note that the variable $X_3$ has completely disappeared and can take any value. Iterating, we see that all the clauses relating $X_1, \dots, X_k$ disappear!

What have we done? We've taken a formula that mentioned $X$ more than three times and replaced these occurrences with successive new variables $X_1, \dots, X_k$, plus the constraint that all these new variables must take the same value. We then deleted all the constraints, so $X_1, \dots, X_k$ can take any value at all, independently of each other and, by the way, each of the variables $X_1, \dots, X_k$ now only occurs once. So, if we started with an unsatisfiable formula in which every variable occurred more than three times, we end up with a formula where every variable occurs exactly once. That formula is always satisfiable.

• Wait, last clause must be $(\overline X_k\lor X_2)$. The rules are for positive literals and if they are not positive, we change polarities. Sep 5, 2017 at 17:51
• @rus9384 Good point. Actually, that makes the answer much more concrete. Let me fix it... Sep 5, 2017 at 18:10
• @rus9384 Done: the transformation now makes every formula satisfiable. Sep 5, 2017 at 18:27
• I think the reason is another. If we have relations $a\rightarrow c$ and $b\rightarrow c$, we can't put $\overline a$ instead of $\overline c$ unless $a\rightarrow b$. But what if each variable appears in 2-clause at most once? Then the rule works? Sep 5, 2017 at 20:19
• @rus9384 I think it's time for me to say "Figure it out yourself." Basically, you're proposing polynomial-time algorithms for 3-SAT. If such simple clause manipulations were enough to prove that P=NP, somebody would surely have done it by now. The way research works is that you test your own ideas and, if your ideas are too difficult for you to test, you either get better at testing or you try to research something where you're already good enough. Sep 5, 2017 at 20:44

You can show a reduction in polynomial time from the standard 3-SAT problem where the number of variable occurrences are unrestricted to the specific version of 3-SAT with utmost three occurrences per variable in order to prove it's NP-Hard. This reduction is explained well in the classic paper by Craig A. Tovey in section-2. As @DavidRicherby explained, this will never become 2-SAT. You are essentially trying to prove P=NP. Please go through this excellent video titled P vs NP and the computational complexity zoo to understand the basics of computational complexity theory as that would help you understand why it's not possible (currently).

• Yeah, I see. Even more, in every such formula every variable can have exactly one negative occurence, and the problem still will be NP-hard. | Although some formulas will become 2-SAT instances after applying the 3rd step iteratively alone. But only a small fraction of them. Nov 5, 2020 at 18:48
• @rus9384, you have highlighted an important point - some problem instances can be solved in polynomial time but not all and hence the complexity does not change. Nov 10, 2020 at 2:10

Your first statement is wrong: 3-SAT with at most 3 occurrences per variable is not NP-hard, in fact it is trivial in the sense that any instance of this problem is satisfiable (see this paper).

• 3-SAT is often described as the satisfiability problem given a boolean formula in CNF with at most 3 litterals per clause, not exactly 3 litterals per clause (see here for reference). This problem is $\mathsf{NP}$-complete (as stated in your paper). For example, $(x) \wedge (\overline{x})$ is not satisfiable. Oct 20, 2022 at 12:32
• I wasn't aware 3-SAT was also used to describe the "at most" version, my bad. Also, point 1. in the post describes the "exactly" version, I was too quick with my answer. I'll leave it so no-one makes the same mistake. Oct 20, 2022 at 12:40