A395739 - OEIS

%I #40 Jun 28 2026 07:56:09

%S 35,40748,4401281,108412740,1223521735

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

%C 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.

%C 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.

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

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

%F a(n) is a polynomial in n of degree 3*6-5 = 13, with leading coefficient (4/3)^4/4! = 32/243.

%Y Cf. A396351, A396353, A396354, A396491.

%K nonn,hard,more,changed

%O 1,1

%A _Ramin Mohammadi Masoudi_, Jun 03 2026