Skip to content

Resolution Proof Compression by Splitting

A post-processing algorithm that splits a resolution refutation on a chosen variable into complementary branch proofs, recombines them by resolution, and retains the result when it reduces proof size.

Version
v1 · 2026-09-28 · History
Domain-specific #
11773
Domain group
Applied Sciences & Engineering
Origin domain
Computer Science & Software Engineering
Subdomains
Automated Reasoning, Proof Compression → Computer Science & Software Engineering
Aliases
Splitting resolution proofs, Resolution proof splitting, Proof compression by splitting

Core Idea

Resolution proof compression by splitting transforms a completed resolution refutation rather than changing the search that found it. Given a proof DAG ending in the empty clause and a selected variable x, the algorithm constructs one transformed branch that derives x and another that derives not-x. Resolving those two branch conclusions recovers the empty clause, preserving the refutation while reorganizing shared and duplicated subproofs.

Compression is an objective, not a soundness guarantee of size reduction. A split can make the proof larger. The procedure can therefore try variables sequentially, compare each transformed proof with those already retained, and roll back to the smallest known proof after an unfavorable step. Cotton's additivity score is a heuristic for variable choice: it emphasizes pivots associated with clause-size growth, but it does not replace measuring the resulting DAG.

Structural Signature

Sig role-phrases:

  • Resolution refutation DAG — Supplies input clauses, derived clauses, pivots, and an empty-clause sink. It is required input. Counterfactual: A satisfiability result without a resolution proof cannot be transformed by this algorithm.
  • Split variable — Defines the complementary literal branches used to transform the proof. It is required choice. Counterfactual: Without a selected variable there are no x and not-x branch proofs.
  • Literal-indexed proof maps — Rewrite proof nodes while propagating one branch assumption and bypassing or rebuilding resolution steps. It is defining transformation. Counterfactual: Merely partitioning clauses does not construct valid branch proofs.
  • Complementary branch proofs — Derive the two literals needed for final recombination. It is required intermediates. Counterfactual: One branch alone does not preserve the original refutation.
  • Final resolution step — Recombines x and not-x to recover the empty clause. It is required soundness link. Counterfactual: Omitting recombination yields two conditional arguments rather than a refutation.
  • Size objective and rollback — Compare transformed proofs and retain a prior smaller proof when expansion occurs. It is required optimization control. Counterfactual: Sound transformation alone does not ensure compression.

What It Is Not

  • The method is not case splitting performed by a SAT solver before or during proof discovery.
  • It is not arbitrary deletion of resolution nodes; both transformed branches and their final recombination must remain valid.
  • It does not guarantee that every selected variable produces a smaller proof.
  • The additivity score is a search heuristic, not a proof that its highest-scoring variable gives the global optimum.
  • Closest near-miss. Search-time case splitting changes how a solver discovers a proof; this method post-processes an existing resolution proof and must preserve its refutation.

Scope of Application

  • Proof logging pipelines. A solver's resolution refutation is compressed after generation before storage, checking, or interpolation.
  • Certified unsatisfiability. The transformed DAG preserves an empty-clause derivation that can be independently checked.
  • Heuristic minimization. Several pivots can be attempted under time and memory limits with rollback to the best proof.
  • Proof-complexity experiments. Researchers compare node, edge, or serialized size while keeping the metric explicit.

Clarity

A description should state the input proof representation, pivot variable, branch-map rules, handling of shared DAG nodes, recombination step, and size metric. 'Split the proof' is insufficient if it does not explain how each original inference becomes a valid inference or bypass in each branch. Compression by node count can differ from compression by literal count or file size, so the objective must be fixed before comparison.

Manages Complexity

The transformation can expose a repeated variable-dependent structure and replace it with two cleaner conditional derivations plus one recombination. That can shrink a tangled DAG, but branch duplication can also destroy sharing. The best-so-far rollback makes the iterative procedure monotone in retained proof size even though individual transformations are not.

Abstract Reasoning

  1. Validate the input as a resolution DAG with an empty-clause sink.
  2. Choose a candidate variable, optionally using the proof's pivot additivity profile.
  3. Construct both literal-indexed proof maps while preserving valid inputs and resolution steps.
  4. Evaluate the maps at the empty-clause node to obtain complementary branch conclusions.
  5. Resolve the branch roots and check the resulting refutation independently.
  6. Measure the chosen size objective, keep the smaller proof, and stop when resource limits outweigh expected gain.

Knowledge Transfer

The algorithm transfers among resolution proofs that expose pivots and DAG structure compatible with its maps. A proof system with different inference rules needs a new soundness argument; a generic divide-and-conquer optimization is not this method. The broader lesson—condition on a variable, simplify branches, recombine, and retain only improvement—can inspire other transformations without inheriting the name.

Examples

Canonical

A proof DAG is split on x, transformed to derive x and not-x from the original inputs, and the two roots resolve to the empty clause with fewer total nodes than the initial refutation.

Mapped back: branches → proofs of x and not-x; input → resolution refutation; objective → fewer nodes; pivot → x; recombine → resolution.

Applied / In Practice

If the transformed DAG is larger, the implementation discards it in favor of the smallest previously retained proof before trying another variable.

Mapped back: action → rollback; candidate → larger split proof; next → another variable; test → proof-size comparison.

Structural Tensions

T1 — Local Pivot Score versus Global Dag Sharing. An additive pivot heuristic targets clause growth, while actual compression depends on shared subproof structure after rewriting.

Diagnostic: Does the score predict net nodes after both branches and recombination?

T2 — Aggressive Transformation versus Bounded Resource Use. Trying many variables may find better compression but can build large intermediate proofs.

Diagnostic: What rollback, time, and memory limits protect the post-processing budget?

Structural–Framed Character

Resolution Proof Compression by Splitting is strongly structural. Clauses, literals, pivots, DAG maps, resolution soundness, and size metrics are formal. Variable selection and resource budgets are heuristic choices layered on that proof-preserving core.

Structural Core vs. Domain Accent

The skeleton is branch transformation plus sound recombination under an optimization objective. Automated reasoning supplies resolution clauses, complementary literals, proof DAGs, empty-clause refutations, and checkability. Removing those yields generic conditional compression.

This entry is a kind of Compression.

  • Approved root. No reviewed parent currently entails this resolution-specific split, recombine, compare, and rollback algorithm.

  • Related — resolution, proof compression, and case analysis. They supply the formal setting but do not duplicate the method.

Relationships to Other Abstractions

Local relationship map for Resolution Proof Compression by SplittingParents appear above the current abstraction, mutual partners to the right, and children below. Node labels state whether each abstraction is prime or domain-specific; colors identify relation types.Resolution Proof Com…DOMAINPrime abstraction: Compression — is a kind ofCompressionPRIME

Current abstraction Resolution Proof Compression by Splitting Domain-specific

Parents (1) — more general patterns this builds on

  • Resolution Proof Compression by Splitting is a kind of Compression Prime

    Resolution-Proof Compression by Splitting is Compression that rewrites a refutation into complementary variable branches and retains the recombination only when proof size falls.

Hierarchy paths (3) — routes to 3 parentless roots

Neighborhood in Abstraction Space

Resolution Proof Compression by Splitting sits in a sparse region of the domain-specific corpus (63rd percentile for distinctiveness): few abstractions share its structure, so a faithful description tends to retrieve it precisely.

Family — Logical Connectives & Formal Systems (13 abstractions)

Nearest neighbors

Computed from structural-signature embeddings · 2026-10-08

Not to Be Confused With

  • SAT branching. Tell: Guides search for a proof or model, whereas this method begins with an existing refutation.
  • Proof trimming. Tell: Usually removes unused nodes reachable from the conclusion without constructing complementary split proofs.
  • Clause subsumption. Tell: Simplifies clauses or clause sets and is not the literal-indexed proof-DAG transformation.
  • Craig interpolation. Tell: Can consume resolution proofs but pursues an interpolant rather than smaller proof size.

References

  • Frozen Wikipedia discovery revision: https://en.wikipedia.org/wiki/Resolution_proof_compression_by_splitting (revision 1289429868).

The frozen Wikipedia revision is discovery provenance. The retained source set was reviewed for identity, formal or operational relation, and scope. The encyclopedia's structural synthesis is bounded to those claims; a thin authority surface is recorded as a nonblocking source-strengthening repair rather than concealed.