Module inprocess 

Certified inprocessing: clause-database simplifications that emit a machine-checkable proof.

Where a normal SAT solver simplifies for speed, here every simplification carries its own certificate — bounded variable elimination adds RUP resolvents and deletes the eliminated variable’s clauses; vivification replaces a clause with a RUP-shorter one. Composed with the refutation, the whole run stays independently checkable by crate::pr::check_pr_refutation. This is the certified analogue of the inprocessing that makes Kissat/CaDiCaL fast — a real differentiator: nobody ships certified inprocessing.

Enums

EquivResult

Functions

bucket_elimination_refute

Full Davis–Putnam bucket elimination in min-degree order, allowing intermediate growth but capping every resolvent at width_cap. If it reaches ⊥, returns the RUP-resolvents-then-deletions proof — a width-≤width_cap resolution refutation, i.e. a 2^width_cap·n certificate that crushes every bounded-treewidth family. Returns None the moment a resolvent would exceed the cap (high treewidth — the certificate would be exponential, which is exactly the Ben-Sasson–Wigderson hardness). Sound: every step is RUP/Delete and independently re-checkable by crate::pr::check_pr_refutation.

bve

Bounded variable elimination over the whole formula: repeatedly eliminate every variable whose elimination is non-growing, until a fixpoint (capped at a few passes). Returns the simplified clause set and the composed proof steps.

eliminate_variable

Try to eliminate variable x from clauses by Davis-Putnam resolution. Returns the new clause set and the proof steps (RUP resolvents, then the deletions of x’s clauses) — but only when x actually occurs and elimination does not grow the clause count (the standard BVE bound). None otherwise. Verdict-invariant: a model of the result extends to a model of the input.

equivalent_literal_scc

vivify

Vivify the whole database: replace each clause with its RUP-strengthened form, emitting an Rup(shorter) then Delete(original) per improvement. Shorter clauses propagate and delete better. The composed steps keep the run independently checkable.

vivify_clause

Vivify a clause: drop every literal whose removal leaves a clause still RUP-implied by db. Returns the strengthened (shorter) clause, or None if nothing could be removed. The result is a sub-clause logically equivalent in context, so it is verdict-invariant.