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

4, 64, 240, 624, 1340, 2544, 4424, 7200, 11124, 16480, 23584, 32784, 44460, 59024, 76920, 98624, 124644, 155520, 191824, 234160, 283164, 339504, 403880, 477024, 559700, 652704, 756864, 873040, 1002124, 1145040, 1302744, 1476224, 1666500, 1874624, 2101680, 2348784

Offset

1,1

Comments

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

This is the m=3 column of A396351.

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..36.

Index entries for linear recurrences with constant coefficients , signature (5,-10,10,-5,1).

Formula

a(n) = 2*n*(2*n^3 + 3*n^2 + 19*n - 18)/3.

From Stefano Spezia, May 24 2026: (Start)

G.f.: 4*x*(1 + 11*x - 10*x^2 + 6*x^3)/(1 - x)^5.

E.g.f.: 2*exp(x)*x*(6 + 42*x + 15*x^2 + 2*x^3)/3. (End)

Mathematica

LinearRecurrence[{5, -10, 10, -5, 1}, {4, 64, 240, 624, 1340}, 36] (* Stefano Spezia, May 24 2026 *)

Prog

(Python)
def a(n):
    return 2*n*(2*n**3 + 3*n**2 + 19*n - 18)//3
print([a(n) for n in range(1, 37)])

Crossrefs

Cf. A396351, A396354.

Sequence in context: A273375 A016934 A260182 * A056229 A062271 A110258

Adjacent sequences: A396349 A396350 A396351 * A396354 A396355 A396356

Keyword

nonn,easy

Author

Ramin Mohammadi Masoudi, May 23 2026

Status

approved