hraness

p-vs-np-adjacent experiments: what they can and can't tell you

average-case evidence, honestly labeled

Drafted by an AI agent at Ben Guo's direct request from the Hraness source repositories, and checked against those sources before publication.

P versus NP is a mathematical question, and it is answered by proofs, not by benchmarks, heuristics, or intuition. And yet the question casts a long shadow over ordinary experimental work: every SAT-solver improvement, every preprocessing trick, every learned heuristic is about the gap between finding a solution and checking one. The problem for a research program is how to run experiments in that shadow without pretending they bear on the millennium problem. The answer, visible in both Platonik’s docs/research.md and the peqnp repository it cites, is a discipline of scoped claims: measure what you can measure, declare what you supplied, and keep the statuses distinct.

what "adjacent" means

P = NP asks whether every problem whose solution can be verified in polynomial time can also be solved in polynomial time. A constructive answer would need a correct algorithm plus a worst-case polynomial bound for an NP-complete problem; a separation would need a lower-bound proof over all algorithms. Neither has been found; Clay still lists the problem as unsolved.

Nothing about a finite experiment can settle that. docs/research.md is categorical: “Finite benchmark success cannot establish polynomial-time performance on all inputs.” An experiment on bounded instances can tell you that a technique helps on those instances, under that cost model, at that scale, which is real knowledge, but a different kind of knowledge. The discipline is to never let the first kind borrow the second’s authority. Platonik goes so far as to ban the meter: there is no “percent of P=NP solved” gauge anywhere in the project, because the frontier it measures is empirical, not proof-theoretic.

the peqnp ledger

peqnp describes itself as “a research laboratory for exploring P = NP through small programs, counterexamples, and explicit proofs,” and its README is a model of scoped reporting. Its experiments operate on a small typed Lisp of candidate SAT transformations, and the results are reported as finite, checkable facts:

  • Calibration: eight programs checked against all 65,536 canonical two-variable clause sets. Exactly one satisfies both satisfiability preservation and variable elimination (it recovers known unit propagation), and the experiment rejects a planted claim that the rule alone decides every CNF. Note the structure: the complete input set is enumerated, so “all” is literal.
  • Clue transfer: four sound rule instances mined from six tiny formulas, frozen, then tested on 122 larger cases. The clues cut search nodes from 738 to 620, and total measured work grew from 424,997 to 1,676,645, because matching the clues costs more than the search they save. Every case still solved correctly; the technique is slower by the declared event metric on every case.
  • Indexed transfer: replacing pair enumeration with a sorted index cuts preprocessing from 11,235,212 to 1,048,871 events on 160 fresh cases and finishes four cases the generic matcher could not, yet still costs more than doing no preprocessing at all on every case: 1,452,179 against a 520,161 baseline.
  • Implication graph: the standard 2-SAT construction recovers all 173 forced literals where the two-clause library finds 63 (including every long-chain case the library cannot start), and its linear-time decision with an explicit certificate still costs more declared events than the toy solver on 102 of 120 cases.
  • Fragment interface: on 162 mixed 2/3-CNF formulas where search is expensive, reading only the binary fragment through the graph scored positive on 22 cases, all but one of them cases where the fragment’s own contradiction decided the formula outright.
  • Extraction cost: a cheaper read (one stamped search state with inheritance) cut extraction by a third on 176 fresh cases and flipped five matched cases and no fresh ones.

Every one of those is a negative or sharply scoped result, preserved rather than buried. The README’s own summary is the honest framing: “These are finite research results, not a polynomial SAT solver.”

the interface delta

The organizing concept in peqnp is worth naming: the interface delta: baseline work minus build, read, and residual work, under one declared cost model. The idea is that a preprocessing representation, a learned clue, or a derived structure is only worth something if reading it is cheaper than recomputing it: a certificate is a pointer that is cheap to follow, and P versus NP asks whether one is always cheap to find. A backbone literal is fixed by its formula, yet reading it from an arbitrary CNF is coNP-hard while reading it from a 2-CNF implication graph takes linear time, so the representation is the variable, and the delta is its honest price.

Platonik’s version of the same rule is the blunt question in docs/research.md: “what was supplied, how was it obtained, and what work remains?” A supplied plan, a prepared register, a frozen clue library: each is a legitimate experimental input, but each is also a transfer of work out of the measured interval. The clue-transfer result is the canonical caution: mining clues reduced search nodes (the headline metric a casual reading would report) while increasing total work by a factor of four; the true result only appears when the whole cost model is charged.

declaring the oracle

The subtlest honesty problem in complexity-adjacent experiments is hidden computation: an oracle, advice, or a preprocessing step that answers a harder question than the measured one. peqnp makes the oracle a declared, pinned artifact: above twelve variables the reference answers come from CaDiCaL 3.0.1, pinned by path and SHA-256, run under a named conflict limit; every SAT model is checked against the raw clauses and every UNSAT answer is checked as an LRAT proof by the repository’s own checker, and a conflict-limit unknown stays unknown. The README notes that artifacts are produced by a replay that re-checks every model and proof without invoking the solver. The oracle can be removed and the evidence still stands.

Platonik’s research.md states the general principle: “an oracle, advice supplied by input length, free input-specific clues, or an altered unit-cost model can change which mathematical question is being asked. State that change explicitly.” This is the working rule for adjacent experiments: the question you can actually answer is the one your cost model and your supplied inputs define, and declaring them is what makes the answer about something.

the history of overreach

The reason this discipline exists is that P-vs-NP claims have a graveyard. research.md cites Gerhard Woeginger’s P-versus-NP page as a historical index of attempted resolutions (“inclusion is not an endorsement”) and picks out two instructive cases. Yannakakis’s 1991 result proves an exponential size requirement for symmetric linear-programming formulations of matching and TSP: it rules out a specified formulation approach, and the docs are explicit that it “does not prove P≠NP or a lower bound for every algorithm.” Gillet’s proposed polynomial-time route through flow networks was withdrawn (the author’s own record says the method fails), and the docs use it to argue for preserving revisions and withdrawals, not only claims.

The lesson the docs draw is a storage rule: “Store the original statement, program and source versions, input family, computational model, claimed guarantee, tests, and any counterexample or withdrawal.” A claim is a versioned artifact with its scope attached, which is, not coincidentally, exactly how the engine treats a receipt.

what you can honestly claim

The honest list of what a bounded experiment can actually establish, assembled from both projects:

  • That a technique works on a declared family under a declared cost model: the clue library, the index, the implication graph each have real measured deltas, and the sign of the delta is the finding.
  • That a claim survives its own accounting: unit propagation is real; “unit propagation decides CNF” is not, and the calibration experiment rejected the planted version.
  • That a representation pays for itself in stated conditions: the fragment interface went positive exactly where its certificate decided the formula, which is a falsifiable, checkable claim about when a read is worth building.
  • Counterexamples and negative results, preserved, published, and load-bearing: the slower total work is the reason the next experiment exists.

And the refused claims: no finite success is a worst-case bound, no heuristic improvement is a complexity result, no amount of average-case evidence is a theorem. The proposed counterexample expedition in research.md is the constructive version: freeze a claim, search for an admitted world where it fails, simplify the failure while preserving its conditions. It is a methodology that treats a refutation as a deliverable rather than a disappointment.

The posture to take home is that P-vs-NP-adjacent work is not lesser work; it is different work, with its own rigorous units: the interface delta, the declared oracle, the scoped counterexample. The experiment earns its claim by naming its envelope, and the envelope is where the science actually lives.

sources