PaperlayerView exact revision on arXiv

Source-linked AI summary

Subsumption-Free Private-Pivot Learning in Resolvable Network-Based SAT Solving

Gábor Kusper

arXiv:2609.34880v1cs.LO

TL;DR

RN-Solver’s global subsumption checks can dominate runtime on random 3-SAT instances, motivating a structural alternative. The paper uses C-falsified mixed reaches and a frozen snapshot to guarantee non-subsumption without those old-white checks. Within an 8-second budget, snapshot/full-DNF solved 963 of 1,000 uf20-91 instances, compared with 724 for the original control flow.

  • Problem

    In RN-Solver, testing every learned white reach for novelty and non-subsumption can dominate runtime on random 3-SAT instances.

    Source: §1 · p. 2

  • Method

    The revised solver learns from C-falsified mixed reaches in a frozen snapshot, using the private-pivot invariant to replace old-white subsumption checks with a structural guarantee.

    Source: §1 · p. 2, §3 · p. 6, §8 · p. 14

  • Results

    Within 8 seconds, snapshot/full-DNF solved 963 of 1,000 uf20-91 instances, compared with 724 for the original control flow.

    Source: §8 · p. 14

  • Takeaways & Limitations

    For these private-pivot candidates, the triggering token distribution certifies that no old white reach subsumes the learned reach, removing the corresponding runtime test.

    Source: §8 · p. 14

    The guarantee depends on the mixed reach being C-falsified; without the condition that its tail is disjoint from C, a generated white reach can be subsumed by an old one.

    Source: §4 · p. 7

Abstract

from arXiv · show

A resolvable network is a directed-graph representation of SAT: every SAT instance can be translated into an RN, and every RN has an associated CNF formula. Each reach represents one clause. In a mixed reach, the head and tail are disjoint sets of variables containing the variables occurring negatively and positively in the clause, respectively; the distinguished symbols Source and Sink represent a missing negative- or positive-literal side. RN-Solver is a proof-of-concept SAT solver based on this representation. Its all-positive clauses are represented by white reaches, and its token distributions are the inclusion-minimal hitting sets of the current white tails, generated by monotone CNF-DNF dualization. RN-Solver learns new white reaches by private-pivot resolution, a structured resolution sequence that uses old white reaches as pivot witnesses. In the original algorithm, every candidate white reach generated by such a chain was followed by a global subsumption test against the current network. Profiling showed that this subsumption test can dominate the runtime on random 3-SAT instances. We show that this check is unnecessary when the mixed reach used for learning is falsified by the current token distribution, meaning that the distribution makes all variables in the head true and all variables in the tail false. The key invariant is simple: the resulting white tail is disjoint from the triggering token distribution, while the same distribution intersects every old white tail. Hence no old white reach can subsume the generated reach. This structural observation allows us to construct a simpler, snapshot-based, subsumption-free variant of RN-Solver, where each main-loop iteration uses a fixed set of old reaches and installs newly generated white reaches only at the end of the iteration. We prove soundness of the revised algorithm. Empirical evaluation confirms the elimination of the targeted checks: within an 8 second budget, snapshot/full-DNF solves 963 of 1,000 uf20-91 instances, compared with 724 for the original control flow. A separate 100-instance comparison identifies exact incremental DNF as the most effective of the three tested configurations.

1 Introduction

RN-Solver combines a clause-level graph representation of SAT with monotone dualization and private-pivot resolution. The paper’s central result is that falsified mixed reaches yield learned white reaches that need no old-white subsumption check.

1 Introduction

  • RN-Solver represents clauses as reaches and uses minimal hitting sets of white tails as token distributions before learning through private-pivot resolution.A token distribution falsifies a mixed reach when it makes the head true and the tail false.Source: §1 · pp. 1–2
  • RN-Solver is presented as a conceptual and algorithmic study of structural reasoning, not as a currently competitive replacement for mature CDCL solvers.The approach combines graph representation, dualization, and restricted resolution to expose invariants that can replace runtime checks.Source: §1 · p. 2
  • A falsified mixed reach yields a white tail disjoint from the triggering token distribution, while every old white tail intersects it, ruling out old-white subsumption.This structural guarantee replaces the runtime novelty and non-subsumption test for these candidates.Source: §1 · p. 2
  • In the frozen-snapshot solver, every active token distribution produces a non-subsumed refinement, removing the resolved and white-fixpoint SAT branches.New reaches are collected during the iteration and installed afterward, preserving a fixed old-reach set but allowing within-batch redundancy and extra work.Source: §1 · pp. 2–3
  • The paper’s contributions include formalizing C-falsified reaches, proving the private-pivot non-subsumption result, and evaluating the revised snapshot/full-DNF control flow.The evaluation includes all 1,000 uf20-91 instances and compares three DNF-control configurations.Source: §1 · p. 3

2 Related Work

The paper places RN-Solver at the intersection of resolution and monotone dualization, distinguishing its dualization-guided proof structure from branching-based SAT and other graph or compiled representations. It uses these connections to clarify the scope of its subsumption result.

2 Related Work

  • RN-Solver belongs to the resolution-based SAT line but uses dualization-driven control rather than DPLL/CDCL-style branching.Its private-pivot chains resolve a selected mixed reach against selected current old white reaches, with pivots supplied by a minimal hitting set.Source: §2 · p. 3
  • RN-Solver remains subject to resolution-style worst-case limitations; its stated interest is guiding restricted resolution through the RN representation and dualization layer.The paper distinguishes this aim from evading known proof-complexity limitations.Source: §2 · pp. 3–4
  • Minimal transversals guide RN-Solver’s resolution and certify non-subsumption, but the paper does not propose a new transversal enumerator.Earlier work studies monotone dualization and practical transversal enumeration.Source: §2 · p. 4
  • Unlike BDD, ZDD, or DNNF-style representations, an RN retains a clause-level correspondence and expresses resolution as operations on reaches.RNs were introduced as a graph-based representation of SAT, and RN-Solver combined them with dualization and private-pivot resolution.Source: §2 · p. 4
  • The result removes old-white subsumption checks only for private-pivot candidates learned from falsified mixed reaches, not redundancy control in general.The snapshot discipline fixes the white family used for token generation and the guarantee; batch-local redundancy remains a separate implementation issue.Source: §2 · p. 4

3 Definitions

The definitions establish reaches as the clause-bearing units of a resolvable network and define the token distributions and falsification conditions used in learning. They also fix the iteration snapshot that anchors the old-white guarantee.

3 Definitions

  • A resolvable network is a directed graph whose reaches correspond to clauses, with ordinary subnetworks and distinguished Source and Sink symbols.Allowed reach forms are mixed, white, black, and empty; Source marks an absent negative-literal side and Sink an absent positive-literal side.Source: §3 · p. 5
  • Token distributions are inclusion-minimal hitting sets of the current white tails, and each selected variable has a private witness tail intersecting the distribution only there.This private-element property supplies the witnesses used by private-pivot learning.Source: §3 · p. 5
  • A token distribution is black-blocked when a black reach’s head is contained in it, terminal when its valuation clause is not subsumed by any reach, and active otherwise..Source: §3 · p. 5
  • A reach is C-falsified when its clause is false under the valuation making exactly the variables in C true.For a mixed reach (G,H), this means G is contained in C and H is disjoint from C.Source: §3 · p. 5
  • The private-pivot construction selects one private witness white tail for each variable in the head of a C-falsified mixed reach.The resulting white tail is defined by the displayed construction.Source: §3 · p. 6
  • An iteration snapshot fixes the network and white family at the start of the main-loop iteration, and the DNF and non-subsumption statements are interpreted against that snapshot.It is formed after initial unit-propagation and decision checks and contains no empty reach.Source: §3 · p. 6

4 Theoretical Results

For a current token distribution, falsifying a mixed reach yields a private-pivot white tail disjoint from that distribution, so no old white reach subsumes it. This supports productive active distributions and the revised solver’s decide-or-refine outcomes.

4 Theoretical Results

  • Every current minimal hitting set intersects every old white tail, so no old white reach is C-falsified.This is the invariant that distinguishes old white reaches from the mixed reach used to learn.Source: §4 · p. 6
  • A C-falsified mixed reach yields a private-pivot tail disjoint from C, while every old white tail intersects C, ruling out old-white subsumption.The complement lemma gives disjointness; the subsumption-free theorem applies it to every old white reach.Source: §4 · p. 6
  • Private-pivot chains preserve satisfiability because each reach-resolution step is sound, even without a subsumption test.Every learned white reach is a logical consequence of the snapshot network.Source: §4 · p. 7
  • Adding the generated white tail eliminates its generating token distribution from the next DNF because that distribution does not hit the new tail.The introductory example shows C still hits both old tails but not the newly added tail.Source: §4 · p. 8
  • Every active snapshot token distribution has a falsified mixed witness and yields a private-pivot white reach not subsumed by old white reaches.Thus the snapshot formulation has no active-but-resolved distribution.Source: §4 · pp. 6, 8
  • One snapshot iteration returns SAT if any distribution is terminal, UNSAT if all are black-blocked, or generates at least one new old-white-non-subsumed reach.If neither decision case holds, an active distribution is productive.Source: §4 · p. 8
  • A unit private-pivot tail arises when the mixed tail is {u} and each chosen private witness adds no variable beyond u after its pivot is removed.The text notes that other valid witness choices need not yield a unit.Source: §4 · p. 8
  • The lost-private heuristic characterizes when adding a tail preserves a minimal hitting set, while partial DNF terms alone cannot generally support exact incremental updates.Exact incremental DNF requires the full old DNF or an independent completeness certificate.Source: §4 · p. 8

5 From the Original Algorithm to the Revised Algorithm

The revised control flow learns only from C-falsified mixed reaches in a frozen snapshot and installs new white reaches after processing the iteration. The theorem replaces old-white subsumption checks, resolved markers, and the white-fixpoint SAT branch.

5 From the Original Algorithm to the Revised Algorithm

  • The original solver explicitly tested candidate novelty and subsumption, marked distributions resolved when no candidate was found, and used a white-fixpoint SAT branch.That branch applied when all token distributions were black-blocked or resolved.Source: §5 · p. 9
  • The revised algorithm uses a frozen snapshot, learns only from C-falsified mixed reaches, and skips old-white subsumption checks by theorem.It removes the resolved marker and white-fixpoint SAT branch; exact duplicates may still be removed within the batch.Source: §5 · p. 9
  • The old and revised flows differ in distribution handling: the revision uses snapshot-generated DNF terms and treats active terms as productive.The comparison also contrasts trying all C′ ⊆ C with using only C-falsified mixed reaches.Source: §5 · p. 9

6 Revised Algorithm

The reference revised algorithm processes token distributions from a frozen snapshot, batches learned white reaches, and adds the batch at iteration end. Soundness follows from unit propagation and private-pivot soundness; termination follows from strict white refinement over a finite universe.

6 Revised Algorithm

  • The reference snapshot/full-DNF solver exhausts unit propagation, computes DNF from frozen white tails, processes distributions, batches learned tails, and installs them at iteration end.It decides SAT for a terminal distribution or UNSAT when every distribution is black-blocked; otherwise it starts another iteration after adding the batch.Source: §6 · p. 9
  • Soundness follows from unit propagation and private-pivot soundness, while termination follows because each non-decision iteration adds an old-white-non-subsumed tail over a finite universe.Exact duplicate filtering within the batch does not replace the non-subsumption guarantee.Source: §6 · p. 9
  • Exact incremental DNF updates the complete previous DNF with recomputation when needed, while depth-first restart refines one minimal distribution and restarts instead of materializing the full DNF.Study 2 compares their runtime and memory trade-offs; snapshot/full-DNF remains the reference formulation.Source: §6 · p. 9

7 Empirical Evaluation

The evaluation compares the revised control flow with the original, tests three DNF-control configurations, and explores black-side enrichment and correlates of solver difficulty. It is not intended as a comparison with modern CDCL solvers.

7.1 Study 1: Original vs. Subsumption-Free Control Flow

  • Study 1 compares the original and revised control flows in the same implementation, so runtime differences reflect combined changes rather than isolated removal of subsumption checks.The comparison combines snapshot updates, learning from C-falsified mixed reaches, and removing old-white subsumption checks.Source: §7.1 · p. 10

7.1.1 Detailed Ten-Instance Comparison

  • 4.84× was the old/sf median-runtime ratio on the original ten-instance uf20 subset; old hard rows made many checks, while revised completed rows made none.This was a preliminary, one-run-per-configuration comparison with an 8-second timeout.Source: §7.1.1 · p. 10, §7.1 · p. 10

7.1.2 Full uf20-91 Fixed-Budget Validation

  • 963 of 1,000 uf20-91 instances were solved by snapshot/full-DNF within 8 seconds, versus 724 by the original control flow (a 23.9-point difference).All 963 completed revised runs reported zero old-white subsumption checks; all successful models were independently validated.Source: §7.1.2 · p. 11

7.2 Study 2: DNF-Control Strategy Comparison

  • Incremental DNF completed all 100 instances across repetitions (full-DNF 94; depth-restart 60); paired incremental/full median ratios favored incremental for wall time (0.807) and solver time (0.665).The comparison covers implemented configurations, not a pure traversal ablation; depth-restart was less effective under this budget, and the strategy ranking is benchmark-specific.Source: §7.2 · pp. 12–13

7.3 Study 3: Exploratory Resolution-Derived Black Enrichment

  • At the 20% enrichment target, median materialized DNF terms fell from 3988 to 2555 and old-solver time from 664 ms to 454 ms, but the result is inconclusive.Black-aware pruning counters remained zero, so the improvement cannot be attributed to that mechanism; larger runs and finer instrumentation are needed.Source: §7.3 · p. 13

7.4 Study 4: Structural Correlates of Solver Difficulty

  • At 8 seconds, successful/timeout black-clause medians were 12/9 for old and 11/8 for sf-full-dnf; these exploratory associations are non-causal.The analysis measures clause-sign composition, not incidence topology, white-tail overlap, hitting-set counts, DNF size, or private-witness structure.Source: §7.4 · pp. 13–14

8 Conclusion

The paper replaces runtime subsumption checks with a structural guarantee for learning from C-falsified mixed reaches, and reports improved 8-second coverage for snapshot/full-DNF. It also identifies follow-up evaluations for black enrichment, incremental DNF, and polarity renaming.

8 Conclusion

  • For C-falsified mixed reaches, the learned white tail is disjoint from C while every old white tail intersects C, ruling out old-white subsumption.The structural result replaces a runtime subsumption check with a theorem.Source: §8 · p. 14
  • In the frozen-snapshot algorithm, each active nonterminal, non-black-blocked token distribution yields a C-falsified mixed reach and a non-subsumed private-pivot refinement.Each non-decision iteration performs a strict white refinement and eliminates the distribution that generated the new reach; the resolved marker and white-fixpoint SAT branch are unnecessary.Source: §8 · p. 14
  • 963 of 1,000 uf20-91 instances were solved within 8 seconds by snapshot/full-DNF, compared with 724 by the original control flow.Exact incremental DNF completed all three repetitions of every instance in the 100-instance strategy holdout and reduced paired runtime and peak working set relative to full-DNF.Source: §8 · p. 14
  • The authors propose testing resolution-derived black enrichment on larger SAT and UNSAT benchmarks and evaluating incremental DNF on more diverse families.Depth-first and unit-oriented DNF control need more efficient oracles that certify minimality without shifting cost from materialization to search.Source: §8 · pp. 14–15
  • Polarity renaming is proposed as a way to increase initial black reaches, but its performance benefit remains unestablished.A dedicated paired comparison should fix solver settings, include preprocessing cost, map models back, and account for other clause-sign changes.Source: §8 · p. 15
Loading 2609.34880v1…