arXiv：cs.AI· Martin S. Fixman, Fredrik R{\o}mming, Sean B. Holden·· 22 小时前
SATResetCoP：不回溯、多重启，用持久 SAT 状态加速连接表证明器
Reset Early, Reset Often, Eliminate Models
AI 导读
SATResetCoP 放弃在无产出的 tableau 上回溯，改为直接重启新 tableau 以更快为增量 SAT 求解器积累 ground clauses。在 TPTP 上它比 leanCoP 风格基线提升 54%、比 SATCoP 风格基线提升 18%；在 bushy MPTP2078 基准上解出 616 题，分别提升 49% 和 12%。该工作发表于 Vampire 2026。
正文
Abstract:Connection-tableau provers typically construct closed tableaux by backtracking search. This gives lightweight proof procedures, but their low-memory search state leaves little derived information to reuse after a failed attempt. SATCoP addresses this by retaining grounded tableau clauses in an incremental SAT solver, allowing the prover to refute the problem once the accumulated ground clauses become propositionally unsatisfiable. We introduce SATResetCoP, which relies more directly on this persistent SAT state by not backtracking on unproductive tableaux and instead starting new ones to generate further ground clauses for the SAT solver. On TPTP, SATResetCoP improves over our leanCoP-style baseline by 54% and our SATCoP-style baseline by 18%. On the bushy MPTP2078 benchmark, it solves 616 problems, a 49% improvement over our leanCoP-style baseline and a 12% improvement over our SATCoP-style baseline. These results suggest that changing tableau guidance to accumulate useful ground clauses faster improves the performance of the prover.
| Comments: | 13 pages, 6 figures, 5 tables. Presented at Vampire 2026. Code: this https URL |
| Subjects: | Logic in Computer Science (cs.LO); Artificial Intelligence (cs.AI) |
| ACM classes: | F.4.1; I.2.3 |
| Cite as: | arXiv:2610.18204 [cs.LO] |
| (or arXiv:2610.18204v1 [cs.LO] for this version) | |
| https://doi.org/10.48550/arXiv.2610.18204 arXiv-issued DOI via DataCite (pending registration) |
Submission history
From: Fredrik Rømming [view email]
[v1]
Tue, 13 Oct 2026 11:39:45 UTC (503 KB)
来源：arXiv：cs.AI · arxiv.org