This directory contains all solver implementations used in the experimental section of our paper "Not All Restarts Are Equal: MAB-Learning at the Right Time Scale for SAT".
Each subdirectory and bin file in "src" and "bin" corresponds to a solver variant, with both their name matching the experiment configurations in the paper.
- AE_kissat_MAB (DV_AE): https://satcompetition.github.io/2025/downloads/solvers/main/AE_kissat2025_MAB.tar.xz
- Kissat 4.0.2 (referred as 'VSIDS' in our experiments result description): https://github.com/arminbiere/kissat
All solver variants in this directory are based on AE_kissat_MAB, which itself is built upon kissat 4.0.2.
The effective modifications across all variants are limited to heuristic switching rules in stable mode, with the primary changes implemented in restart.c. These modifications do not affect other solving strategies, and all non-related parameters remain consistent across variants.
The benchmark sets used in this paper are obtained from the SAT Competition benchmark database:
SAT Competition Benchmark Database
Specifically, the experiments are conducted on the CNF benchmarks from the SAT Competition tracks of 2023–2025:
-
SAT Competition 2023:
Main Track 2023 (CNF) -
SAT Competition 2024:
Main Track 2024 (CNF) -
SAT Competition 2025:
Main Track 2025 (CNF)
To build and a solver from source code, enter its directory and run:
cd src/<solver_name>
./build.sh
./build/kissat <cnf_file> [proof_file]To run pre-build solvers in 'bin':
chmod +x ./bin/<solver_bin>
./bin/<solver_bin> <cnf_file> [proof_file]Binaries are available in the bin/ directory after built.