A395399 - OEIS

%I #35 Jun 27 2026 18:38:47

%S 0,3,240,9641,244322,4401281,60910912,683216362,6453939838,

%T 52822713039,382755638648,2497063563331,14864391434226,81614170235933,

%U 416999303132080,1997369289939522,9024607887247844,38666482790722142,157812408646116372,615951118339821494

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

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

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

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

%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) = 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).

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

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

%K nonn,easy,changed

%O 1,2

%A _Ramin Mohammadi Masoudi_, Jun 15 2026

%E More terms from _Sean A. Irvine_, Jun 18 2026