发表机构
Faculty of Informatics, Eszterh\'azy K\'aroly Catholic University, Eger, Hungary
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
针对RN-Solver中全局包容测试耗时过高的问题，提出无包容的私轴学习变体，基于快照结构优化主循环，证明算法可靠性，实验显示求解效率显著提升。
AI 中文摘要
可解网络（resolvable network，RN）是SAT的有向图表示：每个SAT实例都可转化为RN，且每个RN都对应一个CNF公式。每条reach代表一个子句。在混合reach中，头和尾是不相交的变量集，分别包含子句中负出现和正出现的变量；特殊符号Source和Sink代表缺失的负文字侧或正文字侧。RN-Solver是基于该表示的概念验证SAT求解器。其全正子句由白色reach表示，令牌分布是当前白色尾部的极小命中集，由单调CNF-DNF对偶化生成。RN-Solver通过私轴归结（private-pivot resolution）学习新的白色reach，这是一种结构化归结序列，使用旧的白色reach作为枢轴见证。在原始算法中，由该链生成的每个候选白色reach之后，都要针对当前网络进行全局包容测试。性能分析显示，在随机3-SAT实例上，该包容测试可能占据运行时间的主导地位。我们证明，当用于学习的混合reach被当前令牌分布证伪时，即该分布使头部所有变量为真、尾部所有变量为假时，该检查是不必要的。关键不变量很简单：生成的白色尾部与触发令牌分布不相交，而同一分布与每个旧的白色尾部都相交。因此，没有任何旧的白色reach能包容生成的reach。这一结构性观察使我们能够构建更简单的、基于快照的无包容RN-Solver变体，其中每个主循环迭代使用固定的旧reach集合，并仅在迭代结束时安装新生成的白色reach。我们证明了修订后算法的可靠性。实证评估证实了目标检查的消除：在8秒的时间预算内，snapshot/full-DNF求解了1000个uf20-91实例中的963个，而原始控制流仅求解724个。另一项包含100个实例的比较表明，精确增量DNF是三种测试配置中最有效的。
英文摘要
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.
CommentsIn Proceedings FROM 2026, arXiv:2609.30324
Journal refEPTCS 452, 2026, pp. 35-50
