# RRLS: A Proof Attempt at Universal Relational Compilation

5 September 2026 · Audit of RRLS Studio v0.13 and a tested refinement

**This work does not prove P = NP or P ≠ NP.** It gives a constructive proof that a two-word vocabulary already expresses an NP-complete problem, a polynomial compiler for a restricted family, an explicit obstruction to that compiler's universality, and a reproducible implementation improvement. These results identify what the proposed universal compiler must still accomplish.

The actual `RRLS_Studio_v13_Windows_Source.zip` and its research report were inspected. Its SAT module is preserved as `rrls_pnp_v13.py`. The experiments below were run against that code, not inferred from screenshots or earlier summary claims.

## 1. The universal language claim

Let \(F\) be an ordinarily encoded CNF formula and \(L\) its bit length. A uniform deterministic compiler \(C\) and interpreter \(D\) would settle the question if, for every input,

\[
D(C(F))=1\iff F\text{ is satisfiable},
\]

and both complete computations have polynomial worst-case bit cost, with polynomial-size intermediate representations.

**Theorem 1 — Efficient encoding cannot conceal the decision cost.** Suppose \(C\) runs in time \(p(L)\), produces an encoding of length at most \(p(L)\), and \(D\) decides its satisfiability correctly in time \(q\) of that length, for fixed polynomials \(p,q\). Then SAT is decided in time at most

\[
p(L)+q(p(L)),
\]

which is polynomial. Since SAT is NP-complete, P = NP follows.

**Proof.** Run the compiler and then the interpreter. Correctness follows from the stated equivalence; the time bound follows by addition and composition of polynomials. ∎

Conversely, if P = NP, identity compilation into ordinary CNF followed by a polynomial SAT algorithm would meet these conditions. Thus the existence of a universally efficient language/compiler/interpreter is an equivalent formulation of the open target, not an independently established reason that the target must be true. The reduction framework and SAT completeness are stated in [Cook's official problem description](https://www.claymath.org/wp-content/uploads/2022/06/pvsnp.pdf).

A practical proof attempt must establish a uniform selection procedure, correct YES and NO answers, bounded representation and arithmetic sizes, and bounded total work. A polynomial-size dictionary supplied as unexplained advice is not enough: its construction or uniform generation must be accounted for. A finite benchmark cannot establish the required universal quantifiers.

For a rewrite implementation, a sufficient additional termination argument is an integer potential \(\Phi(F)\), bounded polynomially in the original input length, that decreases at every chosen nonterminal rewrite. This must accompany a polynomial-time selector and polynomial bounds on every intermediate state and operation. Merely asserting that some useful relation exists at each step does not supply these bounds.

## 2. Two individually tractable relations already express all 3-SAT

Use the fixed Boolean relation vocabulary

\[
\Gamma=\{R_{\lor},R_{\ne}\},
\qquad R_{\lor}(a,b,c)\iff a\lor b\lor c,
\qquad R_{\ne}(u,v)\iff u\oplus v=1.
\]

A formula containing only positive applications of \(R_{\lor}\) is satisfied by setting all variables to one. A system containing only \(R_{\ne}\) constraints is an affine system over \(\mathbb F_2\). Each separate constraint language is tractable.

**Theorem 2 — The combined fixed language is NP-complete.** For any 3-CNF formula \(F(x_1,\ldots,x_n)\), introduce variables \(p_i,q_i\) and impose

\[
R_{\ne}(p_i,q_i),\qquad i=1,\ldots,n.
\]

Replace each positive literal \(x_i\) by \(p_i\), each negative literal \(\neg x_i\) by \(q_i\), and each three-literal clause by one application of \(R_{\lor}\). Call the result \(F_\Gamma\). Then

\[
\boxed{F\text{ is satisfiable}\iff F_\Gamma\text{ is satisfiable}.}
\]

**Proof.** Given a satisfying assignment \(x\), set \(p_i=x_i\) and \(q_i=1-x_i\). Every complement constraint holds and every clause retains its truth value. Conversely, each satisfying assignment of \(F_\Gamma\) has \(q_i=1-p_i\); take \(x_i=p_i\), and every original clause is satisfied. Each original assignment has exactly one complement extension, so the correspondence is bijective. ∎

The construction uses \(2n\) variables and \(m+n\) constraints for an input with \(m\) clauses. It is polynomial under the standard dense representation, with \(n\) the number of explicitly represented variables. Arbitrarily large sparse variable identifiers can first be renamed densely. The utility `compile_two_relations` expects this canonical dense convention; the deployed solver independently densifies identifiers in its JSON input.

Membership in NP follows by checking an assignment against the fixed constant-arity relations. The reduction proves NP-hardness, and together they prove NP-completeness.

Therefore even all of the following can hold simultaneously:

- the dictionary has exactly **two entries**;
- recognizing each relation is immediate from its label;
- every local relation is individually tractable;
- compilation has linear-many constraints;
- deciding the **joint** system remains NP-complete.

The unresolved difficulty can reside entirely in compatibility across shared variables. This theorem does not prove the joint system requires exponential time. A polynomial solver for it would prove P = NP.

The experiment checks the reduction on all 256 subsets of the eight possible three-variable full-scope clauses, inspecting all 64 assignments of the six-variable encoding: **16,384 complete assignment checks**. It also checks all 256 original assignments on each of 80 fresh eight-variable cases, for **20,480 further lifted-assignment comparisons**. These tests check implementation; the argument above proves the construction for arbitrary finite 3-CNF formulas in its stated input convention.

## 3. A test for compatible local laws

The engine now computes preservation witnesses for six operations: constant zero, constant one, coordinatewise AND, coordinatewise OR, majority, and ternary XOR. A relation is preserved when applying the operation to any suitable tuple of its satisfying points yields another satisfying point.

For a fixed finite Boolean constraint language, a **common** appropriate operation across all relations supplies the familiar Schaefer tractability cases. The condition must hold across the language, rather than choosing a different operation independently for each relation. See [Allender, Bauland, Immerman, Schnoor, and Vollmer](https://www.cs.umass.edu/~immerman/pub/cspJournal.pdf) for the algebraic classification and its refinements.

For the two-word example, direct enumeration gives:

| Operation | OR3 preserved? | NEQ2 preserved? |
|---|---|---|
| Constant zero | No | No |
| Constant one | Yes | No |
| AND | No | No |
| OR | Yes | No |
| Majority | No | Yes |
| Ternary XOR | No | Yes |

There is no common operation in this list. For example, OR3 permits \(001,010,100\), whose coordinatewise majority is \(000\), which it forbids. NEQ2 permits \(01,10\), whose OR is \(11\), which it forbids. `results/language-audit.json` contains the actual counterexample points.

The classifier applies to its stated fixed-language Boolean CSP model. It is not a proof that any particular finite instance is hard, nor a classification of every possible compiler or richer representation.

A corresponding boundary exists in the ALLDIFFERENT story. One matching constraint is tractable. But on the domain \(\{0,1,2\}\), a pairwise ALLDIFFERENT constraint on each graph edge is exactly graph 3-coloring. A conjunction of these elementary constraints expresses the NP-complete coloring problem. The v0.13 matching recognizer appropriately requires complete cross-object conflict cliques; arbitrary coloring graphs do not satisfy that global matching pattern.

## 4. A polynomial coordinate change that actually helps

The new primitive finds \(s\in\{0,1\}^n\) such that replacing \(x_i\) by \(x_i\oplus s_i\) makes the entire CNF Horn. Horn means that every clause contains at most one positive literal.

For every pair of literals \(\ell_i,\ell_j\) in a clause, the transformed pair must not both be positive. Let

\[
t(\ell_i,s)=\begin{cases}s_i&\ell_i=x_i,\\\neg s_i&\ell_i=\neg x_i.\end{cases}
\]

This is the condition that the transformed literal is negative. Construct

\[
H_F(s)=\bigwedge_{C\in F}\ \bigwedge_{\ell_i,\ell_j\in C,\ i<j}
\bigl(t(\ell_i,s)\lor t(\ell_j,s)\bigr).
\]

**Theorem 3 — Exact sign-renaming recognition.** \(H_F\) is a 2-CNF formula, and

\[
H_F(s)=1\iff F(x\oplus s)\text{ is Horn}.
\]

**Proof.** A clause has at most one positive literal exactly when none of its literal pairs is simultaneously positive. Each generated binary clause expresses that condition for one pair. Conjoining every pair condition proves the equivalence. ∎

The compiler uses \(\sum_C\binom{|C|}{2}\) pair constraints. With dense variable names this is polynomial in input length, and for bounded clause width it is linear-many pairs. A 2-SAT algorithm finds a sign assignment or proves no such assignment exists; a Horn algorithm then solves the renamed formula. Finally, the inverse sign change maps the answer back. This is an established tractable family; [Chandru and colleagues](https://link.springer.com/article/10.1007/BF01531069) give earlier characterizations and algorithms. No discovery of renamable-Horn satisfiability is claimed here.

The implementation caps pair generation at 250,000 per attempt. Exceeding that resource policy skips the primitive; it does not establish unsatisfiability. Failed recognition also means only that this particular primitive does not apply.

**Proposition 4 — Sign flips cannot make every CNF Horn.** Consider

\[
F=(x\lor y\lor z)\land(\neg x\lor\neg y\lor\neg z).
\]

After any sign flips, let the first clause have \(a\) positive literals. The other then has \(3-a\). Horn would require both \(a\le1\) and \(3-a\le1\), which is impossible. This satisfiable formula has six models. All eight flips are also checked in `renaming-obstruction.json`.

This obstruction concerns sign flips. It says nothing by itself about the power of arbitrary nonlinear transformations, auxiliary variables, or a general polynomial SAT algorithm.

## 5. Correcting the proof criterion and the implementation

Zero branch nodes is neither necessary nor sufficient for polynomial time. A single named operator can enumerate \(2^n\) assignments internally. The included one-operator demonstration evaluates \(64,1024,16384,262144\) rows at \(n=6,10,14,18\), with no explicit SAT split operator. Conversely, a binary search tree of depth at most \(a\log_2 L\) has at most \(2L^a-1\) nodes. If each node's full work is polynomial, that branching algorithm is polynomial.

The recurrence \(T(n)\le2T(n-1)+\operatorname{poly}(n)\) supplies an exponential **upper bound** under its cost assumptions. It is not an exponential lower bound and does not prove that no tighter analysis exists. A fitted exponential curve on a short finite range does not supply such a lower bound either.

Four concrete source changes accompany the new primitive:

1. **Recheck reduced formulas.** v0.13 dispatched special languages only on entry to a recursive call. The refinement tries them again when preprocessing has changed the formula, before starting another split.
2. **Save actual cores.** The original `_record_core` stored dimensions, width counts, and a digest. That is insufficient to reconstruct a specimen. The refinement stores bounded clause snapshots that can be replayed. These are formulas unrecognized by the current rules, not mathematically irreducible objects.
3. **Preserve earlier assignments.** Some subsolvers returned assignments for every numeric identifier up to their largest variable, including variables absent from their residual. Merging these could overwrite an ancestor's choice. Returned models are now restricted to the subproblem's actual variables.
4. **Densify external identifiers.** Allocation and iteration use the number of distinct encountered variables, not the largest identifier. A regression case uses an identifier \(2^{200}\) while the solver handles only two distinct variables.

The merge defect also appeared on a complete 40-variable test input: v0.13 raised `RRLS SAT solver returned invalid SAT assignment`. Its final witness check correctly prevented that result from being accepted. An isolated rerun changing only subsolver output scopes, without adding Horn renaming, produced a directly verified satisfying witness. This is recorded in `merge-defect-ablation.json`.

The refinement adds named dispatch counts/times, pair counts, full external timings, and explicit budget outcomes. These are useful execution measurements; they are not a formal accounting of every Turing-machine bit operation. The proof report remains false for `P_equals_NP_proved` irrespective of the finite branch count.

## 6. Measured results and replay

The suite contains 40 cases: six disguised Horn formulas, eight random 3-SAT formulas, four pigeonhole formulas, eight parity formulas, six compiled two-relation formulas, and eight graph-coloring formulas. Some structured families reproduce earlier patterns; the random, disguised, and compiled cases use recorded fresh seeds. There is no claim that all 40 are previously unseen formula families.

Each method has three measured repetitions after one excluded warm-up, in alternating order. Complete in-memory solving and input normalization are timed. Import time and independent evidence construction/checking are excluded. No asymptotic fit is made.

All **40 refined decisions** agreed with independent evidence. Depending on the family, evidence is a directly checked SAT assignment, a separately generated and checked DPLL proof tree, an exhaustively checked local contradiction, or a checked pigeonhole subformula. A standalone checker importing no RRLS solver validated all 40 case results and all 64 saved core replays.

| Case | v0.13 | Refinement | Branches before → after |
|---|---:|---:|---:|
| Disguised Horn, 80 variables, seed variant 0 | 412.747 ms | 14.496 ms | 5 → 0 |
| Disguised Horn, 160 variables, variant 0 | 2,085.619 ms | 27.623 ms | 17 → 0 |
| Disguised Horn, 160 variables, variant 1 | 1,947.410 ms | 27.511 ms | 16 → 0 |
| Two-relation encoding, 24 original variables, variant 0 | 106.934 ms | 123.304 ms | 13 → 13 |

The 160-variable variant 0 is about **75.5 times faster** in this comparison. That is a result for a constructed tractable family, not for general SAT. A baseline error is not included as a valid successful solve in any claimed speedup.

| Family | Cases | Branch total, v0.13 | Branch total, refinement | Median refined time |
|---|---:|---:|---:|---:|
| Disguised Horn | 6 | 49 across the five completed baseline runs; one error | 0 | 13.717 ms |
| Random 3-SAT | 8 | 101 | 101 | 103.118 ms |
| Two-relation encodings | 6 | 32 | 32 | 53.555 ms |
| Graph 3-coloring | 8 | 37 | 36 | 59.596 ms |
| Pigeonhole | 4 | 0 | 0 | 4.941 ms |
| XOR | 8 | 0 | 0 | 4.792 ms |

Generic random and two-relation cases did not lose their branch counts. Several families became slower because of additional normalization, instrumentation, or unsuccessful recognition. The change should not be advertised as a general performance improvement.

The replay set is the **first 64 distinct captured baseline cores**, subject to the declared limits. Of these, **48 were recognized as renamable Horn and solved in one node with zero branching**. Those 48 came from the deliberately disguised Horn families. The selection is biased by suite order and family design; it is not an estimate for arbitrary SAT inputs. The remaining 16 replayed cores still required branching. All 64 had separately checked outcomes.

This implements a concrete cycle: capture the actual formula, test a new algebraic recognizer, execute it, then independently check the outcome. The recognizer was designed before this evaluation; the engine did not autonomously invent the theorem or rewrite its own source.

## 7. Reproduce and inspect

The bundle is a standard-library Python command-line extension to RRLS v0.13. Python 3.10+ is required; execution here used Linux and Python 3.12.13. Windows commands are supplied but were not independently run on Windows.

```powershell
py -3 -m unittest discover -v
py -3 rrls_audit_cli.py results/inputs/two-relations-24-0.json --output answer.json
py -3 -I verify_audit_evidence.py --answer answer.json --input results/inputs/two-relations-24-0.json
py -3 -I verify_audit_evidence.py
```

There are **12 passing test groups**, including exhaustive finite reduction checks, renaming checks, sparse identifiers, saved-core budgets, redispatch, corrupted evidence rejection, and the merge regression.

`py -3 experiment.py` regenerates the benchmark, captured cores, and evidence; it overwrites its result files. `py -3 proof_demonstrations.py` regenerates the finite obstruction, one-operator scan, and isolated merge-defect demonstration. Use `python3` instead of `py -3` on Linux/macOS.

The CLI checks SAT witnesses directly and obtains an independent DPLL proof for an UNSAT candidate under a separate 5,000,000-unit search-work budget. Exhausting that proof budget yields `UNVERIFIED_BUDGET`, not a verified answer. Consequently the checked CLI can refuse to certify an answer that an algebraic route found quickly. This proof-generation cost is additional to the solver-only timings above. The standalone checker can verify a saved answer against the original input and its dense variable mapping; the 40 benchmark answers and 64 core outcomes also have separate saved evidence.

The key files are `refined_solver.py`, `relation_language.py`, `results/evaluation.json`, `results/language-audit.json`, and `results/standalone-evidence-check.json`. The original engine and the independent proof-checking components are preserved with source hashes.

The remaining mathematical obligation is a uniform polynomial bound for **solving every jointly constrained system** after compilation, including the two-relation language above. Dictionary compression, fewer branches on selected families, and additional coordinate changes have not supplied that argument.