How many 3-SAT expressions with up to N variables are satisfiable?

Question

TL;DR

There are exactly 255 possible 3-sat expressions with exactly 3 variables (more meticulously defined below). Of those, exactly 254 are satisfiable. There are exactly 4,294,967,295 possible 3-sat expressions with exactly 4 variables. Of those, how many are satisfiable? How did you get that number?

Problem Statement

Assume you have a 3-SAT equation where all the clauses have exactly 3 distinct variables (i.e. $X$ and $\neg X$ will never appear in the same clause), and no clause appears more than once (i.e. some expression won't have both $(X \lor Y \lor \neg Z)$ and $(X \lor \neg Z \lor Y)$). With this construction, there are a finite amount of expressions with only N variables.

For the class of expressions with up to N variables, is there an equation to compute how many are satisfiable?

Example of N=3

For example, with N=3, there are 254 solutions.

We know this because for N=K, there are exactly $8 *\binom{K}{3}$ distinct clauses, as you must select three distinct variables for each clause, and 1 of 8 possible sign values for those variables (+/+/+, +/+/-, +/-/+, +/-/-, ...). If there are $8 *\binom{K}{3}$ possible clauses, then there must be $2^{(8 *\binom{K}{3})} - 1$ possible boolean expressions, because each clause may appear or not (so $2^{(8 *\binom{K}{3})}$) and we have to subtract one for the case with no clauses.

For N=3, there are 255 possible expressions (using the lemma above), and only one is unsatisfiable. So there must be 254 distinct satisfiable expressions.

How about for N=4?

Answer 1

There is almost certainly no non-trivial formula that will tell you the number of solutions. By non-trivial, I mean something not of the form $$ \sum_{x_1, \dots, x_n\in\{0,1\}} f(x_1, \dots, x_n)\,, $$ where $$f(x_1, \dots, x_n)=\begin{cases}1 &\text{if $x_1, \dots, x_n$ satisfies the formula}\\ 0&\text{otherwise.}\end{cases} $$

Note that if we have a formula $F$ (trivial or otherwise) that tells us how many satisfying assignments there are, we can decide 3-SAT just by computing $F$ and checking whether $F=0$ (unsatisfiable) or $F>0$ (satisfiable). This means that computing $F$ is NP-hard so, assuming that P$\,\neq\,$NP, $F$ is difficult to compute, which suggests that $F$ can't have any nice form.

In fact, $F$ is complete for the complexity class #P, which is essentially at least as hard as all of the polynomial hierarchy. This means that it seems to be quite a lot harder than "just NP-hard". Furthermore, we can't even approximately compute $F$ in any efficient way unless P=NP. Even being able to approximate $F$ with exponential additive error would allow us to distinguish between $F=0$ and $F>0$ and thus allow us to solve 3-SAT. For example, given a formula with $N$ variables and $F$ solutions, we can create a formula with $2N$ variables and exactly the same clauses (so variables $N+1, \dots, 2N$ aren't mentioned in the formula and can take any value). This formula has $2^NF$ satisfying assignments and being able to approximate that number strictly better than $\pm 2^{N-1}$ would allow us to tell the difference between $F=0$ and $F>0$.

Answer 2

I agree with other people here in that there is probably no nice closed formula to compute this number, and if there is one we don't know it yet

However, a lot of research has looked at random 3-SAT problems. It is well known that they experience a "phase transition". With $N$ variables and $M$ clauses, $N$ and $M$ big, there's a number $\alpha \approx 4.267$ such that most problems with $\frac{M}{N} > \alpha$ are unsat, and most others are sat

That's no proof, but it's a hint that the number of satisfiable problems may be close to the number of problems with less that $\alpha N$ clauses for some constant $\alpha$. That is about $\dbinom{N}{3}^{\alpha N} \equiv N^{3\alpha N}$ when $N$ is big - very small compared to the total number of SAT problems $2^{N^3}$

Edit: Link about random 3-SAT with an estimation of $\alpha$

Answer 3

Well this is a way to find all solutions (and hence the number of solutions) and that is simply to try all solution. But this is terribly inefficient and there are exponentially many solutions. The reason it is very unlikely that there is an efficient algorithm for your question is because it is NP-hard, as we can reduce the satisfiability of a 3-SAT equation to computing the number of solutions. In particular, if we can solve your question in polynomial time, then we can solve 3-SAT in polynomial time by checking whether the number of solutions is greater than 0.