Assume that n is the number variables of the given 3CNF formula (n≥3) and all clauses in the given 3CNF formula are different.

That means that for each clause, each literal can be either positive or negative and be one of the n variables, so the number of options for each literal is 2n, but each clause has exactly 3 literals, so the maximum number of different clauses is 2n•2n•2n = (2n)3 = 8n3 = O(n3).

I have read here that 3CNF formula must have at least 8 different clauses in the form:

(x ∨ y ∨ z) ∧ (x ∨ y ∨ ¬z) ∧ (x ∨ ¬y ∨ z) ∧ (x ∨ ¬y ∨ ¬z) ∧ (¬x ∨ y ∨ z) ∧ (¬x ∨ y ∨ ¬z) ∧ (¬x ∨ ¬y ∨ z) ∧ (¬x ∨ ¬y ∨ ¬z)

to be unsatisfiable.

If this small 3CNF formula is included or subset of a larger 3CNF formula, then the larger 3CNF formula is unsatisfiable for sure, because of that subset.

So the algorithm needs to search for this subset and if the algorithm found it then the algorithm returns "given formula is unsatisfiable" as output.

And this suppose to be correct for sure.

But what happens if the algorithm doesn't find such subset?

Does this necessarily means that the given 3CNF formula is not unsatisfiable, i.e. satisfiable?

Because that the subset has exactly 8 clauses, the algorithm needs to iterate through all the different subsets of 8 clauses in the given 3CNF formula.

If the given 3CNF formula has m clauses, then there should be θ(m8) different subsets of 8 clauses, but if all clauses are different, then m=O(n3), thus O((n3)8) = O(n3•8) = O(n24)

So the running time of the algorithm to iterate through all these subsets and to find the unsatisfiable subset, if exists, takes θ(n24) time.

To do this, the algorithm needs 8 inner for loops, where each for loop is inside the other, with 8 iterative variables.

Because that the algorithm doesn't allocate any memory during the run time, the space complexity of this algorithm suppose to be θ(1).

Let me know if I was wrong and on what, i.e. if I am wrong then why?

Why I was wrong?

Please explain.

I want to learn from mistakes.

I think that

it's too good to be true


if it's too good to be true, something's wrong.
  • 1
    $\begingroup$ The maximum number of different clauses is $O(n)$. $n$ is input length. They must have such 8 clauses iff any pair of clauses either have all 3 same variables or different. $\endgroup$
    – rus9384
    Commented Jul 17, 2017 at 0:32
  • 1
    $\begingroup$ Note that $n^{24}$ is practically unsolvable for n ≥ 10. Of course in CS terms being able to solve an NP complete problem in $O(n^{24})$ would be... Well, I think it would be worth to introduce a nobel prize for CS. $\endgroup$
    – gnasher729
    Commented Jul 17, 2017 at 8:49
  • $\begingroup$ You are so right. $\endgroup$ Commented Jul 17, 2017 at 13:09

4 Answers 4


You are correct in your assumption that your algorithm correctly identifies some unsatisfiable instances, but for the general case it does not work.

For instance, you can always rewrite a clause $\{A, B, C\}$ to the equisatisfiable clause set $\{A, X, Y\}, \{\neg X, A, B\}, \{\neg Y, B, C\}$. To see this, observe that you can always recover the original clause through resolution. If applied to say, the first clause in the above example, this will already break your algorithm.

Maybe someone with more knowledge on SAT can give some more insightful information.

  • $\begingroup$ Now it remains what to do in the case that unsatisfiable subset of 8 clauses in this form was not found. Interesting what another search can the algorithm do. $\endgroup$ Commented Jul 17, 2017 at 2:22

The operative phrase is "at least 8"! The funny thing about 3SAT is that every clause with 3 distinct variables eliminates a full 1/8th of the model space. So how is it that you can have a formula with hundreds of clauses in it and not completely obliterate all of the possible solutions? The answer, of course, is that most of the clauses overlap in the portions of the model space that they exclude; and the more variables you have, the more "volume" each clause overlaps in the model space. The scenario where 8 clauses is sufficient to make a formula unsatisfiable is obviously where those 8 "blocks" have no overlap.

Geometrically speaking, one can view the model space for a formula as an $n$-dimensional hypercube of width $2$, where each dimension corresponds to a variable in the formula, and can have the value $true$ or $false$. Since it's hard to visualize hypercubes with more than 3 dimensions, it's helpful to project them down onto 2 dimensions like so:

Table of model space

Here I've rendered the formula provided by @rus9384 as a table showing how the model space is covered. The "canonical" unsatisfiable core with only 3 variables would replace the last 2 clauses with $(\lnot x, \lnot y, z)$ and $(\lnot x, \lnot y, \lnot z)$. In this case, all the "blocks" would be "aligned". If you could see this properly in 4 dimensions, it would look like we are building a 4-dimensional LEGO cube by stacking a bunch of 1x2 bricks in the same direction. What @rus9384 has done is take 2 of the "bricks" (which logically form a 2x2 block) and "rotated" them 90 degrees. Of course, this still covers the model space exactly.

Now, to see why an unsatisfiable core might contain more than 8 clauses, we should first think about what a 2-clause looks like. Suppose our formula contained $(x, y)$. This is actually the resolution of 1 and 2, so in a way, you could say that it does contain this 2-clause. And note that 1 and 2 together cover 1/4th of the space. In general, a clause with $k$ distinct variables covers $\frac{1}{2^k}$th of the model space (assuming no tautologies, of course). Thus, to force more than 8 clauses in the Minimal Unsatisfiable Core (MUC), we need to cover less than 1/8th of the model space with one or more of the clauses! Using the formula above, we can do that by introducing a clause with 4 variables, which only excludes 1/16th of the space (e.g., $(x, y, z, t)$ only takes up 1 cell in the table).

"But wait!" you say: "...we were talking about 3SAT! You can't have 4-clauses!" @Max showed that you can run Resolution forwards and backwards to get the desired clauses. So, for instance, we can introduce a new variable, $w$, and add $(\lnot x, \lnot y, \lnot w)$ and $(w, \lnot z, \lnot t)$, which resolve to the 4-clause $(\lnot x, \lnot y, \lnot z, \lnot t)$. If we replaced clause 8 in our formula with this new 4-clause (or its 3-clause "parents"), then suddenly our formula becomes satisfiable, because we have left a "hole" in the model! We would need at least one more formula to patch it up. As you can imagine, one can force a MUC to be larger than any fixed size ($\geq 8$) simply by building it with "blocks" that are arbitrarily small.

"But wait!" you say: "...you already said that all 3-clauses cover 1/8th of the model space! They are all the same size!!!" And indeed that is true. What's really going on is that we are shifting the overlap into other variables/dimensions so that the intersection with the "MUC core", if you will, is less than 1/8th, if that makes sense.


Following SAT instance is unsatisfiable:

$$(x\lor y\lor z)\land(x\lor y\lor\overline z)\land(x\lor\overline y\lor z)\land(x\lor\overline y\lor\overline z)\land(\overline x\lor y\lor z)\land(\overline x\lor y\lor\overline z)\land(\overline x\lor\overline y\lor t)\land(\overline x\lor\overline y\lor\overline t)$$

And it does not have those 8 clauses that you want to find.

Also, I don't see why it must take $O(n^{24})$ time. Finding a group of 8 clauses (if it exists) can be done in $O(n\log n)$ time.


If the given 3CNF formula has m clauses, then there should be θ(m^8) different subsets of 8 clauses

This is wrong. Number of input clauses always bounded by $n$ (or $m$ in your case). It's initial value.

Number of different subsets would be bounded by $\frac{n}{8} = O(n)$.

Algorithm would be as follows:

  1. Sort all clauses.
  2. Take two variables: a and b. While C[a] and C[b] have all the same variables, increase b : b++.
  3. If C[a] and C[b] differ by at least one variable, put a = b; b++.

This algorithm results in $O(n\log n)$ time.

  • 1
    $\begingroup$ Regarding space complexity, it depends on how you measure space – in bits (like you do) or in machine words (like we usually do when analyzing algorithms). $\endgroup$ Commented Jul 17, 2017 at 5:30
  • 1
    $\begingroup$ @YuvalFilmus, well, measuring in words it takes constant space. $\endgroup$
    – rus9384
    Commented Jul 17, 2017 at 6:18
  • 1
    $\begingroup$ @ErezZrihen, I have described how it could work. $\endgroup$
    – rus9384
    Commented Jul 17, 2017 at 10:50
  • 1
    $\begingroup$ @ErezZrihen, my conjecture was about all instances. No one have found counterexample, so, it is possible that SAT can be solved in polynomial time. $\endgroup$
    – rus9384
    Commented Jul 17, 2017 at 11:07
  • 1
    $\begingroup$ @ErezZrihen, I'm trying to prove it. $\endgroup$
    – rus9384
    Commented Jul 17, 2017 at 16:49

Your evaluation only works into one direction, you can use it to test for unsatisfiability for the listed cases which are only a subset of all unsatisfiability cases. Imagine for example a formula in which 100 clauses contain x and one clause contains (¬x ∨ ¬x ∨ ¬x).


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.