# Preprocessing
What each mode does to the formula, and what a consumer does with the record to
get a correct answer over the original. [`bundle.md`](bundle.md) is the
field-by-field reference for the files described here.
## The lift identity
```text
count(original) == count(reduced) * 2^count_lift_pow2 * weight_lift
```
`count` is the mode's own count — plain, weighted, projected or
projected-weighted. The two factors are disjoint, so apply both unconditionally
and never branch on the mode.
| `mc`, `pmc` | the whole lift | always `"1/1"` |
| `wmc`, `pwmc` | always `0` | the whole lift |
| `compile` | the unused variables, nothing else | always `"1/1"` |
Count `reduced.cnf` under `reduced_weights`, and under
`show_vars_reduced_dimacs` if the mode is projected; multiply by both factors.
`weight_lift` is an exact rational `"numerator/denominator"`. Exact rational
arithmetic is needed throughout: a float rounds a `1/3` that no later step
recovers.
The mode comes from the file's declarations unless `--mode` overrides them, and
every run reports the mode it used.
## The steps
There is no single pipeline with per-mode switches. The mode picks one of three
chains, and the chains differ in which steps run and in what order.
### `mc` and `wmc`
In order. Steps 1–7 are one unit — `--no-simplify` turns off all seven.
1. **Clause simplification** — subsumption, vivification and self-subsumption in
CaDiCaL. Rewrites clauses; removes no variable.
2. **Equivalence detection** — strongly connected components over the binary
clauses. Rewrites onto a class representative but keeps every variable, so
this step alone changes no ids.
3. **Backbone and equivalence probing** — one SAT session that finds forced
literals, propagates them, re-runs step 2 over the clauses that propagation
created, then probes for whatever equivalences remain. Time-budgeted.
4. **Backbone and dead-variable stripping** — drops the forced variables and any
variable no clause mentions. **First renumbering.**
5. **Equivalence reduction** — drops the partners step 2 found, keeping one
representative per class. **Renumbers.** Under `wmc` a dropped partner's
weight is folded into its representative's, which is why `reduced_weights`
comes out of preprocessing rather than out of the input.
6. **Gate detection** — finds AND/OR/XOR/ITE outputs. Removes nothing itself; it
tells step 7 which variables are already known to be defined.
7. **Definability elimination (DVE)** — eliminates defined, free and
newly-equivalent variables by resolution, looped under a round and time
budget. The time budget bounds the vivification each round ends with as well
as the rounds themselves, so a formula whose vivification runs long gets a
weaker reduction rather than a longer pass. **Renumbers.**
8. **Arjun** — independent-support minimization with resolution-based
elimination, backbone and equivalence detection, and optional SBVA.
**Renumbers.** Turned off by `--no-arjun`.
An embedded caller configures steps 1–7 through the public
`RunConfig::simplify: SimplifyPolicy`. Its production default gives the shared
clause/backbone prefix 300 seconds, equivalence probing 300 milliseconds, runs
gate detection, and gives DVE 30 rounds within 3 seconds. The two prefix budgets
are optional; `detect_gates` switches step 6 independently; and `dve=None`
switches step 7 off. An armed `DvePolicy` requires both positive rounds and a
positive millisecond budget. This policy feeds the one path above—it does not
select a second preprocessor.
### `pmc` and `pwmc`
A different chain, not the one above with steps disabled. Every stage is exactly
×1 for the projected count, and only Arjun renumbers — the rest preserve
variable ids by design, so there is just one map to compose.
1. **Arjun projection-set minimization** — shrinks the show set and removes
non-show variables that are free or determined. Runs *first* here, unlike the
count chain. Turned off by `--no-arjun`.
2. **Count-preserving unit propagation** — propagates to fixpoint, then re-pins
each forced show variable as a unit clause so it still contributes ×1 rather
than ×2.
3. **Show-frozen DVE** — the same elimination as the count chain's step 7, but
frozen on the show set: only hidden variables go, and a show variable can be
merged away only into another show variable.
4. **Projected BVE** — resolves away projected-out variables, bounded so the
clause count cannot grow.
Under the default `ProjectionPolicy::Full`, steps 2–4 always run;
`--no-arjun` is the only command-line toggle this chain has.
An embedded caller can instead set `RunConfig::projection_policy` to
`ProjectionPolicy::ArjunOnly(...)`. That exports the post-Arjun formula, show
set, weights, lift and variable map without running steps 2–4. The nested
`ProjectionNoGain` policy either keeps the usual rejection of an Arjun result
that did not shrink the projection (`Reject`) or exports that sound result
anyway (`KeepSound`). The injective-map and every other correctness check still
apply. `ArjunOnly` is refused outside `pmc`/`pwmc` and when Arjun is disabled;
the default `ProjectionPolicy::Full` preserves the complete chain above and may
still run steps 2–4 with Arjun disabled.
### `compile`
Steps 1–5 of the count chain, and nothing after them.
Gate detection, DVE, Arjun, BVE and SBVA are all excluded on purpose: each
removes a variable determined by a *function* of the survivors, and a map entry
names a literal, not a function. So `compile` removes only backbone literals,
equivalence partners and unused variables — every other variable survives, which
is what makes `original_to_reduced_dimacs` total and an assignment liftable with
no propagation.
`reduced_weights` and `show_vars_reduced_dimacs` are carried through unchanged
here, not folded: under `compile` alone they are the input's, renumbered.
`compile` still accepts custom shared-prefix and equivalence budgets, but its
soundness contract always caps gate detection and DVE off. A non-default change
to either count-only field is rejected rather than silently ignored. Projected
modes do not run this simplify path at all, so they likewise reject a
non-default `SimplifyPolicy`.
### Steps that can be discarded
A step can run and then be discarded wholesale, so its presence in the list does
not mean it shaped the output:
- **DVE under `mc`/`wmc`** is thrown away unless it eliminated enough to be
worth the renumbering.
- **DVE under `wmc`** is additionally reverted if it eliminated a variable whose
two polarities carry different weights in a way no rational factor corrects.
- **Show-frozen DVE** reverts to the pre-DVE formula if a show-variable
equivalence chain fails to resolve to a surviving show variable.
- **Arjun**, in all four counting modes, is kept only if its verdict says it
helped and its variable map is injective.
For an embedded caller, `RunConfig::arjun_clause_growth` can change the plain
clause-count verdict from its default `ArjunClauseGrowth::Reject` to
`KeepSound`. That keeps an otherwise sound clause-growing result; the
injective-map and every other correctness check still apply. An embedding that
hands Arjun one formula but will compile a different count-preserving formula
can instead use `ArjunClauseGrowth::RejectAgainst(formula.clauses.len())`; the
candidate then has to be no larger than that caller-provided baseline. Both
non-default policies are refused outside `mc`/`wmc` or when the Arjun stage is
not enabled.
Each of these is reported when it fires: a `c note:` line on stderr names the
step and why it went. The bundle itself describes only the preprocessing that
survived.
A Rust caller reads that off `PreprocessBundle::stages` instead, which also
separates a step that ran out of budget — worth calling again with more — from
one whose result was refused.
`PreprocessBundle::telemetry` reports the work the call attempted, including a
reduction that a keep gate later discarded. Its optional phase durations use
`None` for “not attempted” and `Some(0)` for an attempted phase shorter than a
millisecond. Arjun's duration includes SBVA because both run inside one opaque
native call; `StageReport::sbva` is the participation record. Backbone literals
found and probes completed accompany the backbone duration.
When the exported `mc` formula is a kept Arjun result, the caller also receives
`PreprocessBundle::independent_support_reduced`. It is 0-based in the exported
formula's numbering and may be `Some(empty)`; it is `None` for every other mode
or Arjun outcome. It is deliberately in-process only, because SBVA may put
introduced reduced variables in the support that have no original name.
### Deadlines
A budgeted step stops starting new work at its deadline and hands back the
soundest checkpoint it has reached; a result that lands past the grace after it
is discarded unless `VITRI_ARJUN_KEEP_OVERRUN` asks for it, except under the
projected modes, which keep their checkpoint however late because Arjun is their
first step. Discarding is measured, not assumed: over a set of counting
instances under a two-minute per-instance wall, discarding late reductions
solved four instances more than keeping them did.
A library caller normally leaves `RunConfig::arjun_budget` at
`ArjunBudget::Derived`, which scales Arjun's share from the run budget. A caller
that has already divided its own wall can use `ArjunBudget::Exact(duration)`;
that duration bypasses the derived ratio, floor and cap, but an earlier absolute
run deadline still clamps it. An exact budget is refused when the Arjun stage is
off or the resolved mode has no Arjun stage.
### Disabling preprocessing
Under `mc` and `wmc`, `--no-simplify` and `--no-arjun` together give a bundle
with no preprocessing at all. `compile` has no Arjun stage, so `--no-simplify`
alone does it there, and `--no-arjun` is refused rather than ignored. A
projected mode has no such recipe: it has no simplify chain, so it refuses
`--no-simplify` in the same way, and `--no-arjun` drops only its first step
because steps 2–4 always run.
Neither flag changes the answer; both change only how much work runs first.
A non-default `RunConfig::simplify` with the simplify stage switched off is an
error: accepting it would make an embedding believe its budgets or stage policy
were being used. Leave the policy at `SimplifyPolicy::default()` when using the
stage switch.
## Operations on derived formulas
`bundle::preprocess` remains the one raw-input pipeline. An embedding compiler
can subsequently create a component, cofactor or conditioned residual that
needs one local operation without rerunning that pipeline:
- `cnf::propagate_units` returns the residual and every assignment propagated
out of it. The pair preserves the function; the residual alone does not.
- `projection::eliminate_hidden` applies the projected chain's bounded
resolution step to a supplied show set. It preserves ids and adopts no
clause-growing elimination.
- `projection::classify_hidden_defined_by_show` proves which selected hidden
variables are functions of the show set. Only a completed SAT refutation
enters `defined`; a counterexample or exhausted budget cannot. Appearing
targets are probed by descending literal incidence, then descending variable
id, matching the compiler-facing classifier's deterministic cutoff order.
An absent target is free only after the formula is proved satisfiable; an
unsatisfiable formula vacuously defines every requested target, while an
unfinished base check leaves absent targets unknown. The whole-sweep wall is
a soft setup budget: the linear scan and dual-CNF construction already in
progress cannot be interrupted, but the budget is checked before and after
setup and no SAT query starts once it has expired. Formulas too large for the
guarded dual construction leave every unstarted appearing target unknown.
These are the same implementations the preprocessing chains use. They expose
no second pipeline and carry no vtree or compiler policy.
## The show set and the weights
Counting `reduced.cnf` over the original show ids, or under the input's own
weights, is a silently wrong count: `show_vars_reduced_dimacs` and
`reduced_weights` both come out of preprocessing, not out of the input.
An empty show set is a real answer: `c p show 0` means every show variable was
retired, so the projected count is 1 if `reduced.cnf` is satisfiable and 0 if
not. It does not mean "unprojected".
## Lifting an assignment
1. Read each reduced variable through `reduced_to_original_dimacs`, which is
signed — a variable can come back negated.
2. Set every literal in `forced_literals_original_dimacs` to its polarity.
3. Choose freely for every variable in `free_vars_original_dimacs` — that is
where the `2^k` models come from.
The result is partial: a variable the equivalence reduction or DVE removed is
determined by the others and appears in neither map, and unit propagation over
the original formula recovers it. Under `compile` nothing is partial — lift
through `original_to_reduced_dimacs` instead. Under a projected mode the
reduced formula's models are not models of the input at all; what lifts back
is a show-projection, where a feasible assignment of the retained show
variables names one of their originals.
## Refutation
If preprocessing proves the instance unsatisfiable, `unsat` is `true` and the
count is 0. `reduced.cnf` then holds an explicit contradiction (`x` and `¬x`)
rather than the empty clause, which DIMACS cannot portably spell.