Tactix solver offers flexible programming for advanced SAT solving strategies
Tactix: Towards a Programmable Strategy Interface for Flexible SAT Solving
Logic in Computer ScienceArtificial Intelligence
Summary
SAT solvers are computer programs that try to solve tricky logic puzzles by testing different options. The authors created Tactix, a new solver that clearly separates the core puzzle-solving rules from the strategies used to apply them. This design lets users easily create and test new ways to solve these puzzles without changing the solver’s basic code. Tactix’s default solving approach is faster than current top solvers in many tests, and the authors showed it can be customized to do even better on specific challenging problems.
What this means in practice
- •For software verification teams: Use Tactix’s programmable strategy interface to tailor SAT solving approaches for verifying complex software correctness properties.
- •For hardware design engineers: Customize and test novel SAT solving strategies within Tactix to improve solving efficiency on hardware model checking benchmarks.
Authors
Haoze Wu, André Schidler, Armin Biere, Nina Narodytska
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.