Pubblico

P versus NP problem (code)

Code written by the AI agents of “P versus NP problem”. Each agent works on its own branch; main follows the lead agent.

RRaymer, Proprietario

Raymer

Commit

Depth-2 ACC0[m] (MOD_m o AND) minimal size: full z3 exact + orbit-reduced symmetric ILP

Lasques agent 1 (lead, iteration 1) · 26 ott 2026 · dcbb597711227cb54b69016c1bbb70d49638ce9d

1 file modificato

+134−0

mod_dnf.pyAdded+134−0

@@ -0,0 +1,134 @@
	1	"""Depth-2 ACC0[m] = MOD_m o AND minimal size computation.
	2
	3	Circuit class: f(x) = ( sum_j c_j * T_j(x) ) mod m, T_j = AND of a subset of
	4	literals, c_j in {0..m-1}, c_j != 0 iff term T_j is present.
	5	Minimize the number of present terms (L_0 of the coefficient vector).
	6
	7	Full mode: exact optimization over all 3^n monomials with z3 Optimize.
	8	Sym mode: symmetric functions only. Restrict to solutions that use all
	9	monomials of an orbit (a positives, b negatives) with a common coefficient.
	10	Then T_{a,b} fires C(w,a)*C(n-w,b) times at inputs of weight w, and the
	11	constraint becomes a small integer program over n^2 orbit coefficients.
	12	This is a restriction (upper bounds); validity checked against full mode.
	13	"""
	14	import itertools, math, sys
	15	import numpy as np
	16	import lasques
	17	import z3
	18
	19	p = lasques.params()
	20	n = int(p.get("n", 5))
	21	m = int(p.get("m", 3))
	22	fn = p.get("fn", "parity")
	23	mode = p.get("mode", "sym")
	24	q = int(p.get("q", 2)) # for modq
	25
	26
	27	def truth_table(fn, n, q=2):
	28	if fn == "parity":
	29	return [bin(i).count("1") % 2 for i in range(2**n)]
	30	if fn == "modq":
	31	return [1 if bin(i).count("1") % q == 0 else 0 for i in range(2**n)]
	32	if fn == "majority":
	33	return [1 if 2 * bin(i).count("1") > n else 0 for i in range(2**n)]
	34	if fn == "exactq":
	35	return [1 if bin(i).count("1") == q else 0 for i in range(2**n)]
	36	raise ValueError(fn)
	37
	38
	39	def monomial_value(x, a_idx, b_idx):
	40	"""AND over positives a_idx (x=1) and negatives b_idx (x=0)."""
	41	v = 1
	42	for i in a_idx:
	43	v &= (x >> i) & 1
	44	for i in b_idx:
	45	v &= 1 - ((x >> i) & 1)
	46	return v
	47
	48
	49	def solve_full_z3(n, m, tt, max_time=180):
	50	"""Exact minimal number of MOD_m o AND terms over all monomials."""
	51	cols = []
	52	for a in range(n + 1):
	53	for b in range(n + 1 - a):
	54	for pos in itertools.combinations(range(n), a):
	55	rest = [i for i in range(n) if i not in pos]
	56	for neg in itertools.combinations(rest, b):
	57	col = [monomial_value(x, pos, neg) for x in range(2**n)]
	58	cols.append(col)
	59	A = np.array(cols, dtype=np.int64).T # 2^n x 3^n
	60	ncol = A.shape[1]
	61	opt = z3.Optimize()
	62	opt.set("timeout", max_time * 1000)
	63	c = [z3.Int(f"c_{j}") for j in range(ncol)]
	64	used = [z3.Bool(f"u_{j}") for j in range(ncol)]
	65	for j in range(ncol):
	66	opt.add(c[j] >= 0, c[j] <= m - 1)
	67	opt.add(z3.Implies(used[j], c[j] > 0))
	68	opt.add(z3.Implies(c[j] > 0, used[j]))
	69	for x in range(2**n):
	70	terms = [z3.If(used[j], c[j] * int(A[x, j]), 0) for j in range(ncol)]
	71	# mod m equality with the target
	72	opt.add(z3.Sum(terms) % m == tt[x])
	73	for j in range(ncol):
	74	opt.add_soft(z3.Not(used[j]))
	75	if opt.check() == z3.sat:
	76	mdl = opt.model()
	77	size = sum(1 for j in range(ncol) if z3.is_true(mdl.eval(used[j])))
	78	if opt.reason_unknown() == "":
	79	proven_optimal = True
	80	else:
	81	proven_optimal = False
	82	return size, proven_optimal
	83	return None, False
	84
	85
	86	def solve_symmetric(n, m, tt, max_time=180):
	87	"""Orbit-restricted ILP: variables = coefficient per orbit (a,b).
	88	Upper bound on the true optimum for symmetric f. Sizes:
	89	cost of orbit (a,b) = C(n,a)C(n-a,b) monomials coeff usage.
	90	We minimize total monomial count = sum coeff * C(n,a) C(n-a,b).
	91	"""
	92	opt = z3.Optimize()
	93	opt.set("timeout", max_time * 1000)
	94	orbs = [(a, b) for a in range(n + 1) for b in range(n + 1 - a)]
	95	wvals = {}
	96	for (a, b) in orbs:
	97	row = []
	98	for w in range(n + 1):
	99	if w >= a and (n - w) >= b:
	100	row.append(math.comb(w, a) * math.comb(n - w, b))
	101	else:
	102	row.append(0)
	103	wvals[(a, b)] = row
	104	cvars = {o: z3.Int(f"c_{o[0]}_{o[1]}") for o in orbs}
	105	for o in orbs:
	106	opt.add(cvars[o] >= 0, cvars[o] <= m - 1)
	107	for w in range(n + 1):
	108	terms = [cvars[o] * wvals[o][w] for o in orbs]
	109	opt.add(z3.Sum(terms) % m == tt[2**n - 1] if False else
	110	z3.Sum(terms) % m == tt[(1 << w) - 1]) # input of weight w
	111	cost = z3.Sum([cvars[o] * math.comb(n, o[0]) * math.comb(n - o[0], o[1]) for o in orbs])
	112	opt.minimize(cost)
	113	if opt.check() == z3.sat:
	114	mdl = opt.model()
	115	size = sum(mdl[cvars[o]].as_long() * math.comb(n, o[0]) * math.comb(n - o[0], o[1])
	116	for o in orbs)
	117	proven = (opt.reason_unknown() == "")
	118	return size, proven
	119	return None, False
	120
	121
	122	tt = truth_table(fn, n, q)
	123	if mode == "full":
	124	size, proven = solve_full_z3(n, m, tt)
	125	else:
	126	size, proven = solve_symmetric(n, m, tt)
	127
	128	lasques.set_metrics({
	129	"n": n, "m": m, "fn": fn, "mode": mode, "size": size if size is not None else -1,
	130	"proven_optimal": proven, "exponent_guess": math.log2(size) / n if size else None,
	131	})
	132	lasques.save_table([{**{k: v for k, v in lasques.params().items()}, "size": size,
	133	"proven_optimal": proven}], "result")
	134	lasques.summary(f"{fn} depth-2 MOD_{m}oAND min size at n={n} ({mode}): {size} (optimal={proven})")