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
Figure 1: Tactix system overview with selected interface functions.
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 30s
None
2
Half of the Tier B instances solved within 300s
Tier A
3
PAR-2 ≤1.10× Kissat on Tiers B and C
Tiers A and B
4
Each Tier R instance solved within 1200s ; aggregate runtime ≤1.10× Kissat
B28+C5
5
Each Tier W instance solved within 1200s
B28+C5 and R
6
Selected benchmarks with GF(2) solved within 600s
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 5000s solving-limit boundary; formulas checked by neither are omitted. Points below the diagonal favor Tactix.
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.
Discrete variables are common in many applications, such as probabilistic reasoning, planning and explainable AI. When symbolic reasoning techniques are brought in to bear on these applications, a standard technique for handling discrete variables is to binarize them into Boolean variables to allow the use of Boolean computational machinery such as SAT solvers. This technique can face both computational and semantical challenges though. In this work, we develop a native SAT solver for discrete logic, which is a direct extension of Boolean logic in which variables can take arbitrary values. Our proposed solver has a similar design to Boolean SAT solvers, with ingredients such as unit resolution and clause learning but ones that operate natively on discrete variables. We illustrate the merits of the developed SAT solver by comparing it empirically to CSP solvers applied to discrete CNFs, to Boolean SAT solver applied to binarized CNFs, and to some hybrid solvers.
Yaofang Zhang, Ken Zhou, Adnan Darwiche
Department of Computer Science, University of California, Los Angeles
String constraint solvers are crucial for reasoning about string-manipulating programs. However, many practical string constraints are undecidable, and real-world applications often present complex constraints that challenge current solvers. The rise of multi-core architectures offers an opportunity for parallel solving. A key parallel solving method is cube-and-conquer, in which the quality of splitting heuristics is critical to effectively dividing the search space. Unfortunately, manually designing the heuristics is labor-intensive, and handcrafted heuristics are often sub-optimal. This paper introduces a data-driven approach to automatically generating splitting heuristics. We frame the problem of selecting a splitting atom as a learning task, using features from input formulas and dynamic data from solver execution. We implement this approach in two popular string solvers, Z3seq and Z3str4, demonstrating that the learned heuristics outperform manually designed ones in the number of solved formulas and the average solving time.
Chenhao Gao, Peisen Yao
The State Key Laboratory of Blockchain and Data Security, Zhejiang University Hangzhou, China