Is a CNF SAT problem NP hard when the total number (but not the width) of the 3-or-more-term clauses is bounded above by a constant? What about specifically when there's only one such clause?

  • 8
    $\begingroup$ If there's only one such clause $c$ with more than 2 terms, solving such formulas is trivially in $P$. If $c$ has $n$ terms, try each of the $n$ partial assignments that satisfy $c$, then solve the remaining 2-SAT formula using the known linear-time method. Eventually you'll find a solution for the whole formula or prove that it is unsatisfiable in $O(n^2)$ time, where $n$ cannot exceed the number of variables in the whole formula. $\endgroup$
    – Kyle Jones
    Commented Dec 20, 2013 at 0:36
  • $\begingroup$ @KyleJones But a single clause with $k$ literals has $2^k-1$ satisfying assignments, not just $k$. Since $k$ is not bounded in the question, this approach gives an exponential-time algorithm. $\endgroup$ Commented Dec 22, 2013 at 10:57
  • 2
    $\begingroup$ @DavidRicherby To satisfy the clause you only need make one of the literals evaluate true. After that the clause can be ignored and you only have a 2-SAT formula remaining. $k$ literals means you only have to try $k$ assignments. $\endgroup$
    – Kyle Jones
    Commented Dec 22, 2013 at 14:41

2 Answers 2


It is worth noting that the problem becomes NP-hard when the restriction is relaxed slightly.

With a fixed number of clauses that are also of bounded size, the average number of literals in a clause is as close to 2 as one wants, by considering an instance with enough variables. As you point out, there is then a simple upper bound which is polynomial if the clause size is bounded.

In contrast, if the average number of literals per clause is at least $2 + \epsilon$ for some fixed (but arbitrarily small) $\epsilon > 0$, then the problem is NP-hard.

This can be shown by reducing 3SAT to this problem, by introducing new clauses with 2 literals that are trivially satisfiable. Suppose there are $m$ clauses in the 3SAT instance; to reduce the average clause size to $(2+\epsilon)$, it is enough to add $m(1 - \epsilon)/\epsilon$ new clauses with two literals. Since $\epsilon$ is fixed and positive, the new instance is of polynomial size.

This reduction also shows that even the version where the "large" clauses are restricted to 3 literals is NP-hard.

The remaining case is when the few large clauses are not of bounded size; each large clause seems to make the problem harder. See the SODA 2010 paper by Pǎtraşcu and Williams for the case of two clauses: they argue that if this can be done in sub-quadratic time then we would have better algorithms for SAT. There might be an extension of their argument to more clauses, which would provide evidence that your upper bound cannot be improved (modulo some form of the exponential time hypothesis).

  • $\begingroup$ only tangentially related, but there is a recent ECCC paper that formulates "almost 2-SAT" in a different way and proves strong hardness: eccc.hpi-web.de/report/2013/159 $\endgroup$ Commented Dec 20, 2013 at 21:44

Ok, I got it. The answer is no. This can be solved in poly-time. For each 3-or-more-term clause, select a literal and set it to be true. Then solve the remaining 2-sat problem. If any one provides a solution, then that is a solution to the overall problem. Since the number of 3-or-more-term clauses is fixed (say c), then if all such clauses have size <= m, then this runs in O(m^(c)*n). O(m^c) for going through each possible selection, times O(n) for solving the remaining 2-sat problem.

  • $\begingroup$ But the question explicitly says that $m$ is unbounded, so this is not a polynomial-time algorithm. $\endgroup$ Commented Dec 22, 2013 at 10:59
  • $\begingroup$ It is, because m is implicitly bounded by the number of atoms. Obviously, a clause can't have more literals than there are atoms in the problem. Perhaps I should have clarified m <= n $\endgroup$
    – dspyz
    Commented Dec 22, 2013 at 18:55

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.