pnplab — P vs NP: experimentable algorithms (lab log, started 2026-10-31)

Why a new lab: SHA-256 (/root/shalab) is a hard instance, not a P-vs-NP lever. Every known route to P≠NP goes through lower bounds (circuits or proofs). Those can be measured exactly at small sizes. Python: /root/shalab/venv/bin/python (pysat, numpy). Keep ≤6 procs (box is shared, load ~30).

Track A — exact circuit complexity C(f) over B2 (MCSP via SAT) circuit/

mcsp.py: Kojevnikov/Kulikov/Knuth encoding, normal gates, used-gate + adjacent-lex symmetry breaking; monotone=True restricts to AND/OR. - VALIDATED: npn4.py computes C for all 222 NPN classes of 4-input fns (120 s, 6 procs) →

  {0:10,1:60,2:456,3:2474,4:10624,5:24184,6:25008,7:2720} = Knuth TAOCP 7.1.2 exactly. n=3 also exact.

MAJ4 (≥3 of 4) = 7 (s=6 UNSAT 5.6 s). MAJ5: circuit with 10 gates found in 58 s (lit. C=10);

  the lower-bound proof (s=9 UNSAT) is the expensive part → longrun.sh (results in maj5.txt).

WALL: naive sym.py over all 5-input symmetric fns did not finish one in 14 min before lex-breaking.

  Proving "no circuit with s gates" = coNP; this is MCSP hardness in the flesh.

longrun.sh (background, tgsend on finish): MAJ5 s=9/10, MOD3_5 s=7..10, mono.py (TRIANGLE(K4),

  PERFECT-MATCHING(K4): general vs monotone exact size — Razborov's monotone gap at toy scale).

Track B — proof complexity: CDCL = resolution proof/

scaling.py (CaDiCaL 1.9):

  PHP(n+1,n) conflicts: n=6 1.0k | 7 7.1k | 8 32k | 9 267k | 10 2.2M (185 s)  → ×5–8 per pigeon,
  exactly Haken's 2^Ω(n) resolution lower bound. Same problem is trivial for counting → barrier is the
  proof system, not the problem.
  random 3-SAT @4.26, median conflicts: n=100 332 | 150 5.3k | 200 15.5k | 250 98k | 300 146k
  → ≈2^(0.044 n), in line with literature (≈2^(0.03–0.05 n)). Exponential, small constant.

Honest standing

Nothing new to the literature yet; the tools are validated against known exact numbers. Best known explicit general circuit lower bound is ~3.1n (Li–Yang 2022) — the real frontier.

Next steps (ordered)

Faster lower-bound proofs: add "no two gates compute the same function" + output-gate-last

   constraints, try kissat/cube-and-conquer → target exact C for all 5-input symmetric functions
   and compare to Knuth/Kulikov tables.

Gate-elimination audit: for each 5/6-input fn with exact C, check how far gate elimination

   (the only technique behind 3n-type bounds) gets vs the true C — measures the technique's loss.

Proof systems above resolution: PHP with cardinality reasoning (cutting planes) vs CDCL,

   Tseitin on expanders — map which encodings flip exponential→polynomial.

MCSP self-test: SAT time for C(f)≤s on random vs structured f (Hirahara-style hardness magnification

   at toy scale).

GRENZWERK

pnplab — P vs NP: experimentable algorithms (lab log, started 2026-10-31)

Track A — exact circuit complexity C(f) over B2 (MCSP via SAT) circuit/

Track B — proof complexity: CDCL = resolution proof/

Honest standing

Next steps (ordered)

Rohdaten