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?

  • 1
    $\begingroup$ 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. $\endgroup$ – D.W. Sep 5 '17 at 21:21

Your second step isn't sound.

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.

| cite | improve this answer | |
  • $\begingroup$ 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. $\endgroup$ – rus9384 Sep 5 '17 at 17:51
  • $\begingroup$ @rus9384 Good point. Actually, that makes the answer much more concrete. Let me fix it... $\endgroup$ – David Richerby Sep 5 '17 at 18:10
  • $\begingroup$ @rus9384 Done: the transformation now makes every formula satisfiable. $\endgroup$ – David Richerby Sep 5 '17 at 18:27
  • $\begingroup$ 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? $\endgroup$ – rus9384 Sep 5 '17 at 20:19
  • 1
    $\begingroup$ @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. $\endgroup$ – David Richerby Sep 5 '17 at 20:44

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.