Reset Early, Reset Often, Eliminate Models

Martin S. Fixman; Fredrik Rømming; Sean B. Holden

cs.LOOct 13, 2026

Reset Early, Reset Often, Eliminate Models

Authors: Martin S. Fixman, Fredrik Rømming, Sean B. Holden

Organizations: University of Cambridge, United Kingdom

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.

Figures & tables

Panel of Figure 1 — 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.

Panel of Figure 2 — Figure 2: Example of SATResetCoP on SYN052-1.p . SATCoP and previous provers would backtrack after closing the branch with $F(x_{1})\vee\neg 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.

Panel of Figure 3 — 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 $\leq 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.

Panel of Figure 5 — 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 $\geq 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.

Automated Theorem Proving

Automated theorem proving develops algorithms and AI systems that construct or check formal proofs in mathematics, logic, and software.

See all 152 papers

Tactix: Towards a Programmable Strategy Interface for Flexible SAT Solving
Oct 17, 2026Haoze Wu, André Schidler, Armin Biere +1Boolean Satisfiability
Amherst College, Amherst, MA, USA · University of Freiburg, Freiburg im Breisgau, Germany · Broadcom, Palo Alto, CA, USA
Modal CEGAR-tableaux with RECAR and resolution-based SAT-shortcuts
Jun 30, 2026Rajeev Goré, Cormac KikkertAutomated Theorem Proving Counterexample-Guided Refinement
Faculty of Information Technology, Monash University, Australia · Cormac Kikkert Research
LRAT-Catcher: Importing SAT Solver Certificates into Lean4 by Reflection
Jul 1, 2026Stefan SzeiderLean Theorem Proving Constraint Satisfaction
Algorithms and Complexity Group, TU Wien, Vienna, Austria

Oct 17, 2026J/K move · Enter open · S save

Tactix: Towards a Programmable Strategy Interface for Flexible SAT Solving

Haoze Wu, André Schidler, Armin Biere, Nina Narodytska

Amherst College, Amherst, MA, USA · University of Freiburg, Freiburg im Breisgau, Germany · Broadcom, Palo Alto, CA, USA

Boolean Satisfiability

Open paper AskPDF arXiv

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.

Abstract

Automated Theorem Proving

Explore similar work

Tactix: Towards a Programmable Strategy Interface for Flexible SAT Solving

Modal CEGAR-tableaux with RECAR and resolution-based SAT-shortcuts

LRAT-Catcher: Importing SAT Solver Certificates into Lean4 by Reflection