# RRLS: lift, learn, loop, and decode Research extension to the RRLS P versus NP proof audit. 5 September 2026. This release implements an exact complementary-coordinate lift, a conflict-driven SAT solver, independently checked learned clauses, resumable proof prefixes, and proof slicing. It does not establish P = NP or P ≠ NP. The mathematical arguments below establish the stated transformations and certificate rules. They are not a formal verification of the Python implementation. The implementation applies established conflict-driven clause learning (CDCL), first-UIP conflict analysis, and reverse unit propagation (RUP). These are not discoveries of this project. [Heule's CDCL presentation](https://www.cs.cmu.edu/~mheule/15816-f22/slides/CDCL.pdf), [Wetzler, Heule, and Hunt, DRAT-trim](https://www.cs.cmu.edu/~mheule/publications/drat-trim.pdf). ## 1. The precise target For an explicitly encoded CNF formula F, find an assignment satisfying every clause, or establish that no such assignment exists. A finite execution solves its particular input. Proving P = NP would additionally require a uniform deterministic algorithm with polynomial total bit cost for every input length, including compilation, learned representations, search, arithmetic, and decoding. [Cook's official problem statement](https://www.claymath.org/wp-content/uploads/2022/06/pvsnp.pdf). The sixteen captured cores used here were already decided by the previous engine using branching. Their truth values were not new unknowns. The target of this extension is reusable reasoning and independently checkable evidence on those cores, followed by fixed fresh cases. ## 2. An exact lift with a decoder For each occurring variable x_i, introduce two coordinates a_i and b_i and require \[ a_i\lor b_i,\qquad \neg a_i\lor\neg b_i. \] For Boolean values these constraints are equivalent to b_i = 1-a_i. Replace positive x_i in every original clause by a_i, and negative x_i by b_i. Call the resulting CNF E(F). All original clause bodies now use positive coordinates; the complementary-pair constraints preserve the original consistency problem. Define \[ \ell(x)=(x_1,1-x_1,\ldots,x_n,1-x_n), \qquad d(a,b)=(a_1,\ldots,a_n). \] **Theorem 1.** The maps restrict to inverse bijections between the satisfying assignments of F on its occurring variables and those of E(F): \[ F(x)=1\iff E(F)(\ell(x))=1, \qquad d\circ\ell=\operatorname{id}, \qquad \ell\circ d=\operatorname{id}\text{ on models of }E(F). \] **Proof.** Each complementary pair has exactly the two assignments (0,1) and (1,0). Every lifted literal therefore has the same value as its corresponding original literal. Each clause, and hence the conjunction, has the same value under the lift. Conversely, every lifted model determines exactly one original assignment by selecting its a-coordinates. The pair constraints force all b-coordinates to be their complements. This proves both implications and the inverse identities. ∎ For n occurring variables and m original clauses this adds n variables, 2n clauses, and 4n literal occurrences. The implementation first names the actually occurring variables densely, so an identifier such as 2^200 does not allocate an array with 2^200 entries. Identifier processing still costs its actual bit length. Variables declared but absent from every clause can be assigned arbitrarily and need not be enumerated. For exact 3-CNF the relation vocabulary is OR3 plus NEQ2, as in the previous paper. A bijective lift does not make shared constraints independent. It preserves every solution and every obstruction to a solution; it need not improve runtime. `verify_complement_lift` independently reconstructs the entire expected lifted formula, checks the solver's evidence against that formula, and directly evaluates any decoded SAT model on the original input. For UNSAT, the exact lift equivalence transfers the checked compiled refutation to the original formula. ## 3. Turn an error into an entailed constraint Let F_i be the input plus previously accepted lemmas. A candidate learned clause C_i is accepted only if assigning all of its literals false makes unit propagation derive a contradiction: \[ \operatorname{UP}(F_i\land\neg C_i)=\bot. \] Here the negation of a disjunction is a conjunction of unit assumptions. An unknown value is never silently interpreted as false. **Theorem 2: sound learning.** The RUP condition implies F_i entails C_i, and therefore \[ \operatorname{Models}(F_i\land C_i)=\operatorname{Models}(F_i). \] **Proof.** A unit propagation step assigns the sole remaining literal of a clause true. Every satisfying extension of the current partial assignment must make that assignment. By induction, a satisfying extension must obey all propagated units. A completely false clause is incompatible with such an extension. Thus there is no model of F_i that falsifies all literals of C_i, which is precisely entailment. Adding an entailed clause removes no model. ∎ Induction over the proof sequence gives F entails every accepted lemma. The sequence therefore preserves the original solution set, even though it changes the ease with which consequences are found. A small exact example is \[ F=(\neg a\lor b)\land(\neg a\lor\neg b)\land(a\lor c). \] Trying a=1 forces both b=1 and b=0. Resolution gives the learned unit \[ \frac{\neg a\lor b\qquad\neg a\lor\neg b}{\neg a}. \] The engine can keep a=0 permanently; the third clause then forces c=1. The failed trial has become a consequence of the formula. Calling it a new coordinate does not change what must be proved: that the consequence is entailed. ## 4. The executable loop `conflict_loop.py` uses dense variable names, two watched literals per non-unit clause, explicit implication reasons, decision levels, phase saving, and deterministic integer activity scores. 1. Propagate unit clauses until a fixed point or conflict. 2. At a conflict, resolve implication reasons backward until the conflict clause has exactly one literal at the current decision level: the first unique implication point, or first UIP. 3. Backtrack to the largest decision level of the other learned literals. The learned clause is now unit, so assert its remaining literal. 4. Retain the learned clause and repeat. If propagation is complete but variables remain unassigned, make and count another decision. 5. Return SAT with a complete model on occurring variables, or UNSAT with a RUP sequence ending in the empty clause. A resource cap returns UNRESOLVED with only its checked proof prefix. Every resolution step is sound: from A∨v and B∨¬v, any model must satisfy A∨B. Implication reasons are clauses already in the database. The final independent checker does not use the solver's watched-literal code, conflict analysis, activity scores, or claimed status to infer truth. The independent checker is a separate, scan-based implementation in `verify_conflict_loop.py`. It checks every learned clause in order, including clauses in SAT and unfinished runs. SAT also requires direct evaluation on the original input. UNSAT requires a checked final empty clause. The checker has its own resource limits and may refuse to finish a check; this is not acceptance. **Theorem 3: accepted decisions.** If the specified checker rules accept SAT, the formula has the supplied satisfying assignment. If they accept UNSAT, the formula has no satisfying assignment. **Proof.** The SAT condition is the definition of a model. For UNSAT, Theorem 2 inductively implies the final empty clause from F. An empty disjunction is false under every assignment. Hence F has no model. ∎ These proofs establish the abstract rules. Source review, finite tests, and independent execution provide evidence about their implementation; none is a proof-assistant verification of the program or runtime. ## 5. Checked memory and restarting `resume_until_decided` runs a bounded number of conflicts, saves the learned prefix, and starts a fresh search with that prefix. Before loading it, the checker verifies its exact input fingerprint and rechecks every lemma against that input in sequence. There is no external `trusted` flag, and a lemma from an unrelated problem is not imported merely because it worked elsewhere. By Theorem 2, this restart preserves the solution set. Restarting can change search order and total work. It is not automatically faster: input processing, rediscovered propagation, and rechecking the accumulated prefix are counted again. A round that learns nothing before exhausting its work budget triggers a stop instead of an unproductive endless loop. A completed refutation can yield zero new search decisions when reloaded. That is proof reuse, not a new polynomial-time solution of the original problem: the initial search and subsequent proof checks remain real costs. ## 6. Compress a proof without changing its meaning During RUP replay the checker records the reason clauses used to reach a conflict. Start from the final empty clause, retain the earlier learned clauses needed by those dependencies, and remove the unused learned clauses. Preserve their order and recheck the resulting proof from the original input. The second check is decisive. A sliced proof is accepted only if every retained lemma still has RUP in its reduced context and the final empty clause remains valid. Dependency extraction and both checks cost time. Report the cost of producing the slice separately from the cost of checking it again later. This implementation removes unused lemmas. It does not guarantee a shortest proof, and it does not modify the original solver source or optimize an arbitrary program over itself. ## 7. What looping does and does not bound With n Boolean variables there are 3^n distinct non-tautological clauses when each variable is absent, positive, or negative. That finite count is exponential, not polynomial. Retaining new clauses can ensure finite progress in an unbounded ideal learning procedure without supplying the bound required by P = NP. Let K be the number of learned clauses and S their total literal count. A naive RUP check of one clause takes at most n+1 scans that assign a new variable or terminate. Ignoring identifier bit costs, total replay work has the coarse bound \[ O\bigl(K(n+1)(L+S+K)\bigr), \] where L includes the input clauses and their literals. Including K counts visits to empty clauses. Thus checking is polynomial in the input **and the supplied proof**, not necessarily in the input alone. K and S can be large. Searching for that proof is a separate cost. The runtime ledger records decisions, conflicts, propagation queue pops, watched-clause visits, replacement literal tests, resolution steps, selected analysis operations, variable-score visits, and unassignments. It also records stored and proof literals, proof-check work, and elapsed time. These counters describe selected operations; they are not an exhaustive Turing-machine bit-operation count. Sorting, hashing, allocation, parsing, and Python overhead are reflected in elapsed time but not all expanded in the work proxy. ## 8. A known limitation of the present proof language The following concerns the new native clause-learning/RUP route on unchanged input formulas. It is not a lower bound against every RRLS primitive or every possible compiler. For n+1 pigeons and n holes, let P_n contain the clauses \[ \bigvee_{j=1}^{n}p_{i,j}\quad(1\le i\le n+1), \] and \[ \neg p_{i,j}\lor\neg p_{k,j}\quad(i