Reset Early, Reset Often, Eliminate Models
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-sty...
| Authors | Martin S. Fixman, Fredrik Rømming, Sean B. Holden |
|---|---|
| Primary category | cs.LO |
| Published | 13 October 2026 |
| Last updated at source | 13 October 2026 |
Silytics shows public metadata from arXiv and links to the original. Information may be incomplete or out of date. Last refreshed 15 October 2026. Licenses and terms of the original apply to the work itself. Not financial, legal or professional advice.