Resolvable network method improves SAT solving without subsumption checks
Subsumption-Free Private-Pivot Learning in Resolvable Network-Based SAT Solving
Logic in Computer Science
Summary
SAT problem solvers try to find assignments for variables that satisfy logical formulas. The authors study a special way to represent SAT problems using directed graphs called resolvable networks. They show that a certain time-consuming check in their solver can be skipped without losing correctness by using structural properties of the network. This makes their solver faster on tested problems, solving more instances within a time limit. Their approach also simplifies the solver’s design.
What this means in practice
- •For software verification engineers: Use the improved RN-Solver to verify logical conditions in software faster by eliminating costly subsumption checks during SAT solving.
- •For hardware design verification teams: Incorporate the snapshot-based RN-Solver to speed up hardware logic verification tasks by reducing redundant logical checks in the solving process.
Authors
Gábor Kusper
Abstract
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.