SAT Playground
Fun with Boolean SAT
Boolean SAT asks whether there exists an assignment of true/false values that makes a Boolean formula evaluate to true. The goal of this project is to understand SAT solvers more deeply by building them step by step in Rust, then benchmarking them on 100 randomly selected instances from the SAT Competition 2025 main-track benchmark set. All code in this repository was generated with AI coding tools and then iterated through benchmarking, debugging, and cleanup.
Cumulative Solved vs Time
This follows the standard SAT competition style: each curve rises when a solver finishes an instance. Higher and earlier is better. Click a line or legend card to lock focus on that solver, then move the mouse to inspect per-instance results.
Latest Medium PAR-2
Lower is better. This keeps the aggregate PAR-2 comparison visible next to the more familiar cumulative runtime plot.
Solver Information
Brief notes, source links, and the exact benchmark artifacts used to generate the charts for each plotted solver.
Loading chart data…
Local benchmark host: AMD Ryzen 5 5600 (6 cores / 12 threads, 32 MiB L3) with 62 GiB RAM. These site plots use a 16 GB memory limit per solver on this machine; SAT Competition 2025 uses different infrastructure and larger limits.