Tactix: Towards a Programmable Strategy Interface for Flexible SAT Solving
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.
Related
- Error Analysis for Solving Elliptic Interface Problems with Randomized Neural Networks
- Solving the scattering problem for open wave-guide networks, II: Outgoing estimates
- Solving the scattering problem for open wave-guide networks, I: Fundamental solutions and integral equations
- Digital Learning Platforms and Mathematical Problem-Solving Ability: The Moderating Role of Self-Regulated Learning
- The discontinuous Galerkin method for solving the two-dimensional transport equation with distributed-order memory kernel on triangular meshes
BibTeX
@misc{wu2026tactix,
title = {{Tactix: Towards a Programmable Strategy Interface for Flexible SAT Solving}},
author = {Haoze Wu and André Schidler and Armin Biere and Nina Narodytska},
howpublished = {arXiv},
year = {2026},
month = oct,
doi = {10.48550/arxiv.2610.24369},
eprint = {2610.24369},
archivePrefix = {arXiv},
url = {https://arxiv.org/abs/2610.24369},
note = {CC BY-NC-ND 4.0},
}
RIS
TY - UNPB
TI - Tactix: Towards a Programmable Strategy Interface for Flexible SAT Solving
AU - Haoze Wu
AU - André Schidler
AU - Armin Biere
AU - Nina Narodytska
PY - 2026
DA - 2026/10/17
PB - arXiv
DO - 10.48550/arxiv.2610.24369
UR - https://arxiv.org/abs/2610.24369
AB - 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.
ER -