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%。
正文 · AI 翻译
摘要：连接表证明器通常通过回溯搜索来构造封闭的表。这带来了轻量级的证明过程，但其低内存的搜索状态在尝试失败后几乎没有可复用的派生信息。SATCoP 通过将接地表子句保留在增量 SAT 求解器中来解决这一问题，使证明器在累积的接地子句变为命题不可满足时能够反驳该问题。我们提出 SATResetCoP，它更直接地依赖这种持久 SAT 状态，不对无产出的表进行回溯，而是启动新表为 SAT 求解器生成更多接地子句。在 TPTP 上，SATResetCoP 相比我们 leanCoP 风格的基线提升了 54%，相比我们 SATCoP 风格的基线提升了 18%。在 bushy MPTP2078 基准上，它求解了 616 个问题，相比我们 leanCoP 风格的基线提升了 49%，相比我们 SATCoP 风格的基线提升了 12%。这些结果表明，改变表引导方式以更快地累积有用的接地子句可提升证明器的性能。
| 评论： | 13 页，6 幅图，5 张表。发表于 Vampire 2026。代码：此 https URL |
| 主题： | 计算机科学中的逻辑（cs.LO）；人工智能（cs.AI） |
| ACM 分类： | F.4.1；I.2.3 |
| 引用为： | arXiv:2610.18204 [cs.LO] |
| （或 arXiv:2610.18204v1 [cs.LO] 用于此版本） | |
| https://doi.org/10.48550/arXiv.2610.18204 由 DataCite 颁发的 arXiv DOI（待注册） |
提交历史
来自：Fredrik Rømming [查看电子邮件]
[v1]
2026 年 10 月 13 日星期二 11:39:45 UTC（503 KB）
来源：arXiv cs.AI · arxiv.org