How many tautologies are there?

Question

Given $m, n, k$, how many of $k$-DNFs with $n$ variables and $m$ clauses are tautology? (or how many $k$-CNFs are unsatisfiable?)

Answer 1

The answer depends on $k$, $m$, and $n$. Exact counts are generally not known, but there is a "threshold" phenomenon that for most settings of $k$, $m$, $n$, either nearly all $k$-SAT instances are satisfiable, or nearly all instances are unsatisfiable. For example, when $k=3$, it has been empirically observed that when $m < 4.27 n$, all but a $o(1)$ fraction of 3-SAT instances are satisfiable, and when $m > 4.27n$, all but a $o(1)$ fraction are unsatisfiable. (There are also rigorous proofs of bounds known.)

One starting point is "The Asymptotic Order of the k-SAT Threshold".

Amin Coja-Oghlan has also done a lot of work on these satisfiability threshold problems.

Answer 2

This is an extended comment to complement Ryan's answer, which deals with the thresholds where the number of clauses becomes large enough that the instance is almost surely unsatisfiable. One can also compute the much larger thresholds where the number of clauses forces unsatisfiability when it exceeds a function of $n$.

Note that some technical issues need to be addressed. If repeated clauses are counted in $m$, then $m$ can be made as large as desired without changing $n$. This would destroy most relationships between $m$ and $n$. So assume that $m$ is the number of distinct clauses. We need to decide on another detail, whether instances are encoded so that order of literals within a clause or order of clauses within an instance matter. Suppose this is not important, so two instances are regarded as equivalent if they contain the same clauses, and two clauses are equivalent if they contain the same literals. With these assumptions we can now bound the number of distinct clauses that can be expressed with $n$ variables. Each clause can have each variable occurring positively or negatively, or not at all, and then $m\le 3^n$.

First consider SAT without a restriction on $k$. What is the largest $m$ such that the instance is satisfiable? Without loss of generality we can suppose that the all-zero assignment is a solution. There are then $3^n-2^n$ different clauses consistent with this solution, each containing at least one negated literal. Hence $m\le 3^n-2^n$ for any satisfiable instance. The instance consisting of all clauses that each contain at least one negated literal has this many clauses, and is satisfied by the all-zero assignment. Further, by the pigeonhole principle any instance with at least $3^n-2^n+1$ clauses is unsatisfiable.

This yields $2^{3^n-2^n}$ different subsets of such clauses, each representing a distinct instance which is satisfied by some assignment. In comparison, the total number of different instances is $2^{3^n}$.

Now modifying the above for instances in which each clause has at most $k$ literals, there are $\sum_{i=0}^k \binom{n}{i}2^i$ distinct such clauses, and $\sum_{i=0}^k \binom{n}{i}$ clauses in which there are no negative literals, so $m\le \sum_{i=0}^k \binom{n}{i}(2^i - 1)$ for satisfiable instances, and any larger $m$ is unsatisfiable. There are then $2^{\sum_{i=0}^k \binom{n}{i}(2^i - 1)}$ instances satisfied by any particular assignment, out of the total of $2^{\sum_{i=0}^k \binom{n}{i}2^i}$ $k$-SAT instances.