# A proved self-optimization step for the RE SAT engine

Date: 2026-09-05. Revision 0.2 of the SAT structure laboratory.

**Result:** the engine now learns a route policy from its own execution measurements, reuses a checked vocabulary of local relations, reduces the learned policy, and applies it to new inputs. Its policy learner was then simplified using a proved separability identity. The deployed learner returns the same policy about 2.15 times faster in the recorded run. **This proves a bounded optimization claim, not P = NP.**

## 1. What “run the engine over itself” means here

The input to the second layer is the first layer's execution record: structural features, which route completed, and measured time. It is not an unexplained recursive invocation.

The completed loop is:

1. Run the two existing solving routes on training formulas.
2. Store reusable local relationships under names independent of global variable indices.
3. Learn a route policy from the recorded outcomes and times.
4. Use the engine's Boolean ANF and decision-diagram routines on that policy.
5. Freeze the vocabulary and policy before evaluating fresh formulas.
6. Inspect the errors in representation choice, refine the candidate features, and evaluate another fresh batch.
7. Factor the learner's own optimization problem into independent choices, prove that factorization, and deploy the equivalent faster learner.

The local recognition rules and two candidate feature schemes were supplied in code during this development. The engine automatically derived local affine consequences, collected dictionary entries, measured routes, and selected among those supplied alternatives. It did not autonomously invent unrestricted new mathematics or rewrite arbitrary source code.

## 2. Proof: constructing a local relation without repeated clause evaluation

After normalization, a clause on a fixed scope of \(b\) variables contains one literal per variable and is not tautological. Exactly one assignment makes every literal false: set each positive literal's variable to zero and each negative literal's variable to one.

Let \(B\) contain those forbidden assignments for all clauses in a group. Then the group's entire relation is

\[
\boxed{S=\mathbb F_2^b\setminus B.}
\]

**Proof.** The conjunction fails exactly when at least one clause fails. A clause fails at its unique forbidden assignment, so the conjunction's failure set is precisely their union \(B\).

The previous implementation evaluated each clause against each local assignment, costing up to \(O(mb2^b)\) literal checks for \(m\) clauses. The new implementation extracts the forbidden assignments directly from their literals. General affine-hull recovery may still enumerate the local cube, but it no longer repeats every clause at every point.

Three exact cases avoid that enumeration during discovery:

- No forbidden states: the group is unconstrained.
- Every state forbidden: the group is contradictory.
- Exactly half the states forbidden, all with the same parity: the group is one parity equation.

For the parity case, each parity class has \(2^{b-1}\) elements. A set of that size contained in one parity class equals that class, so its complement is the opposite parity equation. This recognition does not require a supplied hidden basis.

There is also a useful negative recognition rule. If \(b\ge2\) and exactly one state is forbidden, the allowed set has \(2^b-1>2^{b-1}\) states. A nontrivial affine equation holds on only \(2^{b-1}\) states. Therefore no nontrivial affine equation holds on the entire allowed set. The engine retains that nonlinear relation instead of attempting to replace it by an empty set of constraints.

The general case still uses the previously proved affine-hull construction. None of these rules turns a nonlinear relation into a linear one without retaining the necessary residual.

## 3. Proof: vocabulary reuse preserves the represented relation

A dictionary key is \((b,B)\), expressed in local bit positions. A value contains affine equations and an exactness flag. Every loaded value is checked on every local assignment before use. The original separate reduction verifier also checks completed certificates against their clauses.

Renaming the local positions to a new ordered global variable scope is a bijection of assignments. Applying the same renaming to a verified equation therefore preserves its implication or equivalence. This justifies reuse under different global variable names. The key does not promise canonicalization under every rotation or permutation of the local positions.

The training run produced **35 dictionary entries**. In the final fresh evaluation, the selected affine routes recorded **224 hits and 62 misses**. Unseen relations were derived when needed; the frozen dictionary was not changed by test inputs. In particular, the larger graph cases used parity widths absent from training, so their successful recognition came from the general recognition rule, not memorizing those complete problems.

## 4. The first representation lost a distinction

The first policy used three Boolean features:

1. At least half the clauses belong to repeated variable scopes.
2. At least nine tenths belong to repeated scopes.
3. Some scope has at least four variables.

Pure affine inputs and some substitution-expansion inputs had the same feature value. Yet the affine route completed the former and declined the latter under its scope policy. A deterministic selector receiving only that feature value must choose the same first route for both. This is a direct information-loss obstruction for that selector, not an obstruction for SAT itself.

The first round is preserved in `self-results-round-1/`, including its source snapshot. The second candidate scheme replaces feature 2 with:

\[
\text{normalized clause count}\ge2\times\text{declared variable count}.
\]

Using training records, the engine selected this density scheme over the earlier scheme. Its resulting policy was

\[
\boxed{\text{try affine first}\iff
(\text{repeated-scope fraction}\ge1/2)
\land(m\ge2n).}
\]

Otherwise it tries DPLL first. The third feature disappeared from the selected decision function. The policy's reduced ordered decision diagram has **two nonterminal nodes**.

This is a measured routing heuristic for the supplied training distribution. Adding unused variables, changing encoding, or using a different input family can change its utility. It is not a representation-independent test of difficulty.

The runtime also compared table lookup with decision-diagram traversal. For 16,384 lookups per timed sample, medians were 0.305 ms and 3.808 ms respectively. It selected the faster table lookup. The decision diagram and ANF remain checked equivalent representations; fewer diagram nodes are not automatically fewer stored bits or faster Python execution.

## 5. The self-optimization theorem

Fix a representation \(\phi\) that maps each training formula to one of finitely many feature cells \(s\). There are two actions: DPLL and the affine route. For recorded input \(i\), let

\[
c_i(a)=(u_i(a),t_i(a)),
\]

where \(u_i\) is one if the route was unresolved and zero otherwise, and \(t_i\) is its recorded median nanoseconds. Compare summed cost pairs lexicographically: minimize unresolved choices first, then time.

For a policy \(\pi\), define

\[
C(\pi)=\sum_i c_i(\pi(\phi(F_i))).
\]

Then

\[
\boxed{
\min_\pi C(\pi)
=\sum_s\min_{a\in\{\mathrm{DPLL},\mathrm{affine}\}}
\sum_{i:\phi(F_i)=s}c_i(a).
}
\]

**Proof.** Partition the outer sum by feature cell. A policy's choice at one cell does not constrain its choice at any other cell. Each cell can therefore attain its own lexicographic minimum simultaneously. Lexicographic order on these integer pairs is preserved by addition, so replacing any cell's choice by its minimum cannot worsen the total. The simultaneous minima attain the displayed lower bound. Empty cells contribute zero; the implementation resolves ties toward DPLL.

For each of the two feature representations there are eight cells and \(2^8=256\) complete policies. The original learner examined all 512 representation-policy candidates. The deployed learner aggregates costs and makes eight independent binary choices per representation, hence **sixteen local choices**, without enumerating complete policies. It then compares the two representation optima. The later decision-diagram search is a separate fixed-size representation step.

For \(N\) records, \(q\) cells and \(A\) actions, this policy-cost minimization takes \(O(NA+qA)\) arithmetic operations, rather than enumerating \(A^q\) policies. It does not improve the worst-case complexity of the SAT routes being selected, and \(q\) itself can grow exponentially with the number of Boolean features.

The independent `verify_self_optimization.py` takes the raw records and the final policy, explicitly checks all 512 candidates, and confirms that the deployed policy attains the same optimum. The verified recorded objective is **zero unresolved first-route choices and 5,092,643 summed median nanoseconds** on the training records. That number excludes the cost of collecting those measurements; it is not the duration of the training experiment.

The faster learner preserved the selected representation and every route choice on all eight feature states. It was applied to the default `self-results/policy.json`. Its recorded median fitting time fell from **4.766 ms to 2.217 ms**, approximately **2.15×**. The originally timed policy is retained as `policy-measured.json`, and the equivalence/application record is `learner-refinement.json`.

## 6. Fresh results after the representation refinement

Round two reused only the training set for fitting: eighteen ten-variable affine/ordinary/mixed cases, eight relabeled graph-parity cases, and two expansion cases. The final test set used new seeds, fourteen-variable affine/ordinary/mixed cases, larger relabeled graph cases, and expansion cases. Formula hashes were checked for train/test overlap.

**All 28 final test cases were solved.** Eighteen fourteen-variable results were also checked by exhaustive enumeration. SAT witnesses and affine contradictions were checked independently; the more limited verification scope for nonlinear residual counts remains as stated in `STRUCTURAL_REFINEMENT.md`.

| Fresh family | Cases | Previous dispatcher median | Learned engine median |
|---|---:|---:|---:|
| Affine | 6 | 0.409 ms | 0.208 ms |
| Ordinary 3-SAT | 6 | 1.390 ms | 0.598 ms |
| Mixed | 6 | 0.768 ms | 0.455 ms |
| Graph parity | 8 | 16.256 ms | 1.508 ms |
| Scope expansion | 2 | 1.487 ms | 1.066 ms |

Across this declared batch, the ratio of summed per-case median solving times was **6.55×** versus the previous dispatcher. This is not an industrial SAT benchmark or a universal speedup. Plain DPLL remained slightly faster than the learned wrapper on the ordinary family; its median there was 0.579 ms. DPLL exhausted its declared budget on four graph cases. No completed-runtime speedup is assigned to those unfinished runs.

Measurements use three timed repetitions after one excluded warm run, in the shared Linux/Python runtime. They include normalization, feature extraction, solving, and any fallback. Independent proof checking and startup are reported separately. Training and test case construction are outside solving timers; the full training run, including reference checks and file output, took about 0.894 seconds. Vocabulary and policy validation at startup took about 0.634 ms.

Proof checking is now a major remaining cost. For one 28-variable, 512-clause contradiction:

- Previous solving median: 26.112 ms; separate checker sample: 28.791 ms.
- New solving median: 2.051 ms; separate checker sample: 28.405 ms.

Thus the solving-stage change is about 12.7×, while adding those checker samples gives roughly 54.9 ms versus 30.5 ms, about **1.8×**. The latter is a sum of a solve median and one checker measurement, not a separately repeated end-to-end benchmark. It would be misleading to claim a 12.7× improvement in fully checked latency.

## 7. Correctness of routing and its limits

The policy selects a solving route; it never supplies a truth value. If the first bounded route declines or exhausts its budget, the wrapper tries the other route. An unresolved result is never reclassified as UNSAT. Assuming the underlying routes are sound, any completed answer from either route is sound, regardless of whether the learned policy selected the fastest route.

This fallback makes the wrapper able to complete whenever at least one of these two bounded route invocations completes, subject to the declared input validation and runtime environment. Sequential fallback can still cost the sum of both routes. No constant-factor bound against the faster route is claimed.

All **28 test groups passed**, including the prior tests, every three-variable local relation, parity recognition through the supported width, all 256 Boolean route tables, frozen-cache checks, corrupted-policy rejection, representation aliasing, and sixteen separate comparisons of the new learner with exhaustive policy search. The public CLI was run using the deployed refined policy, and its resulting eight-equation contradiction passed the standalone reduction checker in isolated Python mode.

These tests and written arguments are not proof-assistant verification. The policy checker proves an optimum relative to the supplied records and candidate representations. It does not independently establish the physical truth of timing measurements or certify a universal SAT complexity bound.

## 8. Why this still does not prove P = NP

A proof of P = NP would need one uniform algorithm deciding every SAT input in polynomial total time in its encoded length. Optimizing which existing route to try does not supply that bound when both routes may still require expensive search or large residual representations. [Cook's official formulation](https://www.claymath.org/wp-content/uploads/2022/06/pvsnp.pdf)

No finite successful benchmark can establish that universal guarantee by itself. Given a finite tested set, one can construct a program that agrees on that set and deliberately fails outside it. Therefore matching all tested outputs is logically insufficient to prove unrestricted correctness or a polynomial bound. The missing ingredient is a proof about the algorithm on all inputs, not additional confidence assigned to its observed successes.

The techniques have established precedents: XOR extraction and Gaussian elimination in [Soos's SAT work](https://www.msoos.org/wordpress/wp-content/uploads/2010/08/PoS10-Soos.pdf), and choosing solvers from measured instance features in [SATzilla](https://doi.org/10.1613/jair.2490). The contribution here is the concrete engine implementation, checked reductions, learned/application records, and explicit identification of what each result establishes. No mathematical novelty or Millennium solution is claimed.