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