Is this possible to solve 3SAT in O(n^24) time and O(1) space?

Question

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)³ = 8n³ = O(n³).

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 θ(m⁸) different subsets of 8 clauses, but if all clauses are different, then m=O(n³), thus O((n³)⁸) = O(n^3•8) = O(n²⁴)

So the running time of the algorithm to iterate through all these subsets and to find the unsatisfiable subset, if exists, takes θ(n²⁴) 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

and

if it's too good to be true, something's wrong.

Answer 1

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.

Answer 2

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:

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.

Answer 3

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.

Edit:

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.

Answer 4

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