Tactix：面向灵活 SAT 求解的可编程策略接口

Tactix 是一个可产出证明的顺序 CDCL SAT 求解器，将证明规则与求解策略解耦，通过公开接口让用户调用技术、观察效果并编写策略。其默认可编程策略在 2024–2026 年 SAT 竞赛基准上优于当前最优求解器，并已用该接口为两个应用领域的困难基准开发新策略，性能超过强基线。作者还以自述形式介绍了 Tactix 背后的 AI 辅助开发过程。