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.
Figures & tables
Figure 1: Drawing convention for the tableau diagrams, illustrated on steps from SYN052-1.p [ 16 ] . Each box is a clause instance in the tableau. An edge records the connection that introduced a child clause, with the edge label showing the resulting substitution. Grey boxes mark clauses whose selected open literal has been closed. A Reduction closes against a complementary literal already on the current path, so it adds no new child.
Figure 2: Example of SATResetCoP on SYN052-1.p . SATCoP and previous provers would backtrack after closing the branch with F(x1)∨¬p ; instead, SATResetCoP resets into a new tree. This accumulates the ground clauses that form the UNSAT core shown at the bottom faster than in SATCoP , allowing the SAT solver to reach unsatisfiability earlier. Substitutions are omitted for simplicity. At the end of the last extension, the accumulated ground clauses are unsatisfiable and the entire tableau prover can report UNSAT.
Strategy
Explanation
Cut
SAT Refutation
SAT Guidance
Reset on Backtrack
leanCoP Con
leanCoP with initial set of predicates.
✓
SATCoP 0 Con
Based on the initial implementation of SATCoP [ 18 ] .
✓
✓
SATCoP Con
Improvements on SATCoP [ 18 , § 9.1] .
✓
✓
✓
SATResetCoP
Novel strategy, specified in Section 0.3.1 .
✓
✓
✓
✓
Table 1: Control features of the baseline strategies and SATResetCoP .
TPTP CNF
TPTP FOF
MPTP2078
Total
strategy
Number
%
Number
%
Number
%
Number
%
leanCoP Con
723
9.3
1200
13.7
413
19.9
2336
12.5
SATCoP 0 Con
804
10.3
1067
12.2
321
15.4
2192
11.7
SATCoP Con
1067
13.7
1442
16.4
549
26.4
3058
16.4
SATResetCoP
1273
16.3
1698
19.3
616
29.6
3587
19.2
Table 2: Number and percentage of TPTP CNF, TPTP FOF, and MPTP2078-derived problems solved within the time limit by each strategy. The total column combines all three benchmark sets.
Figure 3: Results of running the strategies on all TPTP problems under a time limit of 120 seconds and step limit of 1 million steps. SATResetCoP solves more problems in fewer steps than in previous strategies, and also faster except for the niche category of ≤1s solves.
Strategy
Newly Solved
Newly Unsolved
Total Solved
leanCoP Con
—
—
1923
SATCoP 0 Con
327
379
1871
SATCoP Con
661
23
2509
SATResetCoP
598
136
2971
Table 3: Problems from the TPTP dataset newly solved and newly unsolved by each strategy compared with the previous strategy in the table, together with the total number of solved problems. The reset policy changes which parts of the search space are explored: SATResetCoP solves 598 TPTP problems missed by SATCoP Con , but misses 136 problems solved by SATCoP Con . This shows that aggressive resetting is not only a speedup of the same proof attempts, but a different search tradeoff.
Figure 4: Pairwise comparison of strategy results: the cell in column y and row x shows the number of problems solved by strategy y , but not by strategy x . For example, SATResetCoP solved 1123 TPTP problems that SATCoP 0 Con did not.
Strategy
SYN
SWC
SWV
GEO
NUM
Rest
Total
leanCoP Con
486
14
163
216
86
958
1923
SATCoP 0 Con
459
2
161
177
90
982
1871
SATCoP Con
549
11
173
260
151
1365
2509
SATResetCoP
672
64
215
293
179
1548
2971
Table 4: Number of problems solved, per category, for each strategy.
Figure 5: Density of problems solved at each step count by SATCoP Con and SATResetCoP on the TPTP categories SYN , SWC , SWV , GEO , and NUM . The area of each violinplot is the same; besides solving more problems in each category, SATResetCoP solves many problems in fewer steps. Unsolved problems are collected in the ≥10k category on the right.
FOF
CNF
Declared status
Unsolved
Solved
Unsolved
Solved
Satisfiable
358
0
1095
0
CounterSatisfiable
746
0
0
0
Unknown
139
0
745
0
Open
4
0
28
0
Unsatisfiable
110
66
4674
1273
Table 5: Number of problems solved and unsolved by SATResetCoP , grouped by TPTP declared status. No satisfiable or countersatisfiable problem was incorrectly proven to be unsatisfiable.
Modern SAT solvers combine a rich repertoire of proof rules with sophisticated strategies that determine when and how to apply them. Often, the internal implementations are tightly coupled to particular strategies, making it inconvenient to define new strategies without changing solver internals. We present Tactix, a proof-producing sequential CDCL solver that incorporates a wide range of techniques in state-of-the-art solvers with a clean separation of proof rules from solving strategies. This separation enables a public interface through which users can invoke particular techniques, observe their effects, and program a wide range of solving strategies. The default strategy of Tactix is programmable over this interface and outperforms state-of-the-art solvers on benchmarks from the 2024--2026 SAT Competitions. We also use the interface to develop novel strategies tailored to challenging benchmarks from two application domains, which led to performance gains over strong baselines. We intend Tactix to serve as an infrastructure for designing and evaluating novel solving strategies. Finally, we also present a self-study of the AI-assisted development process behind Tactix.
Haoze Wu, André Schidler, Armin Biere +1
Amherst College, Amherst, MA, USA · University of Freiburg, Freiburg im Breisgau, Germany · Broadcom, Palo Alto, CA, USA
We investigate two approaches for extending CEGAR-tableaux with SAT-shortcuts using a previously known approach called RECAR but also a totally new approach using the modal resolution theorem prover KSP as an oracle. Our experiments using our C++ implementation CEGARBox++ of CEGAR-tableaux show that: (1) CEGARBox++ with RECAR SAT-shortcuts is not competitive (2) CEGARBox++ using KSP to provide SAT-shortcuts is superior to both CEGARBox++ and KSP, particularly on large satisfiable problems. As far as we know, this is the first effective integration of SAT, tableaux and resolution methods for modal satisfiability which performs better than its parts.
Rajeev Goré, Cormac Kikkert
Faculty of Information Technology, Monash University, Australia · Cormac Kikkert Research
SAT solvers settle combinatorial problems beyond the reach of interactive theorem provers and produce LRAT certificates for independent verification. We present LRAT-Catcher, a standalone, general-purpose tool that imports a DIMACS formula together with an LRAT certificate into Lean 4 as a theorem. LRAT-Catcher runs the formally verified LRAT checker from Lean core as compiled native code via reflection. This scales to instances where Mathlib's explicit proof-term import exhausts memory. LRAT-Catcher also composes cube-and-conquer solving runs entirely inside Lean. Per-cube refutations are combined with a cover-completeness certificate, itself an LRAT proof, into a single unsatisfiability theorem. Verified encodings connect CNF-level results to the original combinatorial problems. We evaluate the tool against Mathlib's proof-term import and the external checker cake_lpr on establishing the Schur number S(4) = 44 and the Ramsey number R(4,4) = 18 as Lean theorems.
Stefan Szeider
Algorithms and Complexity Group, TU Wien, Vienna, Austria