# Applying the RE engine to the structure inside SAT

Date: 2026-09-05. Research companion to the Reality Bit Engine and RRLS audit.

**Outcome:** a new engine stage recovers affine relationships from ordinary CNF clauses, derives independent coordinates, preserves nonlinear residual constraints, and selects a fallback when the transformed representation is unsuitable. The mathematical result is an exact reduction with explicit limits. This work does not resolve P versus NP or establish a new complexity class.

## 1. The precise refinement

P and NP are classes of decision problems. P concerns deterministic polynomial-time decision algorithms; NP concerns polynomially verifiable positive certificates. The input-length variable usually written \(n\) is separate from those class names. NP does not mean “non-polynomial.” SAT provides a concrete target because a polynomial-time algorithm deciding every SAT instance would imply P = NP. [Cook's official problem description](https://www.claymath.org/wp-content/uploads/2022/06/pvsnp.pdf)

The user's representation hypothesis can be investigated through instance structure. For a CNF formula \(F\), record

\[
\Phi(F;R,\sigma)=(L,n,m,b,r,k,q,w_\sigma),
\qquad k=n-r.
\]

| Symbol | Meaning |
|---|---|
| \(L\) | Length of an explicit input encoding, including variable indices |
| \(n,m\) | Number of declared variables and normalized clauses |
| \(b\) | Largest scope of a locally inspected clause group |
| \(r\) | Rank of the recovered consistent affine equations |
| \(k\) | Independent bits remaining under those equations |
| \(q\) | Largest residual scope after affine substitution |
| \(w_\sigma\) | Largest intermediate boundary size under a specified elimination order |

These are descriptors of a representation and solving route. They are not a complete intrinsic difficulty score. Inconsistent reductions report the pivots accumulated before the conflict, not a falsely asserted full matrix rank. The code records literal occurrences; that count alone is not the bit length \(L\).

The practical question becomes: can the engine recover a representation with inexpensive residual computation, while charging for recovery itself?

## 2. What was implemented

The new `re_sat.py` uses the existing RRLS exact factor-elimination engine. `dispatcher.py` also uses the existing v0.19/v0.20 Python DPLL solver. Unmodified copies are included with source hashes in `vendor/ORIGINS.json`.

The input contains only a variable count and ordinary signed CNF clauses. No planted equation labels or hidden basis are passed to discovery.

1. Normalize duplicates and tautologies, preserving the formula's solution set.
2. Group clauses mentioning exactly the same set of variables.
3. Enumerate each bounded local relation, rather than enumerate a global truth table.
4. Recover all affine consequences of that local relation as an equation basis.
5. Replace a group completely only when its relation is exactly affine; otherwise retain the original group too.
6. Combine recovered equations by GF(2) elimination. Produce either a contradiction witness or a complete affine coordinate map.
7. Solve retained constraints in those coordinates when appropriate. Preserve the original CNF for fallback.

This is a development of the engine, using established mathematical techniques. Extraction of XOR constraints from CNF and Gaussian elimination inside SAT solvers already appear in [Soos's SAT research](https://www.msoos.org/wordpress/wp-content/uploads/2010/08/PoS10-Soos.pdf). No priority or novelty claim is made.

## 3. Exact recovery of local hidden relationships

Let a local relation have satisfying states \(S\subseteq\mathbb F_2^b\), with \(S\ne\varnothing\). Choose \(s_0\in S\), and define

\[
V=\operatorname{span}\{s\oplus s_0:s\in S\}.
\]

Then

\[
\boxed{a\cdot x=a\cdot s_0\text{ for every }x\in S
\iff a\in V^\perp.}
\]

**Proof.** The equation holds on all of \(S\) exactly when \(a\cdot(s\oplus s_0)=0\) for every \(s\in S\). By linearity, this is equivalent to orthogonality to their span. A basis of \(V^\perp\) therefore generates every affine equation true throughout the relation.

Moreover,

\[
S\subseteq s_0+V,
\qquad S=s_0+V\iff |S|=2^{\dim V}.
\]

Containment follows from the definition of \(V\); equal finite cardinality makes containment equality. This gives an exact test for whether the affine description loses information. If \(S\) is empty, the contradictory equation \(0=1\) represents it directly.

A nonlinear relation can still reveal an affine restriction. For instance,

\[
S=\{(1,0,0),(1,1,0),(1,0,1)\}
\]

implies \(x_0=1\), but that equation alone admits a fourth state. The engine discovers the restriction and retains the nonlinear remainder. It does not mislabel the affine hull as the original relation.

## 4. A worked recovery, calculated by the engine

The supplied example consists of twelve ordinary three-literal clauses. The engine reconstructs

\[
\begin{aligned}
x_0\oplus x_1\oplus x_2&=0,\\
x_2\oplus x_3\oplus x_4&=1,\\
x_0\oplus x_4\oplus x_5&=1.
\end{aligned}
\]

The rank is three. With free bits \(a,b,c\), its complete solution map is

\[
\boxed{
\begin{aligned}
x_0&=1\oplus b\oplus c,&x_1&=a\oplus c,\\
x_2&=1\oplus a\oplus b,&x_3&=a,\\
x_4&=b,&x_5&=c.
\end{aligned}}
\]

There are exactly eight satisfying assignments. Six displayed variables reduce to three independent coordinates. The engine inspected 24 local table rows to discover the equations. `results/worked-example.json` and its solution file preserve the input and output.

In general, for consistent recovered equations \(Ax=b\), the engine constructs

\[
x=p+Nz,\qquad z\in\mathbb F_2^{n-r},
\qquad Ap=b,\quad AN=0,\quad\operatorname{rank}N=n-r.
\]

These identities prove the map is a bijection from free coordinates onto the full affine solution space. When nonlinear groups remain, their original clauses are evaluated at \(p+Nz\). This preserves precisely the original CNF solutions. The basis need not be unique, and recovered dependencies are mathematical relationships in the input, not evidence for new physical dimensions.

## 5. A boundary that cannot be removed by adding affine coordinates

The two-variable clause \(x\lor y\) has three satisfying assignments:

\[
\{(0,1),(1,0),(1,1)\}.
\]

The image of any nonempty affine set under an affine projection is affine. Every finite affine set over GF(2) has a power-of-two number of elements. Consequently:

\[
\boxed{\text{OR's three-state relation cannot be the affine projection of a linear system,}}
\]

even if the linear system has auxiliary coordinates.

**Proof.** An affine set is \(p+V\). Under an affine map \(x\mapsto Bx+c\), its image is \(Bp+c+B(V)\), a translated vector space, of size \(2^{\dim B(V)}\). Three is not a power of two.

This rules out one proposed universal route: exact solution-preserving linearization with affine decoding. It does not rule out nonlinear encodings, other algorithms, or decision-only equisatisfiable transformations. Those would need their own correctness and cost arguments. It is not a proof of P ≠ NP.

## 6. Frozen experiments and the failure they exposed

The first benchmark contains 28 synthetic cases: eight graph-parity instances, eighteen separately seeded affine/ordinary/mixed CNFs, and two substitution-expansion cases. Inputs, outputs, baseline proofs, raw timing samples, and source hashes are retained under `results/`.

Timings below are medians of three measured runs following one excluded warm run, on this shared Linux x86-64 runtime with Python 3.12.13. Construction of test inputs and independent certificate checking are excluded for both methods. Discovery, coordinate construction, residual solving, and checking a lifted witness are included in the RE timing. Timings are not portable guarantees.

| Input | RE result | RE median | Existing DPLL result |
|---|---|---:|---|
| 10 variables, 40 clauses, graph parity | UNSAT, checked XOR contradiction | 0.432 ms | UNSAT in 3.571 ms |
| 15 variables, 96 clauses, graph parity | UNSAT, checked XOR contradiction | 1.493 ms | Reached 500,000-unit literal-work budget |
| 28 variables, 512 clauses, graph parity | Rank 7, 21 free bits, exactly **2,097,152** models | 25.996 ms | Found one satisfying model in 12.084 ms |
| Same 28-variable structure, inconsistent charge | UNSAT, **eight-equation** contradiction | 26.275 ms | Reached the same work budget |
| 17 variables, 29 clauses, substitution expansion | Exactly 896 models; residual scope grows 3 → 10 | 5.651 ms | Found a model in 0.335 ms |
| 37 variables, 69 clauses, substitution expansion | Residual scope grows 3 → 20; declared table budget exceeded | 0.683 ms to refusal | Found a model in 1.574 ms |

The baseline is our existing research DPLL, not a modern competitive SAT solver. The RE counting route performs a stronger task than finding one model. Budget-exhausted baseline cases have no claimed completed-runtime speedup.

The graph cases encode one parity constraint at each vertex of a complete graph. Each edge variable occurs in two equations. XOR-ing every equation cancels every variable. Odd total charge produces \(0=1\), giving a global contradiction although every local equation is individually satisfiable. For a connected graph with \(E\) edges and \(V\) vertices, the constraint matrix has rank \(V-1\): a dependency selects a vertex subset with no edge crossing to its complement, so only the empty and whole subsets are possible. Consistent charge therefore gives \(2^{E-V+1}\) models. This explains and proves the tested counts.

Across the eighteen ten-variable cases, recovered ranks were 7 or 8 in the affine and mixed families, but **zero in all six ordinary 3-SAT cases**. Exact counts matched exhaustive enumeration in all eighteen. This is a deliberate check against claiming that every input must expose useful affine structure.

The substitution-expansion family demonstrates why eliminating variables is not automatically an improvement. A ternary XOR chain expresses one variable as a parity of many free bits. Substituting it into one three-variable OR clause makes that clause depend on all those free bits. The current map is exact, but the proposed dense residual representation is expensive.

## 7. The engine revision prompted by that failure

The original experiment remains frozen. A separate `dispatcher.py` now:

- accepts a directly verified affine solution or contradiction;
- uses the reduced factor engine when there is positive rank reduction, at most twelve free bits, and no increase in the largest residual scope;
- otherwise retains the original CNF and invokes the existing DPLL solver;
- reports unresolved if the selected bounded route exhausts its budget.

The twelve-bit threshold is a declared implementation policy, not a theorem or an optimized universal constant. The scope comparison is a conservative heuristic. The dispatcher does not claim global optimality or an overall complexity improvement for every input.

It resolves the preserved 37-variable expansion case through the original CNF. After fixing this rule, a fresh set of eighteen cases used seeds 180001–180006, distinct from both the first benchmark and unit tests. **All eighteen decisions matched exhaustive enumeration.**

| Fresh family, six cases each | Dispatcher median | DPLL-only median |
|---|---:|---:|
| Affine | 0.387 ms | 0.188 ms |
| Ordinary 3-SAT | 0.950 ms | 0.209 ms |
| Mixed | 0.546 ms | 0.236 ms |

Discovery overhead dominates these tiny examples. The result is a correctness and representation-routing improvement, with useful parity contradiction handling. The measurements do not show a general runtime win. The dispatcher optionally returns exact model counts on its affine/reduced routes; DPLL returns a decision and proof or witness.

## 8. What a proof of P = NP would still require

For this architecture, computation decomposes as

\[
T(F)=T_{\rm discovery}(F)+T_{\rm map}(F)
+T_{\rm residual}(F)+T_{\rm verification}(F).
\]

Local enumeration can cost \(\sum_g O(m_g b_g2^{b_g})\). Substitution can require \(\sum_j2^{q_j}\) table entries. Exact elimination can create buckets of size \(2^{w_\sigma+1}\). These are costs of this implementation, not lower bounds on all algorithms. Width-dependent elimination is an established technique with an exponential width parameter. [Dechter's bucket-elimination framework](https://www.ics.uci.edu/~csp/R48a.pdf)

A sufficient theorem for P = NP would be: one uniform algorithm, on every SAT input of encoded length \(L\), discovers and verifies a correct representation and decides it in total time at most \(CL^c\), for fixed constants \(C,c\), on both satisfiable and unsatisfiable inputs. Small width is one possible route, not a necessary condition: the parity examples are easy algebraically despite large graph-based bucket estimates.

Producing a short representation after exhaustive search does not establish that theorem. Giving the solver the correct hidden representation for free does not establish it either. A polynomial-time computable change of encoding cannot evade this accounting: composing the change with the proposed polynomial solver is itself a polynomial algorithm for the original problem.

The remaining empirical target is broader structure discovery that reliably reduces total cost on difficult, independent inputs. The remaining mathematical target is a universal bound or an applicable impossibility theorem. Neither follows from renaming P/NP, assuming seven layers, or assigning an unexplained remainder to another coordinate.

## 9. Verification scope

All **15 test groups passed**. Checks include every three-variable Boolean relation, completeness of its affine consequence basis, fresh CNF counts, full reduced-assignment reconstruction, explicit nonlinear remainder preservation, parity contradictions, empty domains, arbitrary-precision counts, budget handling, and ten corrupted reduction variants.

`verify_reduction.py` is a standalone standard-library checker. It does not import the discovery engine. It independently verifies local clause implications/equivalences and the complete affine map using a different pivot convention, or checks the explicit XOR combination yielding \(0=1\). It was also run in isolated Python mode on the largest contradiction certificate.

For fully affine inputs it verifies the final model count. With nonlinear residuals, its claim is limited to the correct complete affine map with original residual constraints retained. It does not independently certify arbitrary residual model counts. The small reported residual counts are checked by exhaustive reference enumeration; additional tests compare the existing factor engine with exhaustive solutions. Profiling/timing fields are diagnostics, not trusted proof claims. There is no proof-assistant verification and no claim of a solved Millennium Prize problem.