Subsumption-Free Private-Pivot Learning in Resolvable Network-Based SAT Solving
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.