A395399 Number of unsatisfiable 3-SAT formulas with 3 variables and n clauses in the multiset clause model.

0, 3, 240, 9641, 244322, 4401281, 60910912, 683216362, 6453939838, 52822713039, 382755638648, 2497063563331, 14864391434226, 81614170235933, 416999303132080, 1997369289939522, 9024607887247844, 38666482790722142, 157812408646116372, 615951118339821494

Offset

1,2

Comments

Clauses are multisets of 3 literals chosen from {x_1, x_2, x_3, not x_1, not x_2, not x_3}; repeated literals inside a clause are allowed. A formula is a multiset of n such clauses, so repeated clauses are also allowed.

This is row 3 of the array A396351; that is, a(n) = A396351(3,n).

There are binomial(2*3+2,3) = binomial(8,3) = 56 clause types over 3 variables, so the total number of n-clause formulas is binomial(n+55,n), and a(n) is that total minus the number of satisfiable formulas.

References

Stephen A. Cook, The complexity of theorem-proving procedures, Proceedings of the Third Annual ACM Symposium on Theory of Computing, 1971, 151-158.

Links

Table of n, a(n) for n=1..20.

Formula

a(n) = binomial(n+55,n) - 8*binomial(n+45,n) + 12*binomial(n+39,n) + 12*binomial(n+36,n) + 4*binomial(n+35,n) - 24*binomial(n+33,n) - 18*binomial(n+30,n) - 8*binomial(n+28,n) + 32*binomial(n+27,n) + 30*binomial(n+25,n) - 24*binomial(n+24,n) - 24*binomial(n+22,n) + 14*binomial(n+21,n) - 8*binomial(n+20,n) + 16*binomial(n+19,n) - 8*binomial(n+18,n) + binomial(n+17,n).

a(n) = A396351(3,n).

Crossrefs

Cf. A396351, A396353, A396354, A396491, A395739.

Sequence in context: A142730 A264549 A024044 * A356568 A069640 A324444

Adjacent sequences: A395396 A395397 A395398 * A395400 A395401 A395402

Keyword

nonn,easy,new

Author

Ramin Mohammadi Masoudi, Jun 15 2026

Extensions

More terms from Sean A. Irvine, Jun 18 2026

Status

approved