# RRLS Invariant Discovery Engine ## Scope and result **The engine was built, run, extended in response to counterexamples, and tested on a fresh cohort. It has not solved P versus NP.** The implemented research loop is: 1. Compute an explicit catalogue of exact structural invariants. 2. Obtain SAT labels using existing algorithms and independent certificate checking. 3. Cluster formulas by exact invariant equality. 4. Preserve every cluster containing both SAT and UNSAT inputs. 5. Select additional invariant operators on training data. 6. Freeze the selection and test it on fresh formulas. The first catalogue failed on a checked 45-variable pair. Adding higher Gram-matrix traces distinguished that pair. The training selector chose the fourth trace: it removed all 214 opposite-label training pairs. On a separate fresh cohort, it reduced 290 opposite-label pairs to one. That last pair contains **two 51-variable, 170-clause formulas with the same entire extended fingerprint and opposite certified answers**. This is an executable counterexample-guided research tool. Its catalogue is finite and uses established mathematical constructions. It does not automatically invent arbitrary algebras, compute every known invariant, or establish a new complexity result. ## What the proposed target means Let \(F\) be a CNF formula. A sufficient route to a polynomial SAT algorithm would be algorithms \(I,D\) such that \[ \operatorname{SAT}(F)=D(I(F)), \qquad \operatorname{time}(I,F)+\operatorname{time}(D,I(F)) \le p(|F|) \] for one fixed polynomial \(p\), for every input. Construction, representation size, recognition, arithmetic bit costs, and decoding must be counted. Conversely, if SAT has a polynomial-time algorithm, take \(I(F)=\operatorname{SAT}(F)\) and let \(D\) be the identity. This is already a one-bit invariant. Thus the existence of a polynomial-time SAT-deciding invariant is equivalent to the original algorithmic goal; the terminology alone does not narrow the unresolved mathematics. SAT's role in P versus NP and the use of input bit length are set out in [Stephen Cook's official problem description](https://www.claymath.org/wp-content/uploads/2022/06/pvsnp.pdf). A complete canonical form for formula isomorphism would be a different requirement. Isomorphism invariance alone does not determine satisfiability, and a full canonical form is not necessary for a decision algorithm. The engine tests the necessary separation property: \[ I(F)=I(H)\quad\Longrightarrow\quad \operatorname{SAT}(F)=\operatorname{SAT}(H). \] One certified counterexample disproves this property for the particular \(I\). No finite collection of successful examples proves it universally. ## The invariant catalogue Input is `{"variables": n, "clauses": [[...], ...]}`. All numerical feature calculations use integers or finite fields. There are no floating-point eigenvalues or tolerances in fingerprint equality. Normalization removes tautologies, duplicate literals, and duplicate clauses. Only occurring variables receive internal coordinates; a large declared variable number does not allocate that many coordinates. The declared unused-variable count is retained as a feature. The allowed equivalences are variable renaming, independent complementation of variables, clause reordering, and literal reordering. The features are **not** invariant under every logically equivalent rewriting or the addition of arbitrary redundant clauses. | Group | Exact information retained | |---|---| | `shape` | Variable and clause counts, clause widths, unordered positive/negative occurrence degrees, component-size histogram | | `ranks` | Incidence rank over GF(2); signed and unsigned incidence ranks over GF(3) and GF(5) | | `moments` | Signed and unsigned Gram traces of degrees 1 and 2 | | `wl` | Stable, typed 1-dimensional Weisfeiler–Leman color-refinement trace | | `affine` | Complete same-scope XOR blocks of width at most 6, coefficient and augmented ranks, rank gap, uncovered-clause count | | `gram_trace3` | Signed and unsigned Gram traces of degree 3, added in the refinement | | `gram_trace4` | Signed and unsigned Gram traces of degree 4, added in the refinement | For color refinement, the graph has two identically colored literal nodes per variable, a complement edge between them, and a separately typed clause node connected to its literals. Complementing a variable swaps its literal nodes. The saved trace includes each round's exact descriptor dictionary and multiplicities, not merely locally assigned color IDs. Cluster equality compares exact serialized features; SHA-256 is used for input identity and convenience, not as a mathematical equality oracle. Stable color refinement is not a complete graph-isomorphism test. Its relation to graph structure and its indistinguishability classes are studied in [Dell, Grohe, and Rattan, *Lovász Meets Weisfeiler and Leman*](https://arxiv.org/abs/1802.08876). RRLS implements a finite invariant based on that established method, not a new canonicalizer. ## Why the matrix features survive coordinate changes Let \(A\) be the signed clause-variable incidence matrix: a positive occurrence is \(+1\), a negative occurrence is \(-1\), and absence is zero. Under an allowed change of coordinates, \[ A'=QAPD, \] where \(Q,P\) are permutation matrices and \(D\) is diagonal with entries \(\pm1\). Therefore rank over every tested field is preserved. If \(G=A^{\mathsf T}A\), then \[ G'=DP^{\mathsf T}GPD, \qquad \operatorname{tr}((G')^k)=\operatorname{tr}(G^k). \] The unsigned incidence matrix similarly changes by row and column permutations. This proves the stated transformation invariance of the rank and trace operators. The extension computes \(G^2\) using sparse integer multiplication, then uses symmetry: \[ \operatorname{tr}(G^3)=\sum_{i,j}G_{ij}(G^2)_{ij}, \qquad \operatorname{tr}(G^4)=\sum_{i,j}(G^2)_{ij}^2. \] These are exact polynomial-cost operations for fixed degree. Sparse intermediate matrices can become dense. The implementation caps work and reports `BUDGET` if necessary; it does not assume sparsity persists. ## A global parity distinction that local structure misses The controlled parity family assigns one Boolean variable to every edge of a connected cubic prism graph. Each vertex imposes \[ \bigoplus_{e\ni v}x_e=b_v. \] Each degree-three equation is encoded by its four forbidden CNF assignments. Changing a vertex charge leaves all the initial structural groups equal for the paired examples. However, summing all vertex equations cancels every edge twice: \[ 0=\bigoplus_v b_v. \] An odd total charge is impossible. For even total charge, a spanning-tree elimination constructs an edge assignment: satisfy leaf charges upward, with the root condition supplied by even total parity. This gives a complete decision rule for this connected parity family. The engine recognizes only complete local XOR truth-table encodings of bounded width. It constructs \(Mx=b\) and records \[ \delta=\operatorname{rank}[M\mid b]-\operatorname{rank}(M)\in\{0,1\}. \] If \(\delta=1\), the recognized subsystem is inconsistent. If \(\delta=0\), it is consistent; **unrecognized clauses may still make the full formula UNSAT**. The uncovered-clause count is therefore retained. On each of the original training and held-out parity subsets, the structural catalogue had 256 opposite-label pairs. Adding the affine group reduced that to zero. These 128 formulas came from eight prism sizes and multiple charge patterns, not 128 independent hard graph structures. Many charge patterns are equivalent under variable complementation. ## The first complete-catalogue collision For a graph \(H\), encode three-coloring with three variables per vertex, one positive choose-a-color clause, three pairwise at-most-one clauses per vertex, and three color-conflict clauses per edge. The explicit development pair uses: - the square of the 15-cycle, which is three-colorable by repeating colors 0, 1, 2; - the line graph of the Petersen graph, whose encoding has an independently checked UNSAT refutation. Both have 15 vertices, are connected and 4-regular, and produce 45-variable, 150-clause CNFs. All five original feature groups are exactly equal. The rank equality is particularly instructive. Within one vertex's three variables, the three at-most-one rows have determinant \(\pm2\), giving full rank over the odd fields. Over GF(2), those rows span the even-parity subspace and the choose-a-color row adds the third direction. Consequently every tested incidence rank is already 45 in both formulas. An additional rank deficit is not being concealed here. For a connected \(d\)-regular graph on \(N\) vertices, this encoding has \[ G=(d+1)I+2(I_N\otimes J_3)+A_H\otimes I_3, \] where \(J_3\) is the all-ones matrix. At \(d=4\), \[ \operatorname{tr}(G)=21N, \qquad \operatorname{tr}(G^2)=183N. \] Thus the first two moments cannot distinguish these graphs. The third includes triangle information: \[ \operatorname{tr}(G^3)=1833N+18\,\#\operatorname{Triangles}(H). \] It equals 27,765 for the cycle-square encoding and 27,675 for the Petersen-line encoding. This is a concrete way that a higher-order invariant recovers information omitted by the initial fingerprint, using established matrix algebra. ## The finite refinement experiment The first run had 1,346 base entries: 64 saved RRLS residual cores, 1,024 fixed-seed random 3-CNFs, 128 parity encodings, 128 regular-graph coloring encodings, and the two explicit development examples. There were 1,344 distinct raw base inputs. One recorded bijective transformation per entry produced 2,692 formula records in total. The old core split groups related residuals by their original source formula. Generated training and held-out sets use different sizes. Every transformed copy stays with its parent. The explicit development examples are excluded from training and held-out statistics. The residuals are not claimed to be irreducible under all possible algorithms. The initial selector chose `shape` and `affine`. After seeing the development collision and the original held-out collision count, we added the fixed candidate family consisting of traces 3 and 4. This is a deliberately limited operator search, not open-ended symbolic invention. It chooses the operator removing the most opposite-label training pairs, with catalogue order breaking ties. The original held-out set became reused development data at that point. A **fresh 256-formula cohort** was fixed separately: 128 regular graphs of sizes 16–19, 64 parity encodings at prism sizes 11–12, and 64 random 24-variable CNFs. The selector was frozen before consulting their labels. All test inputs were retained. | Dataset | Base entries | Original full catalogue: opposite-label pairs | Add trace 3 | Add trace 4 | Add both | |---|---:|---:|---:|---:|---:| | Original training | 656 | 214 | 8 | 0 | 0 | | Reused original held-out | 688 | 117 | 9 | 3 | 3 | | Explicit development pair | 2 | 1 | 0 | 0 | 0 | | Fresh test | 256 | 290 | Not separately selected | 1 | 1 | The training selector chose trace 4 and stopped because no training collisions remained. The fresh result shows why that stopping condition cannot be a proof gate for P=NP. These are counts of **SAT/UNSAT pairs sharing a fingerprint**, not accuracy scores. A singleton cluster does not supply a decision rule for future formulas. The records also include transformations, repeated structure, and synthetic families; they must not be described as thousands of independent hard SAT cores. ## The remaining exact counterexample The fresh witness is saved as: - `fresh-regular4-17-07`: SAT, with a checked assignment; - `fresh-regular4-17-26`: UNSAT, with a checked 53-clause RUP proof ending in the empty clause. Each formula has 51 variables, 170 clauses, and 357 literal occurrences. Their entire seven-group profiles are equal, including the stable color-refinement trace. All five incidence ranks are 51. Their common signed and unsigned moments are \[ (\operatorname{tr}G,\operatorname{tr}G^2, \operatorname{tr}G^3,\operatorname{tr}G^4) =(357,3111,31269,344607). \] Neither has a recognized complete XOR block. Both have an affine rank gap of zero, which says nothing decisive about their non-affine constraints. **Consequent limitation.** For the exact implemented fingerprint \(I_2\), no function \(D\)—even one with unlimited computation—can satisfy \(D(I_2(F))=\operatorname{SAT}(F)\) for every formula. On this pair its input would be identical and its required outputs different. This limitation applies to the information retained in \(I_2\), not to all polynomial invariants, all future RRLS extensions, or all algorithms. It proves neither P=NP nor P≠NP. The next candidate must retain information this pair loses; fitting a different classifier to these same features cannot repair that loss. ## Composition: what is preserved and what is missing For conjunctions on disjoint variable sets, incidence matrices are block diagonal up to permutations. Their ranks add, and their Gram traces add at every fixed degree: \[ r(F\land H)=r(F)+r(H), \qquad m_k(F\land H)=m_k(F)+m_k(H). \] For the recognized affine systems, coefficient ranks add, but the inconsistency bit composes by OR: \[ \delta(F\land H)=\max(\delta(F),\delta(H)). \] This follows because the combined right-hand side belongs to the block-diagonal column space exactly when both component right-hand sides belong to their respective column spaces. Augmented ranks themselves do not generally add: there is one shared augmented column. The experiment checked 32 disjoint compositions against these rules. Clause-count additivity in those tests uses nonempty clauses; normalization can merge repeated empty clauses. Shared variables require more information. Consider \[ F(x)=x,\qquad H(x)=\neg x,\qquad C(x)=x. \] The two factors have identical unlabelled fingerprints and are both satisfiable, yet \(F\land C\) is SAT and \(H\land C\) is UNSAT. Variable complementation is allowed when comparing an isolated formula, but a shared boundary must keep its orientation consistent across pieces. An exact summary for an ordered boundary \(B\) is \[ R_F(B)=\{b:\exists u\ F(b,u)\}. \] If two components share only \(B\), their boundary relations combine by intersection. The included `boundary_invariants.py` computes this small relation by explicit bounded enumeration and counts the assignments visited. It is a diagnostic microscope, not a polynomial general solver. A summary that answers correctly in **every boundary context** must distinguish any two different boundary relations. If \(a\in R\triangle S\), conjoin unit clauses fixing the boundary to \(a\); the resulting SAT answers differ. There are \(2^{2^b}\) relations on \(b\) bits, so lossless summaries for all such relations need at least \(2^b\) bits in the worst case. This is a counting statement in boundary width. Arbitrary relations can require exponentially large input formulas too, so it is **not** a super-polynomial lower bound in CNF input length. ## Verification, cost, and preserved failures Across the two completed cohorts there are 1,602 independently checked base decisions and 1,602 checked bijective transformations: 3,204 formula records. The original cohort has 953 SAT and 393 UNSAT labels; the fresh cohort has 191 SAT and 65 UNSAT labels. All 37 project test groups passed. New tests include exhaustive small finite-field rank comparisons, every Boolean truth table of arity up to three for local XOR-recognition soundness, independent dense-matrix checks of the sparse moment formulas, certificate corruption rejection, normalization and transformation cases, composition, and budget behavior. Truth checking and feature replay have different scopes: - SAT models and generic UNSAT RUP proofs use the separate scan-based checker. - Fresh parity UNSAT certificates are checked by `verify_affine_invariant.py`, which imports no producer or solver. It exhaustively verifies each bounded local truth table, then checks that the cited equations sum to \(0=1\). - Transformation maps are independently checked as exact bijections with the claimed signed clause image. - Every saved feature vector and collision catalogue was recomputed with the feature implementation. This catches persistence/replay errors; it is not an independently implemented feature checker or proof-assistant verification. The first generic labeling attempt on `fresh-parity-11-00-1` exceeded the RUP checker's 20,000,000-work cap. Its proposed answer remained unverified in that attempt. The partial 129-case run, failed check, and protocol are retained. The labeling policy was then amended for the entire fresh parity family to use exact XOR elimination and independent certificates. The input list and feature selection were unchanged. No difficult input was removed because of its outcome. A feature-replay check also exposed an in-memory tuple versus saved JSON-array mismatch in histogram keys. The keys were made JSON-native; serialized feature values did not change. The original sources are retained under `source-at-benchmark/`. A later selector metadata correction states its actual stop reason, “no training collisions remain”; it did not change selected operators or arithmetic. On the original completed run, base labeling took approximately 7.03 seconds of solver time plus 12.98 seconds of independent checking. Profiling the bases took 20.87 seconds and their transformed copies 20.56 seconds. The moment extension over those records took 6.19 seconds in the completed refinement run. Fresh labeling took 0.32 seconds plus 0.32 seconds of checking; profiling its 512 records took 4.87 seconds. These are one-run in-memory timing sums, excluding generation, serialization, clustering, re-audits, and development retries. They are not speedup claims or worst-case bounds. The fixed-width local scans, finite-field elimination, fixed-degree moments, and finite color-refinement trace have polynomial bounds. The selected work counters are partial implementation proxies, not a full Turing-machine bit-cost measurement. **Dataset truth labeling can still require exponential search.** The engine cannot treat that oracle cost as part of a polynomial SAT decision algorithm and then omit it. ## Run it on a PC Python 3.10 or newer and the standard library are sufficient for this extension. It was tested with Python 3.12 on Linux; Windows commands are provided but were not separately executed on Windows. Place CNF JSON files in a directory, then run: ```powershell py -3 invariant_discovery.py my-cnf-inputs --output-dir my-discovery py -3 -I verify_invariant_evidence.py --directory my-discovery ``` The first command profiles, labels, clusters, tries the finite extension catalogue, and saves collision witnesses. It retains invalid, unresolved, and budget-limited records separately. The independent archive checker checks the labelled subset. An arbitrary user batch is discovery data, not a held-out evaluation. Reproduce the final collision directly: ```powershell py -3 invariant_discovery.py invariant-results/examples/final-collision --output-dir collision-replay py -3 -I verify_invariant_evidence.py --directory collision-replay ``` Profile a single formula without any SAT oracle: ```powershell py -3 invariant_refinement.py invariant-results/examples/final-collision/sat.json --output fingerprint.json ``` Recheck the saved studies and run tests: ```powershell py -3 -I verify_invariant_evidence.py py -3 -I verify_invariant_evidence.py --directory invariant-results/refinement py -3 invariant_experiment.py --recheck py -3 invariant_refinement_experiment.py --recheck py -3 -m unittest discover -v ``` Use `python3` in place of `py -3` on Linux/macOS. Running the experiment scripts without `--recheck` regenerates their results and overwrites those result files. The reusable achievement is an auditable mechanism for identifying **which distinctions a proposed invariant loses**, adding a specified mathematical operator, and checking whether the improvement survives fresh inputs. The unresolved target remains a uniformly computable invariant and decoder that work for every SAT formula with a proved total polynomial bound.