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

35, 40748, 4401281, 108412740, 1223521735

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 6 clauses, so repeated clauses are also allowed.

This is the m=6 column of the array A(n,m), where A(n,m) is the number of unsatisfiable 3-SAT formulas with n variables and m clauses in the multiset clause model.

The total number of 6-clause formulas is T(n,6) = binomial(C(n)+5,6), where C(n)=binomial(2*n+2,3).

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

Formula

Conjecture: a(n) = (102014438*n^4 - 972478827*n^3 + 3290991742*n^2 - 4595717868*n + 2175190620)/3.

Crossrefs

Cf. A396351, A396353, A396354, A396491.

Sequence in context: A285388 A212926 A139473 * A110596 A286178 A126029

Adjacent sequences: A395736 A395737 A395738 * A395740 A395741 A395742

Keyword

nonn,hard,more,new

Author

Ramin Mohammadi Masoudi, Jun 03 2026

Status

approved