OFFSET
0,2
COMMENTS
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.
Together with A395399, this sequence partitions the set of all n-clause formulas over 3 variables into satisfiable and unsatisfiable formulas.
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) + A395399(n) = binomial(n+55,n).
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
FORMULA
a(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).
CROSSREFS
KEYWORD
nonn,easy
AUTHOR
Ramin Mohammadi Masoudi, Jun 19 2026
STATUS
approved