2026-07-24T03:27:53Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:23895 2025-11-12T13:11:08Z ddc:004 open_access

DynamicSAT: Dynamic Configuration Tuning for SAT Solving Shi, Zhengyuan Jiang, Wentao Zhang, Xindi Luo, Jin Liang, Yun Chu, Zhufei Xu, Qiang Boolean satisfiability problem configuration tuning multi-armed bandit Boolean Satisfiability (SAT) problem serves as a foundation for solving numerous real-world challenges. As problem complexity increases, so does the demand for sophisticated SAT solvers, which incorporate a variety of heuristics tailored to optimize performance for specific problem instances. However, a major limitation persists: a configuration that performs well on one instance may lead to inefficiencies on others. While previous approaches to automatic algorithm configuration set parameters prior to runtime, they fail to adapt to the dynamic evolution of problem characteristics during the solving process. We introduce DynamicSAT, a novel SAT solver framework that dynamically tunes configuration parameters during solving process. By adjusting parameters on-the-fly, DynamicSAT adapts to changes arising from clause learning, elimination, and other transformations, thus improving efficiency and robustness across diverse SAT instances. We demonstrate that DynamicSAT achieves significant performance gains over the state-of-the-art solver on 2024 SAT Competition Benchmark. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Zhengyuan Shi and Wentao Jiang and Xindi Zhang and Jin Luo and Yun Liang and Zhufei Chu and Qiang Xu 2025 Is Part Of LIPIcs, Volume 340, 31st International Conference on Principles and Practice of Constraint Programming (CP 2025) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CP.2025.34 urn:nbn:de:0030-drops-238952 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2025.34 eng https://creativecommons.org/licenses/by/4.0/legalcode