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

0, 2, 64, 831, 6760, 40748, 198496, 823058, 3005484, 9896922, 29901820, 83980533, 221486288, 552967280, 1315425728, 2997604237, 6572985724, 13920899500, 28568160620, 56964835770, 110632071840, 209707281240, 388690007880, 705598592985, 1256335203240

Offset

1,2

Comments

Clauses are multisets of 3 literals chosen from {x_1, x_2, not x_1, not x_2}; 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 2 of the array A396351; that is, a(n) = A396351(2,n).

There are binomial(2*2+2,3) = binomial(6,3) = 20 clause types over 2 variables, so the total number of n-clause formulas is binomial(n+19,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..25.

Formula

a(n) = binomial(n+19,n) - 4*binomial(n+15,n) + 4*binomial(n+12,n) + 2*binomial(n+11,n) - 4*binomial(n+9,n) + binomial(n+7,n).

Crossrefs

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

Sequence in context: A264481 A120121 A274656 * A298276 A299369 A299138

Adjacent sequences: A394066 A394067 A394068 * A394070 A394071 A394072

Keyword

nonn,easy

Author

Ramin Mohammadi Masoudi, Jun 13 2026

Status

approved