The SAT Museum - virtual SAT Solver Museum preserves historical SAT solvers

Sep 14, 2026

Uploaded by Grenda

The virtual SAT Solver Museum preserves historical SAT solvers by collecting and porting their source code to modern compilers, then evaluating them on representative benchmarks using consistent hardware. This enables direct comparisons between historic and contemporary solvers under the same experimental conditions. Results indicate a substantial performance improvement over the last 30 years, while also showing that year-to-year gains are often gradual with intermittent larger jumps. The study further analyzes solver progress using competition winners and key legacy solvers across multiple benchmark sets.

LanguageEnglish

CategoryResearch & Report

FormatPDF

Pages16

Reading Time40 min

AccessFree to download

Introduction

Purpose and motivation

SAT competition background and benchmarks

Preliminaries

Core SAT solving concepts

CDCL and DPLL overview

Preprocessing vs inprocessing

The SAT Museum Armin Biere1, * , Mathias Fleury1 , Nils Froleyks2 and MarijnJ.H. Heule3 1 University of Freiburg, Germany 2 Johannes Kepler University Linz, Austria 3 Carnegie Mellon University, Pittsburgh, PA, USA Abstract The virtual SAT Solver Museum is an effort towards preserving historical SAT solvers, by collecting and porting their source code to modern compilers and evaluating them on representative benchmark setson the same hardware. This allows us to compare historic and modern solvers in the same environment. Our results clearly show a remarkable improvement of SAT solver performance in the last 30 years. Keywords Satisfiability, SAT Solvers, SAT Competition 1. Introduction It has been stated that “No major performance breakthrough [happened in SAT solving] in close to two decades”. Notable proponents of this claim are Karem Sakallah at the recent Simons Institute’s seminar in 2023 and Joao Marques-Silva during his invited talk at POS 2019 [1, Slide 12 (or 53 of the total number)] . The SAT Museum exists to document the history of SAT solving and to show in contrast to these claims that indeed “SAT solvers are getting faster and faster”. The SAT Museum is curated by two authors of this paper; Armin Biere and Marijn Heule have put considerable effort into collecting and restoring the SAT solvers that have been published since the first SAT competitions more than two decades ago. Some results of this effort have been presented as a lightening talk at POS’20, as well as in the form of a (comparatively) high-impact tweet with preliminary plots for the SAT Competition 2020 benchmarks on Twitter. Even though a first SAT competition was conducted more than 3 decades ago in 1992 [2], the current regular series of annual SAT competitions was started in 2002 [3] by Laurent Simon and Daniel Le Berre and in most years attracts dozens of SAT solver submissions. The SAT competition provides a fair environment where solvers compete on the same benchmarksand hardware. These competitions have been credited as a main driving force in advancing SAT-solving technology and are a well-recognized show-case with high visibility and impact far beyond the core SAT community. Each year, the benchmark suite consists of a combination of old and new benchmarks. In recent years, at least 75% of the benchmarks were new, and no more than 14 out of 400 originated 14th International Workshop on Pragmatics of SAT (PoS 2023) * Corresponding author. 􀀚 0000-0001-7170-9242 (A. Biere); 0000-0002-1705-3083 (M. Fleury); 0000-0003-3925-3438 (N. Froleyks); 0000-0002-5587-8801 (M. J.H. Heule) © 2023 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0) . CWPEURorkroceshopedings http://ceurISSN 1613-ws-0073.org CEUR Workshop Proceedings ([CEUR-WS.org](CEUR-WS.org)) from the same research group to ensure diversity. For more information on the competition we refer to the yearly SAT competition proceedings, e.g., the SAT Competition 2022 proceedings [4], or to the last article describing the SAT Competition in 2020 [5] . To asses the progress in solver performance, we consider all winning solvers since the SAT Competition 2002, whose code we could find on the SAT Competition website or obtain through personal communication. Note, that there was no requirement to publish source code nor even binaries in earlier incarnations ofthe SAT Competition (Section 3) . Besides providing data on competition winners we also include two historically important solvers: Boehm1, the winner of the first SAT competition in 1992 [2], as well as Grasp [6] from 1997 . We run on the same hardware (from 2016) all collected and patched solvers on six benchmark sets from SAT competitions spanning more than two decades, namely 2002, 2011, 2019, 2020, 2021, and 2022 . We report results on each set separately, in order to address an argument brought forward by Laurent Simon at a re

FAQs

What is the SAT Museum aiming to achieve?

It documents the history of SAT solving and demonstrates, in contrast to earlier claims, that SAT solvers have been getting faster over time.

How does the SAT Museum enable fair comparison across years?

It ports historical solver source code to modern compilers and evaluates all collected solvers on representative benchmark sets using the same hardware environment.

Which solvers and benchmark sets are used to measure progress?

Winning solvers since the SAT Competition 2002 are included, along with historically important solvers such as Boehm1 and Grasp, evaluated on benchmark sets spanning 2002, 2011, 2019, 2020, 2021, and 2022.

Sep 14, 2026

Uploaded by Grenda