Tactix: Towards a Programmable Strategy Interface for Flexible SAT Solving

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

cs.LOOct 17, 2026

Tactix: Towards a Programmable Strategy Interface for Flexible SAT Solving

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

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

Abstract

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.

Figures & tables

Panel of Figure 1 — Figure 1: Tactix system overview with selected interface functions.

Panel of Figure 2 — Figure 2: The development workflow of Tactix . Correctness and performance tests provide feedback for revising the implementation and its specification.

Milestone	Performance Gate	Regression Tests
1	Each Tier A instance solved within $30\text{\,}\mathrm{s}$	None
2	Half of the Tier B instances solved within $300\text{\,}\mathrm{s}$	Tier A
3	PAR-2 $\leq 1.10\times$ Kissat on Tiers B and C	Tiers A and B
4	Each Tier R instance solved within $1200\text{\,}\mathrm{s}$ ; aggregate runtime $\leq 1.10\times$ Kissat	B28+C5
5	Each Tier W instance solved within $1200\text{\,}\mathrm{s}$	B28+C5 and R
6	Selected benchmarks with GF(2) solved within $600\text{\,}\mathrm{s}$	B28+C5, R, W

Table 1: Development milestones, performance gates, and retained benchmark sets for regression testing.

Tier	#	Use	Source
A	200	milestone 1	simple crafted benchmarks
B	28	milestone 2, regression	SC’23-24, took Kissat 5-30 seconds
C	30	milestone 3, regression	SC’23-24, took Kissat 5-300 seconds
R	50	milestone 4, regression	SC’24-26, hard for Tactix , easy for Kissat
W	100	milestone 5, regression	SC’24-26, uniquely solved by one baseline
D	1,166	final eval.	SC24–26 development milestones

Table 2: Benchmark tiers used during development.

Set	Configuration	Solved	Solved (checked)	SAT	UNSAT	UNSAT (checked)	Average runtime on checked solves (s)	Average PAR-2 (checked) (s)
SC24	Tactix	355	350	167	188	183	331.1	1540
	Satsuma + Kissat	346	339	163	183	176	343.8	1816
	Kissat 4.0.4	326	324	159	167	165	352.4	2185
	LymphoSAT	351	328	169	182	168	269.6	2021
	Kissat-sc2024	327	326	158	169	168	371.3	2153
	AE-Kissat-MAB	330	325	165	165	160	368.6	2174

Table 3: Results on the SC’24-26 benchmark sets (400 each) and their union (1166). Solved, SAT, and UNSAT count solver answers; parenthesized “checked” columns count independently verified solutions.

Figure 3: Cumulative checked-solve counts on the three annual competition sets.

Figure 4: Tactix against a virtual portfolio of Satsuma + Kissat (SK) and LymphoSAT (Lym). For every formula, the portfolio uses the faster checked result of the two solvers.

Figure 5: Solving time of the default strategy implemented over the C interface against the same strategy implemented in C++ on four test sets.

Seed	Tactix			Tactix mi			Kissat 4.0.4
	Solve (s)	Check (s)	Proof (GB)	Solve (s)	Check (s)	Proof (GB)	Solve (s)	Check (s)	Proof (GB)
0	2167.6	8071.6	4.64	823.2	1510.7	1.89	883.1	1828.0	1.96
1	2167.3	8216.7	4.64	826.9	1515.3	1.89	880.6	1829.5	1.96
2	276.3	977.1	0.70	223.9	432.2	0.54	599.2	1284.3	1.53
3	1806.1	5556.7	3.61	277.0	487.2	0.67	342.4	661.6	0.80
4	4373.0	13271.7	7.97	1386.2	3174.2	3.30	6099.0	12462.0	11.64

Table 4: Performance of a specialized Tactix strategy ( Tactix mi ) on the cruxmiter benchmarks.

Configuration	Solved	Runtime (s)	Checked	Check time (s)
Tactix ch	23	8,463	23	26,562
Tactix	23	18,799	23	41,357
Satsuma + Kissat	23	22,121	23	85,165
Kissat 4.0.4	23	21,791	23	34,151

Table 5: Performance of a specialized Tactix strategy ( Tactix ch ) on 23 Chvátal subproblems.

Figure 6: Tactix ch on the 23 Chvátal subproblems. Left and middle: solving time against Tactix and Satsuma + Kissat . Right: proof-checking time against Satsuma + Kissat .

Version	Commit	Day	Solved	Commits	Solver/API lines added / deleted	Test/fuzzing lines added / deleted
1	dcc3e	5	625	47	3,679 / 416	1,726 / 24
2	54629	11	735	131	9,488 / 1,599	3,286 / 225
3	6f44f	34	818	831	48,943 / 24,954	15,295 / 3,150
4	f50e4	71	977	1,003	57,939 / 13,778	37,196 / 1,782
5	0a906	80	979	246	13,282 / 1,383	8,964 / 447
Now	0f7c1	93	1,006	603	84,566 / 17,540	59,077 / 9,253

Table 6: Performance and implementation activity of the evaluated versions. Days are counted from project start. Commits and added/deleted lines cover the interval since the preceding row, or project start.

Figure 7: Performance of the evaluated versions on SAT and UNSAT benchmarks from SC24–26.

Appendix figures & tables6 assets

Supplementary material from the paper’s appendix.

Appendix

Figure 8: Tactix against Satsuma + Kissat on SC24, SC25, and SC26.

Figure 9: Tactix against LymphoSAT on SC24, SC25, and SC26. Circles denote SAT and crosses UNSAT. For a result checked on only one side, the other side is plotted at the

5000\text{\,}\mathrm{s}

solving-limit boundary; formulas checked by neither are omitted. Points below the diagonal favor Tactix.

Configuration	Accepted	Solve total (s)	Check total (s)	Proof (GB)
Tactix	10	15,481.213	51,812.555	31.502
Tactix mi	10	4,859.624	9,634.313	11.607
Kissat 4.0.4	10	16,025.548	33,132.869	32.296

Appendix

Table 7: Aggregate cruxmiter results.

Benchmark	SC	S/U	T	K4	K24	AE	SK	L	V1	V2	V3	V4	V5
00d1f-lec_mult_KvW_12x11.sanitized	24	U	4060/10800	3900/7550	3620/7330	TO	3930/6650 *	3430/45000 *	?	?	?	3880	?
00d5a-st_890_86_9_572.normalised	25	?	TO	TO	TO	TO	TO	TO	?	?	?	?	?
00fd8-2.normalised	25	S	26.3	12.1	11.9	11.8	33	5.57 p	1300	33.1	14.5	12.1	23.9
01198-arles_thres20_p10_r7533	26	U	0.069/0.14	0.01/0.084	0.01/0.084	0.01/0.084	0.117/0.096	0.034/0.026	0.018	0.217	0.018	0.034	0.034
01d6f-lightsout_sat_25_unbounded_direct_planted250_4_sat.sanitized	26	S	0.037	416	420	3280	447	426	1350	503	1590	0.018	0.018
0205e-bp4_CSO_AM_IXA_LP.normalised	25	U	155/818	88.5/681	116/790	76.9/981	120/702	118/5440	1280	724	160	114	161

Appendix

Table 8: Per-instance competition and development results (competition cells: solve/check).

Tier	Benchmark	S/U	C++	C	Tier	Benchmark	S/U	C++	C
A	color-n14-k3-s006.cnf	U	0.009	0.008	A	xor-n56-s001.cnf	U	0.007	0.008
A	color-n15-k4-s007.cnf	U	0.008	0.008	A	xor-n65-s005.cnf	U	0.007	0.008
A	color-n16-k4-s009.cnf	U	0.008	0.008	A	xor-n70-s007.cnf	U	0.007	0.021
A	color-n17-k4-s011.cnf	U	0.008	0.023	A	xor-n71-s011.cnf	U	0.007	0.008
A	color-n18-k3-s010.cnf	U	0.008	0.008	A	xor-n84-s000.cnf	S	0.008	0.008
A	color-n26-k4-s001.cnf	U	0.009	0.01	A	xor-n86-s008.cnf	S	0.007	0.01

Appendix

Table 9: Per-instance interface runtimes (read down each half).

Table 19

Boolean Satisfiability

See all 22 papers

Reset Early, Reset Often, Eliminate Models
Oct 13, 2026Martin S. Fixman, Fredrik Rømming, Sean B. HoldenAutomated Theorem Proving
University of Cambridge, United Kingdom
Dsat: A Native SAT Solver for Discrete Logic
May 10, 2026Yaofang Zhang, Ken Zhou, Adnan DarwicheConstraint Satisfaction Boolean Satisfiability
Department of Computer Science, University of California, Los Angeles
Learning Splitting Heuristics for Parallel String Solvers
Jun 9, 2026Chenhao Gao, Peisen YaoAutomated Algorithm Discovery Automated Heuristic Design
The State Key Laboratory of Blockchain and Data Security, Zhejiang University Hangzhou, China

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

Reset Early, Reset Often, Eliminate Models

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

University of Cambridge, United Kingdom

Automated Theorem Proving

Open paper AskPDF arXiv

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.

Abstract

Boolean Satisfiability

Explore similar work

Reset Early, Reset Often, Eliminate Models

Dsat: A Native SAT Solver for Discrete Logic

Learning Splitting Heuristics for Parallel String Solvers