arXiv cs.AI· Martin S. Fixman, Fredrik R{\o}mming, Sean B. Holden·· 3 天前AI 评分13
SATResetCoP：不回退低效 tableau，加速积累 ground 子句以提升定理证明器性能
Reset Early, Reset Often, Eliminate Models
AI 导读
SATResetCoP 通过不再回退无产出的 tableau、转而开启新 tableau 为 SAT 求解器生成更多 ground 子句，在 TPTP 上较 leanCoP 风格基线提升 54%、较 SATCoP 风格基线提升 18%。
正文 · 原文
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