{"id":"arxiv/2610.24369","url":"https://arxiv.org/abs/2610.24369","tags":["cs.LO","cs.AI","math.LO"],"score":0,"title":"Tactix: Towards a Programmable Strategy Interface for Flexible SAT Solving","domain":"cs.LO","source":"arxiv","authors":["Haoze Wu","André Schidler","Armin Biere","Nina Narodytska"],"reviews":0,"subject":"cs.LO","summary":"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,…","category":"research","comments":0,"disputed":false,"division":"cs","mentions":0,"discussed":0,"published":"2026-10-17","reactions":{}}