Paper deep dive
Reset Early, Reset Often, Eliminate Models
Martin S. Fixman, Fredrik Rømming, Sean B. Holden
Intelligence
Status: not_run | Model: - | Prompt: - | Confidence: 0%
Entities (0)
Relation Signals (0)
No relation signals yet.
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
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.
Tags
Links
- Source: https://arxiv.org/abs/2610.18204v1
- Canonical: https://arxiv.org/abs/2610.18204v1
Trouble viewing inline? Open PDF directly →
Full Text
35,877 characters extracted from source content.
Expand or collapse full text
Reset Early, Reset Often, Eliminate Models Martin S. Fixman Fredrik Rømming Sean B. Holden Email: fr409@cl.cam.ac.uk Email: sbh11@cl.cam.ac.uk Affiliation: University of Cambridge, United Kingdom Email: msf43@cl.cam.ac.uk 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 616616 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. 0.1 Introduction Connection-tableau provers prove first-order problems by constructing closed tableaux from sound tableau-construction rules [8]. Implementations usually turn this construction into backtracking search over applications of those rules. This gives a lightweight and goal-directed proof procedure, but its small search state means that failed partial tableaux leave little derived information for later attempts to reuse. Much practical work on connection-tableau proving has therefore focused on controlling backtracking, and learning how to restrict it. The line from semantic tableaux and model elimination to leanTAP and leanCoP showed that goal-directed tableau search could be implemented in small, effective proof procedures [4, 9, 3, 11]. leanCoP uses Prolog’s SLD resolution for depth-first connection-tableau search with iterative deepening, and leanCoP 2.0 obtains substantial speedups by restricting this backtracking with Prolog cuts at the cost of completeness [14]. meanCoP refines this pruning strategy by separating cuts on reductions from cuts on extensions and by introducing exclusive cuts, which preserve more alternatives than the inclusive cuts used by leanCoP [6]. SATCoP addresses the same weakness from a different direction [18]. During tableau construction, it grounds encountered clauses and stores them in an incremental SAT solver. If the accumulated ground clauses become propositionally unsatisfiable, the original first-order problem can be proved before the active tableau has closed. We introduce SATResetCoP, which pushes this idea further: when the active tableau stops producing new ground clauses, it is reset, while the accumulated SAT solver state is kept. The tableau is therefore used as a generator of ground clauses, and the SAT solver becomes the persistent object from which a proof may ultimately be obtained. We evaluate SATResetCoP on TPTP against leanCoP-style and SATCoP-style baselines implemented in a fully compatible backend. SATResetCoP solves 54% more problems than the leanCoP-style baseline and 18% more than the SATCoP-style baseline, suggesting that once ground clauses are preserved in the SAT solver, starting a new tableau rather than continuing to backtrack on an unproductive one can be an effective way to generate the clauses needed for a proof. 0.2 Preliminaries 0.2.1 Connection Calculus and Tableau Search Connection tableaux and model elimination give a goal-directed alternative to the saturation style used by provers such as Vampire [19]. Instead of deriving clauses from a global clause set until a contradiction is found [2, 21], connection calculi try to close a tableau by connecting goal literals to complementary literals, either on the current path or in a fresh copy of an input clause [8, 12]. The standard clausal connection tableau has three proof-building rules [8, 13]. Start Choose an input clause and make its literals open goals. Extension Open a branch on a clause containing a complementary literal, and add the remaining literals as new subgoals. This may require a substitution of variables with terms. Reduction Close the current goal against a complementary literal already on the current branch. This may also require a substitution. The rules are sound, and with the possibility of backtracking over rule applications the calculus is complete. The calculus is not confluent: a locally sound connection can bind variables in a way that prevents later branches from closing [8]. Backtracking is therefore part of the operational search procedure, not a proof-building rule. StartF(Y)∨pF(Y) pExtensionF(Y)∨pF(Y) p¬F(X)∨p F(X) pσ0=X←Y _0=\X← Y\ExtensionF(Y)∨pF(Y) p¬F(X)∨p F(X) p¬p∨¬F(a) p F(a)σ1=σ0 _1= _0σ0=X←Y _0=\X← Y\ReductionF(a)∨pF(a) pσ2=X←aY←a _2= \ gatheredX← a\\ Y← a gathered \¬F(a)∨p F(a) p¬p∨¬F(a) p F(a)ExtensionF(a)∨pF(a) pσ2=X←aY←a _2= \ gatheredX← a\\ Y← a gathered \¬F(a)∨p F(a) p¬p∨¬F(a) p F(a)¬F(a)∨¬p F(a) p 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. 0.2.2 Backtracking Control Backtracking lets a prover recover from locally sound choices that later prevent tableau closure. In leanCoP-style provers, this search is controlled mainly by iterative deepening and Prolog cuts. Iterative deepening bounds the tableau height and raises the bound when no proof is found. Cuts prune alternatives after selected reductions or extensions, reducing search but making the cut phase incomplete unless the surrounding schedule later explores less restricted search [14]. meanCoP refines this pruning mechanism by separating cuts on reductions from cuts on extensions and by introducing exclusive cuts, which preserve more alternatives than the inclusive cuts used by leanCoP [6]. hopCoP takes a different route: instead of pruning alternatives directly, it learns constraints explaining why a search state is stuck, reducing repeated backtracking while preserving completeness at a fixed iterative-deepening bound [17]. 0.2.3 SATCoP and Persistent Ground Clauses SATCoP maintains an incremental SAT solver alongside tableau search [18]. During tableau search, clauses appearing in the tableau are heuristically grounded and added to the SAT solver. If the accumulated ground clauses are propositionally unsatisfiable, proof search can stop even if the active first-order tableau has not closed. The soundness condition is that every clause sent to the SAT solver must be a ground instance of a clause generated by the tableau. Remaining tableau variables are therefore mapped to ground terms before a clause is added. Rawson and Reger use the grounding heuristic inspired by a similar suggestion by Schulz [22]: choose the most frequent constant in the conjecture, falling back to a fresh constant when no conjecture constant is available [18]. Later SATCoP variants also use the SAT solver to guide tableau search. Rawson and Reger describe a literal-selection refinement that prefers extension choices whose selected literal is true in the current SAT assignment [18, § 9.1]. 0.3 Research Vehicle 0.3.1 SATResetCoP Specification We propose a new tableau prover based on SATCoP, but guided by the goal of producing the ground clauses needed for a SAT refutation rather than using the leanCoP heuristics that attempt to close the current tableau. The resulting strategy is simple: aggressively reset the tree when the SAT solver stops receiving new ground clauses. This adds a broader set of ground clauses to the solver in less time, allowing the SAT solver to reach unsatisfiability earlier. SATResetCoP uses many of the properties of SATCoP described in the original paper and in its “Future Research” section [18, § 9.1], but changes the tableau guidance to prioritise aggressive resets. Like SATCoP, the implementation keeps a persistent SAT solver alongside the active tableau search. Ground clauses accumulated in earlier tableau attempts remain available in later attempts, and new clauses are added incrementally to the same solver instance. This keeps the approach sound but incomplete. However, we expect it to certify unsatisfiability of problems faster and in fewer steps. SATResetCoP randomises the Start and Extension steps in the same way as SATCoP. When starting a new tree, the implementation shuffles the possible starts and the literals inside each start clause. When several extensions are possible from the leftmost open node, it shuffles the extension choices and the literal order inside the copied extension clause. A new virtual operation, Reset, clears the tableau, the current substitution, and the proof sequence, and starts a new tableau attempt with a specified depth bound. It does not clear the persistent SAT solver: every reset starts from an empty tree, while the SAT solver keeps the ground information produced by earlier attempts. An example of how this operation works can be seen in Figure 2. Start¬F(g)∨p F(g) p¬F(g)∨p Bmatrix F(g) p BmatrixExtension¬F(g)∨p F(g) pF(x0)∨¬pF(x_0) p¬F(g)∨pF(x0)∨¬p Bmatrix F(g)& & p\\ F(x_0)& & p BmatrixExtension¬F(g)∨p F(g) pF(x0)∨¬pF(x_0) pF(x1)∨¬pF(x_1) p¬F(g)∨pF(x0)∨¬pF(x1)∨¬p Bmatrix F(g)& & p\\ F(x_0)& & p\\ F(x_1)& & p BmatrixReduction¬F(g)∨p F(g) pF(x0)∨¬pF(x_0) pF(x1)∨¬pF(x_1) p¬F(g)∨pF(x0)∨¬pF(x1)∨¬p Bmatrix F(g)& & p\\ F(x_0)& & p\\ F(x_1)& & p BmatrixResetStartp∨F(g)p F(g)¬F(g)∨pF(x0)∨¬pF(x1)∨¬p∨F(g) Bmatrix F(g)& & p\\ F(x_0)& & p\\ F(x_1)& & p\\ p& & F(g) BmatrixExtensionp∨F(g)p F(g)¬p∨¬F(a) p F(a)¬F(g)∨pF(x0)∨¬pF(x1)∨¬p∨F(g)¬p∨¬F(a) Bmatrix -2.0pt F(g)& & p -2.0pt\\ -2.0pt F(x_0)& & p -2.0pt\\ -2.0pt F(x_1)& & p -2.0pt\\ -2.0pt p& & F(g) -2.0pt\\ -2.0pt p& & F(a) -2.0pt BmatrixExtensionp∨F(g)p F(g)¬p∨¬F(a) p F(a)F(a)∨¬pF(a) p¬F(g)∨pF(x0)∨¬pF(x1)∨¬p∨F(g)¬p∨¬F(a)F(a)∨¬p Bmatrix -2.0pt F(g)& & p -2.0pt\\ -2.0pt F(x_0)& & p -2.0pt\\ -2.0pt F(x_1)& & p -2.0pt\\ -2.0pt p& & F(g) -2.0pt\\ -2.0pt p& & F(a) -2.0pt\\ -2.0pt F(a)& & p -2.0pt Bmatrix Figure 2: Example of SATResetCoP on SYN052-1.p. SATCoP and previous provers would backtrack after closing the branch with F(x1)∨¬pF(x_1) 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. The grounded clauses used by SATResetCoP come from clauses that have appeared in the tableau, after applying the tableau substitution accumulated so far. Start clauses are added to the SAT state when the run is initialised. After successful Extension and Reduction steps, the implementation grounds the clauses currently present in the tableau and records the genuinely new ones, which are later added to the SAT solver. The grounding scheme follows the soundness argument of Section 0.2.3: the SAT solver receives only ground instances of clauses generated by the tableau. Ground terms are kept as they are, and variables assigned by the current tableau substitution are replaced by their assigned terms. Only tableau variables that remain unassigned need to be replaced by a ground term. Our Python SATCoP-style variants use the simpler fallback-style choice throughout, mapping every remaining tableau variable to the same fresh artificial constant. The reset policy does not change this soundness argument. Cuts and resets only affect which ground instances are discovered, and hence the completeness and performance of the search, not the soundness of a SAT refutation once found. The aggressive reset-on-backtrack policy is the main implementation difference between SATResetCoP and SATCoP. At a dead end, the prover first asks whether the current tableau attempt produced any new ground clauses that have not yet been added to the SAT solver. If it did, those clauses are flushed to the SAT solver and the prover resets at the same depth. This gives the next tableau attempt the same depth bound, but a larger SAT state and a fresh set of grounded clauses. If the attempt did not produce any new ground clauses, the prover treats the current depth as exhausted and resets at the next depth instead of spending more steps on local backtracking. The process stops as soon as the accumulated ground clauses become propositionally unsatisfiable. Since SATResetCoP resets the tree aggressively, it only increases the depth bound when the accumulated ground clauses have not been updated since the last Reset. This prevents trees from growing out of control, while still trying to maximise the set of accumulated ground clauses. Pseudocode for this implementation can be found in . ⬇ 1 def solve_tableau(start_clauses): 2 solver := incremental_sat_solver() 3 solver.add(ground(start_clauses)) 4 pending := empty_set 5 6 max_depth := 1 7 tableau := empty_tableau(max_depth) 8 9 while solve_sat(solver) != UNSAT: 10 model := current_model(solver) 11 actions := legal_actions(tableau) 12 13 if any Start, Extension, Reduction in actions: 14 model_rank(a) := 15 2 if a is Start 16 0 if selected_literal(a) is true in model 17 1 if selected_literal(a) is unknown in model 18 3 if selected_literal(a) is false in model 19 20 next_action = argmin(actions, key = model_rank) 21 tableau_step(next_action) 22 23 if next_action is Reduction or Extension: 24 pending.add(ground(tableau)) 25 26 else: 27 if pending is not empty: 28 solver.add_all(pending) 29 pending := empty_set 30 tableau := empty_tableau(max_depth) 31 else: 32 max_depth := max_depth + 1 33 tableau := empty_tableau(max_depth) Listing 1: Pseudocode of the SATResetCoP control policy. 0.3.2 Implementation and benchmarking We implement SATResetCoP using the Connections library [20], which provides primitives for implementing connection-tableau provers, together with the incremental SAT solver CaDiCaL [5]. We also implement the control strategies leanCoPCon, SATCoP0Con, and SATCoPCon using the same backend, as mirrors of LeanCoP, SATCoP0, and SATCoP. Using a common backend makes the strategies easier to compare by keeping the tableau representation, rule applications, grounding interface, SAT interface, and step accounting fixed. The source code for this implementation is available online,11 1 https://github.com/mfixman/resetsatcop and is released under the GNU Lesser General Public Licence [7]. We evaluate these 3 control strategies along with the test strategy SATResetCoP on 78157815 CNF problems and 87798779 FOF problems from the Thousands of Problems for Theorem Provers (TPTP) library [23]. The TPTP problems cover all 50 TPTP categories containing at least one CNF or FOF problem. These benchmark sets provide a varied collection of problems for first-order provers. TPTP also provides declared statuses for its problems, which are a useful sanity check for false unsatisfiability results. We additionally test these strategies in the Bushy MPTP2078 library, which contains 20782078 problems exported from the Mizar Mathematical library [1]. This benchmark is useful because its problems share a large formal-mathematical vocabulary and test whether the strategies remain effective on related large-theory problems rather than only on the more heterogeneous TPTP collection. 0.4 Experimental Evaluation 0.4.1 Experiment Design As a leanCoP-style baseline we use leanCoPCon [14]. This is a Python version of the leanCoP Prolog implementation, with the two recommended predicates used in the first step of the schedule of LeanCoP 2.0 [14, § 5.5]. cut Choose one extension or reduction and commit to it, similarly to Prolog’s ! operator. comp(7) The prover increases the depth bound by 1 whenever the current tree saturates, until reaching maximum height 7. Afterwards, the height limit is removed. These simple policies tend to be very effective in tableau provers [15]. We add Python implementations in the connection prover of the two versions of SATCoP presented by Rawson and Reger [18]: SATCoP0Con, corresponding to SATCoP0, and SATCoPCon, corresponding to the version of SATCoP with the improvements in the “Future Research” section that was submitted to CASC. These implementations use similar techniques to the original provers, and since they use the same backend as SATResetCoP allow for a fair comparison. An overview of these strategies is shown in Table 1. Strategy Explanation Cut SAT Refutation SAT Guidance Reset on Backtrack leanCoPCon leanCoP with initial set of predicates. ✓ SATCoP0Con Based on the initial implementation of SATCoP [18]. ✓ ✓ SATCoPCon 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. Each problem-strategy pair is run until the problem is solved, or until either 120 seconds or 1 million steps pass, on a single core of the University of Cambridge CSD3 Cluster with dual-socket Intel Xeon Platinum 8368Q CPUs at 2.60 GHz, with 38 cores per socket and one thread per core, and 3370 MiB RAM per core [24]. We thank the Computer Science Lab of the University of Cambridge for providing this computer. 0.4.2 Results Individual Results SATResetCoP considerably improves on the number of problems solved by both SATCoP0Con and SATCoPCon under the 120-second time limit, as shown in Table 2. The results are consistent with the claim that the SAT solver reaches unsatisfiability in less time and fewer Start, Extension, and Reduction steps than in the previous strategies, as seen in Figures 3(a) and 3(b). The improvement is visible in both TPTP problem formats and on the MPTP2078-derived problems. SATResetCoP solves 529529 more problems than SATCoPCon, with a net gain of 206206 TPTP CNF problems, 256256 TPTP FOF problems, and 6767 Mizar Bushy problems. Compared with SATCoP0Con, it solves 13951395 more problems, an increase of 63.663.6%, and compared with leanCoPCon it solves 12511251 more problems, an increase of 53.653.6%. TPTP CNF TPTP FOF MPTP2078 Total strategy Number % Number % Number % Number % leanCoPCon 723 9.3 1200 13.7 413 19.9 2336 12.5 SATCoP0Con 804 10.3 1067 12.2 321 15.4 2192 11.7 SATCoPCon 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. (a) Problems solved, stacked by time in seconds. (b) Problems solved, stacked by number of steps. SAT-based strategies can solve a problem in 0 steps if the initial ground SAT clause set is already unsatisfiable. 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≤ 1s solves. Comparative Results The tableau guidance in SATResetCoP allows it to solve several problems left unsolved by strategies without the same mechanism for accumulating ground clauses, and even by SATCoP0Con and SATCoPCon, which use less aggressive guidance. A comparison of newly solved and newly unsolved problems can be seen in Table 3. This comparison is useful because the total number of solved problems hides changes in which problems are solved. On TPTP, SATResetCoP solves 598598 problems that SATCoPCon does not, but loses 136136 problems solved by SATCoPCon. The reset policy is therefore changing the search distribution rather than just speeding up the same proof attempts. Strategy Newly Solved Newly Unsolved Total Solved leanCoPCon — — 1923 SATCoP0Con 327 379 1871 SATCoPCon 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 598598 TPTP problems missed by SATCoPCon, but misses 136136 problems solved by SATCoPCon. This shows that aggressive resetting is not only a speedup of the same proof attempts, but a different search tradeoff. The same tradeoff appears on the bushy MPTP2078 benchmark. SATResetCoP solves 111111 MPTP2078 problems that SATCoPCon does not, while SATCoPCon solves 4444 problems missed by SATResetCoP. The resulting net gain of 6767 problems is smaller than on TPTP, but the pattern is similar. Resets help when useful ground instances appear quickly, and hurt when the useful branch requires longer local tableau search. This is the expected behaviour for a policy that treats the tableau mainly as a source of ground clauses. When the early branches already expose the clauses needed by the SAT solver, resetting avoids spending many steps on similar local backtracking. When the useful clauses only appear after a longer sequence of tableau choices, the same reset policy can discard the partial search state too early. Figure 4 shows the number of problems solved by one strategy but not by another. 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 SATCoP0Con did not. The improvement between SATResetCoP and the best previous experimental strategy, our SATCoPCon implementation of SATCoP, is especially visible in TPTP categories where the accumulated ground clauses become propositionally unsatisfiable quickly, such as SYN, SWC, and SWV. This can be seen in Table 4. As expected, this strategy also solves problems in fewer steps, as can be seen in Figure 6 for TPTP problems and in Figure 6 for the Mizar MPTP2078 dataset. Strategy SYN SWC SWV GEO NUM Rest Total leanCoPCon 486 14 163 216 86 958 1923 SATCoP0Con 459 2 161 177 90 982 1871 SATCoPCon 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 SATCoPCon 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≥ 10k category on the right. Figure 6: Density of problems solved at each step count by SATCoPCon and SATResetCoP on the Mizar Bushy MPTP2078 dataset. Just like in TPTP, SATResetCoP solves more problems in fewer steps. Unsolved problems are collected in the ≥10k≥ 10k category on the right. Satisfiability Sanity Check The TPTP library includes declared statuses for its problems [23]. While this does not demonstrate soundness, it provides a useful check that the strategy has not become unsound by mistake. As a sanity check, we group the SATResetCoP results by TPTP declared status in Table 5. The results are consistent with what we would expect if the prover were sound: it does not find unsatisfiability (“Solved”) in any problem marked satisfiable or countersatisfiable. It also does not solve any unknown or open problems, which would require solutions to be checked closely to ensure that they were not caused by an incorrect prover. 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 ContradictoryAxioms 493 36 0 0 Theorem 5231 1596 0 0 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. 0.5 Conclusion The experiments on SATResetCoP show that replacing local backtracking with resets can improve tableau performance when ground clauses are retained. Section 0.4.2 shows that, on a 1 million step and 120 second time limit, SATResetCoP solves 29712971 problems. This is 462462 more problems than SATCoPCon, an 18% increase, and 10481048 more problems than leanCoPCon, a 54% increase. Pairwise, SATResetCoP solves 598598 problems that SATCoPCon does not, and 11391139 problems that leanCoPCon does not. The improvement is not uniform across TPTP. It is strongest in categories where useful ground clauses accumulate quickly: SATResetCoP solves 672672 SYN problems, 6464 SWC problems, and 215215 SWV problems, compared with 549549, 1111, and 173173 for SATCoPCon. It also improves on GEO and NUM, solving 293293 and 179179 problems respectively. The newly unsolved problems show the other side of this tradeoff. These are cases where the accumulated ground clauses do not become propositionally unsatisfiable quickly enough, and the aggressive reset policy can discard tableau branches that a less aggressive prover eventually closes. This suggests that accumulating ground clauses is a useful objective for connection tableaux, but not a replacement for all tableau control. The most promising direction is therefore not a single fixed reset policy, but a schedule or controller that can use aggressive resets when ground instances are informative and fall back to ordinary connection search when they are not. 0.6 Future Work 0.6.1 Schedule with different provers The reset policy is deliberately incomplete, and the newly unsolved problems show cases where less aggressive tableau search finds proofs that SATResetCoP misses. A natural next step is to use SATResetCoP as one component of a schedule, following leanCoP 2.1 and the strategy-scheduling work of Mangla [14, 10]. leanCoP 2.1, for example, obtains stronger performance by scheduling several strategy variants with different options and resource limits, rather than relying on a single fixed configuration [15]. The simplest schedule would run SATResetCoP first as a fast ground-clause generator, then switch to a more conventional leanCoP- or SATCoP-style strategy after a fixed time or step budget. More adaptive schedules could use the SAT state itself, for example whether new ground clauses are still being produced or recent resets have stopped changing the accumulated clause set. 0.6.2 Further Experiments The current implementation uses CaDiCaL as its incremental SAT solver. Future experiments should test whether the results are stable under different SAT solvers, solver restart policies, and incremental interfaces. This matters because SATResetCoP relies on the solver not only for the final unsatisfiability result, but also for the model information used to guide tableau extensions. It would also be useful to vary the reset policy itself. The present policy resets aggressively when the current tableau stops producing new ground clauses, but the newly unsolved problems suggest that some domains need longer tableau branches before the useful ground instances appear. A broader experiment could compare fixed reset budgets, category-specific schedules, and policies that delay resets when recent SAT models still give useful literal guidance. 0.6.3 CASC Submission SATResetCoP will also be packaged as a CASC entrant. This will test whether the improvements seen here survive the standard competition setting, including the official hardware, time limits, problem selection, and input requirements. It will also make the comparison with earlier connection-tableau systems more direct, since both leanCoP and SATCoP have been evaluated through CASC. Preparing a CASC version requires more than submitting the current research prototype. The prover should expose a stable command-line interface, handle TPTP input robustly, report SZS statuses consistently, and include a reproducible installation path for the SAT backend. This would turn the current experimental result into a system that can be compared against the broader ATP ecosystem. 0.7 Acknowledgements This work was performed using resources provided by the Cambridge Service for Data Driven Discovery (CSD3) operated by the University of Cambridge Research Computing Service (w.csd3.cam.ac.uk), provided by Dell EMC and Intel using Tier-2 funding from the Engineering and Physical Sciences Research Council (capital grant EP/T022159/1), and DiRAC funding from the Science and Technology Facilities Council (w.dirac.ac.uk). References [1] J. Alama, T. Heskes, D. Kühlwein, E. Tsivtsivadze, and J. Urban (2014) Premise selection for mathematics by corpus analysis and kernel methods. Journal of Automated Reasoning 52 (2), p. 191–213. External Links: Document Cited by: §0.3.2. [2] L. Bachmair, H. Ganzinger, D. McAllester, and C. Lynch (2001) Resolution Theorem Proving. In Handbook of Automated Reasoning, p. 19–99. External Links: Document, Link, ISBN 978-0-444-50813-3 Cited by: §0.2.1. [3] B. Beckert and J. Posegga (1995) leanTAP: lean tableau-based deduction. Journal of Automated Reasoning 15 (3), p. 339–358. External Links: Document Cited by: §0.1. [4] E. W. Beth (1955) Semantic entailment and formal derivability. Mededelingen der Koninklijke Nederlandse Akademie van Wetenschappen, Afd. Letterkunde, Nieuwe Reeks, Noord-Hollandsche Uitgevers Maatschappij. Note: Deel 18, no. 13 Cited by: §0.1. [5] A. Biere, T. Faller, K. Fazekas, M. Fleury, N. Froleyks, and F. Pollitt (2024) CaDiCaL 2.0. In Computer Aided Verification, Lecture Notes in Computer Science, Vol. 14681, p. 133–152. External Links: Document Cited by: §0.3.2. [6] M. Färber (2023) A Curiously Effective Backtracking Strategy for Connection Tableaux. In Automated Reasoning with Connection Calculi, J. Otten and W. Bibel (Eds.), CEUR Workshop Proceedings, Vol. 3613, p. 23–40. External Links: 2106.13722, Document, Link Cited by: §0.1, §0.2.2. [7] Free Software Foundation (2007) GNU lesser general public license, version 3. External Links: Link Cited by: §0.3.2. [8] R. Letz and G. Stenz (2001) Model Elimination and Connection Tableau Procedures. In Handbook of Automated Reasoning, p. 2015–2114. External Links: Document, Link, ISBN 978-0-444-50813-3 Cited by: §0.1, §0.2.1, §0.2.1, §0.2.1. [9] D. W. Loveland (1968) Mechanical theorem-proving by model elimination. Journal of the ACM 15 (2), p. 236–251. External Links: Document Cited by: §0.1. [10] C. Mangla, S.B. Holden, and L.C. Paulson (2022) Bayesian ranking for strategy scheduling in automated theorem provers. In International Joint Conference on Automated Reasoning (IJCAR), p. 559–577. External Links: Document Cited by: §0.6.1. [11] J. Otten and W. Bibel (2003) leanCoP: lean connection-based theorem proving. Journal of Symbolic Computation 36 (1–2), p. 139–161. External Links: ISSN 07477171, Document, Link Cited by: §0.1. [12] J. Otten and W. Bibel (2017) Advances in Connection-Based Automated Theorem Proving. In Provably Correct Systems, M. Hinchey, J. P. Bowen, and E. Olderog (Eds.), p. 211–241. External Links: Document, Link, ISBN 978-3-319-48627-7 978-3-319-48628-4 Cited by: §0.2.1. [13] J. Otten and S. Holden (2023) A Syntax for Connection Proofs. In Automated Reasoning with Connection Calculi, J. Otten and W. Bibel (Eds.), CEUR Workshop Proceedings, Vol. 3613, p. 84–94. External Links: Document, Link Cited by: §0.2.1. [14] J. Otten (2010) Restricting backtracking in connection calculi. AI Communications 23 (2–3), p. 159–182. External Links: ISSN 09217126, Document, Link Cited by: §0.1, §0.2.2, §0.4.1, §0.6.1. [15] J. Otten (2023) 20 years of leanCoP — an overview of the provers. In Proceedings of the 1st International Workshop on Automated Reasoning with Connection Calculi (AReCCa@TABLEAUX 2023), CEUR Workshop Proceedings, Vol. 3613. External Links: Link Cited by: §0.4.1, §0.6.1. [16] F. J. Pelletier (1986) Seventy-five problems for testing automatic theorem provers. Journal of Automated Reasoning 2 (2), p. 191–216. External Links: Document Cited by: Figure 1, Figure 1. [17] M. Rawson, C. Eisenhofer, and L. Kovács (2026) Constraint Learning for Non-confluent Proof Search. In Automated Reasoning with Analytic Tableaux and Related Methods, G. L. Pozzato and T. Uustalu (Eds.), Vol. 15980, p. 103–119. External Links: Document, Link, ISBN 978-3-032-06084-6 978-3-032-06085-3 Cited by: §0.2.2. [18] M. Rawson and G. Reger (2021) Eliminating Models During Model Elimination. In Automated Reasoning with Analytic Tableaux and Related Methods, A. Das and S. Negri (Eds.), Vol. 12842, p. 250–265. External Links: Document, Link, ISBN 978-3-030-86058-5 978-3-030-86059-2 Cited by: §0.1, §0.2.3, §0.2.3, §0.2.3, §0.3.1, §0.4.1, Table 1, Table 1. [19] A. Riazanov and A. Voronkov (2002) The design and implementation of VAMPIRE. AI Communications 15 (2–3), p. 91–110. External Links: Document, Link Cited by: §0.2.1. [20] F. Rømming, J. Otten, and S. B. Holden (2023) Connections: Markov Decision Processes for Classical, Intuitionistic and Modal Connection Calculi. In Proceedings of the 1st International Workshop on Automated Reasoning with Connection Calculi, CEUR Workshop Proceedings, Vol. 3613, p. 107–118. Cited by: §0.3.2. [21] S. Schulz and M. Möhrmann (2016) Performance of Clause Selection Heuristics for Saturation-Based Theorem Proving. In Automated Reasoning, N. Olivetti and A. Tiwari (Eds.), Vol. 9706, p. 330–345. External Links: Document, Link, ISBN 978-3-319-40228-4 978-3-319-40229-1 Cited by: §0.2.1. [22] S. Schulz (2018) Light-weight integration of SAT solving into first-order reasoners: first experiments. In Vampire 2017. Proceedings of the 4th Vampire Workshop, L. Kovács and A. Voronkov (Eds.), EPiC Series in Computing, Vol. 53, p. 9–19. External Links: Document, Link Cited by: §0.2.3. [23] G. Sutcliffe (2017) The TPTP problem library and associated infrastructure: from CNF to TH0, TPTP v6.4.0. Journal of Automated Reasoning 59 (4), p. 483–502. External Links: Document Cited by: §0.3.2, §0.4.2. [24] University of Cambridge Research Computing Services (2026) Ice Lake Nodes. Note: https://docs.hpc.cam.ac.uk/hpc/user-guide/icelake.htmlAccessed 13 May 2026 External Links: Link Cited by: §0.4.1.