What is the set of all minimal 3CNF formulas?

Definition: A minimal 3CNF formula is an unsatisfiable 3CNF formula with minimum clauses connected by conjunctions, where each clause is disjunction of 3 literals, that is if any of it's clauses is removed from the formula, then the 3CNF formula becomes satisfiable.

For some natural number n, where n is the number of atomic variables, what is the set of all minimal 3CNF formulas? Is it finite? If it is finite then what is it's cardinality, i.e. how many different minimal 3CNF formulas is possible?

In a minimal k-cnf formula, there should be 2k different k literals clauses exactly, so in a minimal 3CNF formula, there should be 23=8 different 3 literals clauses exactly.

That's what I think anyway, but correct me if I am wrong.

Note that for k-cnf formula n≥k, so in 3CNF formula n≥3.

• If a 3CNF formula $P(x_1, \dots, x_n)$ is minimal, then $P(y_1, \dots, y_n)$ is also minimal. So it may be better to fix the set of variables, not the size of it. (Or, count formulae up to α-equivalence.) – nekketsuuu Jul 17 '17 at 21:26
• I didn't understand what you said. Can you explain me please? – Farewell Stack Exchange Jul 17 '17 at 21:37
• For example, if $n=1$, then $(x \vee x \vee x) \wedge (\neg x \vee \neg x \vee \neg x)$ is minimal for every variable $x$. So if we fix the number of variables occurring in the formula, the number of minimal formulae is always infinite because the number of variables is infinite. – nekketsuuu Jul 17 '17 at 21:57
• n suppose to be finite number, not infinite, so for particular n, the number of minimal formula should be finite, but not infinite, no? I have edited my question. Please read the update. – Farewell Stack Exchange Jul 17 '17 at 22:00
• I may misunderstand the definition of $n$. Do you mean that, for example, "the number of atomic variables" of $(x \vee \neg x \vee y)$ is 3, not 2? Also, is $(x \vee \neg x \vee y)$ different from $(z \vee \neg z \vee w)$ when counting minimal 3CNFs? – nekketsuuu Jul 17 '17 at 22:48

The number of minimal formula is finite. Indeed, if a formula is minimal, then no clause can be repeated. Now there are $(2n)^3=8n^3$ possible clauses, so there are at most $2^{8n^3}$ different formulas with no repeated clauses. Thus there are at most $2^{8n^3}$ minimal formula, which is finite.
I don't know of any clean way to count the number of minimal formula; probably there is no simple formula for it. You could try computing the number for $n=1,2,3$ by brute-force, then looking up the resulting sequence in OEIS, but I don't expect you to find any simple expression for this number.
• It's possible that number of minimal 3CNF's is $2^{n+C_n^2+C_n^3} + 1$. At least, if we put n instead of 3, it will be $2^{2^n}$ which is true. – rus9384 Jul 17 '17 at 22:20