# Complete irreducible RAF enumeration through supported-trace SAT

Companion to paper 14, **The complexity of complete irreducible autocatalytic
families: output-polynomial enumeration of irreducible RAFs if and only if
P = NP**. This package provides a reusable solver-backed enumerator and the
paper's exact SAT-to-RAF source, whose entire irreducible family consists of
known conflict-pair cores plus satisfying-assignment cores.

Manuscript SHA-256:
`d3f3798ee1f02275a8ecbd97805982690d1d0f793ba8eb90a028fbc51d5d9004`.
The manuscript is unchanged. This original Python is not extracted from Lean,
does not reproduce the Turing-machine proof, and does not assume P = NP in
order to run: practical SAT calls may take a long time or return unknown.

## Run or import

Python 3.11 or newer:

```sh
python -m venv .venv
# Windows PowerShell: .venv\Scripts\Activate.ps1
# macOS/Linux: source .venv/bin/activate
python -m pip install -r requirements.txt
python example.py --output outputs
python -m unittest -v
```

Pinned `python-sat==1.9.dev5` supplies the Glucose3 backend; `matplotlib` draws
the explanatory figure. The package was checked on Windows with Python 3.11.
The scientific results use finite Boolean/set operations, not numerical ODEs.

Inputs at the top declare the variable universe, two CNFs, solver choice and
resource limits. A positive integer denotes a positive literal; a negative
integer denotes its negation; indices start at one. Defaults are (x1) AND (x2)
and (x1) AND (NOT x1), both on three declared variables. Unused variable x3
still contributes to the satisfying-assignment count.

`ReactionSystem`, `RAFOracle`, `SupportedTraceCNF`, `PySATBackend`,
`ModelEnumerator` and `SATFamilySource` can be imported separately. The solver
adapter is replaceable through `backend_factory`; a backend must support
`solve`, `add_clause`, and `close`, with solve returning `sat` plus a model,
`unsat`, or `unknown`. No shared framework with other paper packages is needed.

## Enumerate your own reaction system

Edit the emitted `outputs/model_input.json`, which contains `food`, a list of
reactions, and an optional `known_family`. Each reaction has a unique name and
sets of reactants, products and catalysts. Then run:

```sh
python example.py --input outputs/model_input.json --output custom_run
```

The custom path writes `custom_run/enumeration.json`. Starting from a partial
family is supported: initial members are deduplicated and independently
validated as irrRAFs. Distinct reaction names with identical incidence remain
separately selectable. Representing a reversible reaction as two selectable
directions is a modeling decision, not a harmless relabeling.

```python
from example import Reaction, ReactionSystem, ModelEnumerator
system = ReactionSystem({"food"}, (
    Reaction("a", {"food"}, {"x"}, {"y"}),
    Reaction("b", {"x"}, {"y"}, {"x"}),
))
result = ModelEnumerator(system).run()
print(result["status"], result["family"])
```

Ordinary RAF food closure ignores catalysts while generating molecules;
catalysts are required in the final closure. This permits a later-generated
catalyst and self-catalysis. It says nothing about concentrations, initiation
kinetics, mass balance, thermodynamics or sustained production.

## The exact supported-trace compiler

For d molecules and r reactions, `SupportedTraceCNF` uses selection variables
s_a, stage-row variables z_(i,x) for i=0,...,d, and firing variables f_(i,a)
for i<d. Its clauses require:

- a nonempty selected set inside the requested container;
- no non-food molecule in row zero;
- each claimed firing to be selected and have its reactants in that row;
- every claimed next-row molecule to have previous-row or producer support;
- each selected reaction to have all reactants and a catalyst in the last row;
- at least one omitted reaction from each already known irreducible set.

The support implications are deliberately one-way. Food variables need not
all be true, rows need not be monotone, and every enabled reaction need not
fire. The invariant is that each claimed row is a subset of actual staged
closure. A model can omit reachable molecules but cannot invent unsupported
ones. `check_model` checks the clauses, that invariant and the ordinary RAF
predicate independently. `witness` builds a canonical satisfying trace from a
valid RAF for testing or inspection.

The compiler preserves the paper's exact unsimplified variable, clause and
literal counts and checks its own accounting. Empty disjunctions stay empty
clauses. Thus a source with no reactions is UNSAT, and a reaction with no
reactants still needs a catalyst. `dimacs()` exports the formula to a standard
text format; the saved completion queries use `.txt` filenames for the site.

## Model-assisted enumeration and honest stopping

The enumerator solves one incremental chemistry formula with one blocking
clause per known irreducible set. On SAT it validates the selected RAF and
minimizes **inside that avoiding witness**, using ordinary maxRAF deletions.
Every subset of an avoiding witness still avoids the known family. Each new
irreducible output gets a clause blocking all its supersets, not merely one
SAT assignment or one support history.

On a completed run with K total cores and g initial cores, the solver-call
count is exactly K-g+1. The last call is UNSAT. Each successful round needs at
most r maxRAF calls for minimization; independent output-validation calls are
not included in that counter. These are invocation counts, not polynomial
runtime guarantees. The SAT solver is where hard cases can remain hard.

`complete` means that a final solver result was UNSAT. `incomplete` means the
formula-size, solver-call or conflict limit prevented that conclusion, or the
solver returned unknown. Returned members remain verified. Discovering what
happens to be the full family is insufficient if the completion call has not
run. A partial result can be supplied to a new run as its initial family.

Positive outputs are independently checked in Python. Completeness trusts
the pinned solver's UNSAT answer and the Python compiler; no independently
checked DRAT proof or Lean-certified execution is claimed. Call and conflict
limits are not a wall-clock timeout. Formula compilation is guarded by the
analytic literal count before clause allocation.

## Why the source describes the whole family

`BooleanFormula` defines the monotone accepted-choice condition: either both
truth values of a variable are selected (a conflict), or exactly/at least one
choice covers every variable and the selected choices hit every clause.
Its minimal accepted sets are the n conflict pairs and the satisfying full
assignments, provided n>=2. The code requires that hypothesis explicitly;
padding variables would change the model count.

`SATFamilySource` turns choices into food-consuming input reactions. Signal
rules produce coverage wires, clause wires and the output wire. Every signal
rule has its own auxiliary reaction and marker, and each auxiliary reaction
is catalysed only by the next marker in a cycle. A reset requires the output
wire and produces every wire plus the final marker. The cycle forces every
auxiliary into every RAF. The reset cannot create its own first prerequisite:
the output wire must be reached without it before the reset can fire.

Even clause rules for absent literals are retained with no produced signal
wire, because their marker-producing reactions are part of the literal
construction. Removing those reactions would alter the family and dimensions.

With n=3 and two clauses, the source has 36 molecules, 29 reactions and a
3235-bit incidence input under the paper's encoding. Both examples have three
known conflict-pair cores, each of size 25. The satisfiable formula has two
additional size-26 cores; the unsatisfiable formula has none. Hence:

| Source | Satisfying assignments | Total irrRAFs | Calls from three known cores | Count-first output bits |
|---|---:|---:|---:|---:|
| (x1) AND (x2) | 2 | 5 | 3 | 151 |
| (x1) AND (NOT x1) | 0 | 3 | 1 | 91 |

`output_bits` writes the unary count, delimiter and fixed-width reaction masks
used by the manuscript's contract. It does not emulate a Turing machine.
The saved bits encode the returned family; if edited limits stop a run early,
the accompanying status must be read before treating that family as complete.

The count identity is n + #SAT, not a parsimonious equality with #SAT. The
small source audit independently enumerates Boolean assignments, with an
explicit 4096-assignment limit. That truth-table audit is separate from the
general solver-backed enumerator and is not a scalable counting algorithm.

## What makes the lower bound stronger than “many outputs”

An unsatisfiable formula has a **known small complete family**: just the n
baseline cores. If a uniform output-polynomial enumeration algorithm with
polynomial p existed, p(N+B0) would be a polynomial deadline on those cases.
Failure to finish with exactly n outputs by that deadline would certify SAT.
The example displays the relevant dimensions and counts; it does not invent
a runtime polynomial for the practical solver or apply a timeout as a SAT
proof. The theorem's deadline is conditional on that hypothetical guarantee.

The deletion profile illustrates another limitation: deleting fewer than n
input reactions leaves some conflict pair intact, regardless of the formula.
At order n, deleting one choice per variable exposes whether the remaining
assignment satisfies it. On the satisfiable default source, 1/1, 6/6, 15/15
and 14/20 input-deletion sets of orders 0,1,2,3 leave a RAF. The 14 includes
deletions leaving conflict pairs; among the eight deletions leaving full
assignments, exactly two survive.

`essential_reactions` computes the intersection of all irreducible RAFs using
single-deletion maxRAF queries without enumeration, reporting `no RAF` rather
than a misleading vacuous intersection for an empty family. A separate test
shows that the union of all irreducibles need not equal the maximum RAF: the
family determines existence of survivors, not every surviving reaction.

## Outputs and validation

Outputs include `results.json`, the reusable input JSON, both completion
queries in DIMACS text, both count-prefixed mask strings, a PNG/SVG figure,
console output and metadata with inputs, versions and source/manuscript/output
hashes. Scientific JSON replays with the pinned solver; solver model/output
order can change with a different backend or version. SVG metadata may vary.

Seven test groups check the SAT correspondence for every selected set on tiny
sources; all containers and known-family subsets on a three-core source;
all 512 CNFs formed from the nine non-tautological two-variable clauses and
all 16 choice sets for each; the exact family/count correspondence and reset
obstruction; both worked examples from empty and seeded families; limits,
unknown responses and malformed models; low-order deletions and essentiality;
distinct duplicate-chemistry identifiers; and DIMACS/JSON roundtrips.

These finite tests validate this implementation. They neither settle P versus
NP nor reproduce the paper's verified machine construction or timing pilot.

## License

MIT is proposed for this original example code, pending the owner's license
choice. No license grant is asserted here. This does not change the license of
the manuscript or any third-party dependency.