pub fn emit_sr(
num_vars: usize,
original: &[Vec<Lit>],
steps: &[ProofStep],
) -> Result<String, EmitError>Expand description
Emit our refutation in Marijn Heule’s .sr (substitution-redundancy) proof format — the input
sr2drat expands into plain DRAT for drat-trim to verify. This is the pipeline that makes our
marquee symmetry proofs externally machine-checkable, closing the “SR witnesses not yet exportable”
gap: a Pr step carrying a Witness::Substitution no longer dead-ends at
EmitError::RequiresSubstitutionRedundancy but is written as a substitution line sr2drat knows.
Per the sr2drat grammar (sr2drat.c) a lemma line is the clause, then — each delimited by a repeat
of the pivot (the clause’s first literal) — the PR witness ω, then optionally the permutation
σ as var image pairs. RUP additions carry no witness (a bare C 0 line sr2drat forwards to
DRAT). Each step is re-verified (pr::is_pr / RUP) before it is written, so a returned proof is
sound by our checker; the trailing empty clause closes it.
The decisive subtlety, matching the reference .sr shape: sr2drat expects the lemma’s pivot
variable to be held by the assignment ω, with σ permuting only the other variables. For a unit
lemma [p] witnessed by a transposition that moves p, we therefore decompose the witness —
ω = {p, ¬σ(p)} pins both swapped copies in that coordinate and σ′ (σ with p’s and σ(p)’s
variables fixed) carries the rest. This keeps the pivot out of the permutation entirely, which is
what makes the expansion check: verified end-to-end through sr2drat→drat-trim for PHP(n) up to
n=18 (a 591k-line DRAT proof), the marquee symmetry refutations Kissat and CaDiCaL time out on.