DynamicSAT: Dynamic Configuration Tuning for SAT Solving

Official code repository for the paper: DynamicSAT: Dynamic Configuration Tuning for SAT Solving

Abstract

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.

Quick Start

Replace the following parameters in src/dynamicsat.c and src/dynamicsat.h

Implementation

Easy to transfer to other solvers: Find "DynamicSAT" for the DynamicSAT code snippet Add src/dynamicsat.c and src/dynamicsat.h

Reference

Please feel free to insert DynamicSAT into your SAT solver. If DynamicSAT could help your project, please cite our work: