2
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ 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.) $\endgroup$ – nekketsuuu Jul 17 '17 at 21:26
  • $\begingroup$ I didn't understand what you said. Can you explain me please? $\endgroup$ – Farewell Stack Exchange Jul 17 '17 at 21:37
  • $\begingroup$ 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. $\endgroup$ – nekketsuuu Jul 17 '17 at 21:57
  • $\begingroup$ 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. $\endgroup$ – Farewell Stack Exchange Jul 17 '17 at 22:00
  • $\begingroup$ 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? $\endgroup$ – nekketsuuu Jul 17 '17 at 22:48
2
$\begingroup$

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.

What you are thinking is wrong. A minimal, unsatisfiable formula can have more than 8 clauses.

$\endgroup$
  • $\begingroup$ "An unsatisfiable formula can have more than 8 clauses" this is correct, but then it is probably not minimal, because probably there exists a possibility to remove any of it's clauses and it will remain unsatisfiable. $\endgroup$ – Farewell Stack Exchange Jul 17 '17 at 22:16
  • $\begingroup$ @ErezZrihen, see edited answer. An unsatisfiable formula can have more than 8 clauses even if it is minimal. I suggest you try to find an example (it will be a good exercise for you that will boost your understanding). $\endgroup$ – D.W. Jul 17 '17 at 22:16
  • $\begingroup$ Oh, now I understand. Okay thanks for your answer. $\endgroup$ – Farewell Stack Exchange Jul 17 '17 at 22:17
  • $\begingroup$ 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. $\endgroup$ – rus9384 Jul 17 '17 at 22:20
  • $\begingroup$ 2^(2^n) is double/super exponential!!! :O How did you get to these terrible results? $\endgroup$ – Farewell Stack Exchange Jul 17 '17 at 22:26

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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