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

10, 831, 9641, 50018, 183940, 549145, 1416331, 3270676, 6922158, 13649155

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

This is the m=4 column of A396351.

For fixed m, the corresponding column is expected to be a polynomial in n, since an m-clause formula involves only finitely many literal positions. The polynomial in the Formula section was obtained by interpolation from the listed terms and should be treated as conjectural unless independently verified.

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

Formula

Conjecture: a(n) = n*(16*n^6 + 48*n^5 + 340*n^4 + 180*n^3 + 2818*n^2 - 10011*n + 6789)/18.

Prog

(Python)
from itertools import combinations_with_replacement
def clauses(n):
    lits = list(range(-n, 0)) + list(range(1, n+1))
    return list(combinations_with_replacement(lits, 3))
def lit_value(lit, a):
    v = abs(lit)-1
    val = (a >> v) & 1
    return val if lit > 0 else 1-val
def unsat(n, formula):
    for a in range(1 << n):
        if all(any(lit_value(lit, a) for lit in clause) for clause in formula):
            return False
    return True
def a(n):
    cl = clauses(n)
    s = 0
    for idxs in combinations_with_replacement(range(len(cl)), 4):
        if unsat(n, [cl[i] for i in idxs]):
            s += 1
    return s
print([a(n) for n in range(1, 8)])

Crossrefs

Cf. A396351, A396353.

Sequence in context: A272854 A015093 A104906 * A378324 A013386 A013385

Adjacent sequences: A396350 A396351 A396353 * A396355 A396356 A396357

Keyword

nonn,hard,more

Author

Ramin Mohammadi Masoudi, May 23 2026

Status

approved