OFFSET
1,4
COMMENTS
A clause is a multiset 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 m such clauses, so repeated clauses are also allowed.
This is the multiset clause model. It differs from the common random 3-SAT model in which clauses usually contain three distinct variables and tautological clauses are excluded.
The first row is A(1,m) = binomial(m+1,3). The first column is A(n,1)=0. The second column is A(n,2)=n.
LINKS
Stephen A. Cook, The complexity of theorem-proving procedures, Proceedings of the Third Annual ACM Symposium on Theory of Computing, 1971, 151-158.
Jian Ding, Allan Sly, and Nike Sun, Proof of the satisfiability conjecture for large k, Annals of Mathematics 196 (2022), 1-388.
Marc Mézard, Giorgio Parisi, and Riccardo Zecchina, Analytic and algorithmic solution of random satisfiability problems, Science 297 (2002), 812-815.
FORMULA
A(n,1) = 0.
A(n,2) = n.
A(1,m) = binomial(m+1,3).
A(n,3) = 2*n*(2*n^3 + 3*n^2 + 19*n - 18)/3.
EXAMPLE
Array begins:
m | 1, 2, 3, 4, 5, 6, ...
-----------------------------------------------
n = 1| 0, 1, 4, 10, 20, 35, ...
n = 2| 0, 2, 64, 831, 6760, 40748, ...
n = 3| 0, 3, 240, 9641, 244322, 4401281, ...
n = 4| 0, 4, 624, 50018, 2703376, 108412740, ...
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, m):
cl = clauses(n)
s = 0
for idxs in combinations_with_replacement(range(len(cl)), m):
if unsat(n, [cl[i] for i in idxs]):
s += 1
return s
def table_by_antidiagonals(N):
out = []
for s in range(2, N+2):
for n in range(1, s):
m = s-n
out.append(A(n, m))
return out
print(table_by_antidiagonals(10))
CROSSREFS
KEYWORD
AUTHOR
Ramin Mohammadi Masoudi, May 23 2026
STATUS
approved