---
title: "An Extensible SAT-solver — paper by Eén and Sörensson (2003)"
description: "Beyond the standard features, MiniSat offers an incremental interface: callers can solve sequences of related… Cited by 12 papers here."
authors: ["Niklas Eén", "Niklas Sörensson"]
year: 2003
venue: "SAT 2003, LNCS 2919, 502–518"
source: "http://minisat.se/Papers.html"
doi: "10.1007/978-3-540-24605-3_37"
licence: "author's copy — read only"
summary_licence: "Elamur Cosmic License"
canonical: "https://research.elamur.ai/free/en/papers/een-2003-extensible-sat-solver/"
---
[Elamur Research](https://md.research.elamur.ai/free/en/) · [this page in HTML](https://research.elamur.ai/free/en/papers/een-2003-extensible-sat-solver/)

[home](https://md.research.elamur.ai/free/en/) / [papers](https://md.research.elamur.ai/free/en/papers/) / [2003](https://md.research.elamur.ai/free/en/papers/2003/) / An Extensible SAT-solver

# An Extensible SAT-solver

**Authors:** [Niklas Eén](https://md.research.elamur.ai/free/en/authors/niklas-een/) and Niklas Sörensson · **Year:** 2003 · **Venue:** [SAT 2003, LNCS 2919, 502–518](https://md.research.elamur.ai/free/en/venues/lecture-notes-in-computer-science/) ([Lecture notes in computer science 2003](https://md.research.elamur.ai/free/en/venues/lecture-notes-in-computer-science/2003/)) · **Publisher:** [Springer Science+Business Media](https://md.research.elamur.ai/free/en/publishers/springer-science-business-media/) · **Licence:** author's copy — read only

**Links:** [Publisher's page](https://doi.org/10.1007/978-3-540-24605-3_37) · [PDF](http://minisat.se/downloads/MiniSat.pdf) · [DOI 10.1007/978-3-540-24605-3\_37](https://doi.org/10.1007/978-3-540-24605-3_37) · [OpenAlex](https://openalex.org/W1518705996)

**Citations:** 2,629 citations (OpenAlex, 2026-10-14) · [12](https://md.research.elamur.ai/free/en/papers/een-2003-extensible-sat-solver/cited-by/) in our library, of the 149,439 papers whose bibliographies we read

## Summary
Modern conflict-driven SAT techniques are well described in the literature, but the low-level details needed to implement them were mostly hidden in large solver codebases. That makes building a new solver, or adapting an existing one to a specific domain such as electronic design automation, slow and error-prone. Eén and Sörensson address this gap by presenting MiniSat, a deliberately minimal yet complete and efficient solver. They distilled it from their earlier solvers Satzoo and Satnik. The paper walks through the code in a style readable by C++ or Java programmers. It covers DPLL-style search, clause learning following GRASP, and watched-literal propagation with dynamic variable ordering following Chaff. Beyond the standard features, MiniSat offers an incremental interface: callers can solve sequences of related problems under temporary unit assumptions. It also provides a lightweight hook for adding arbitrary boolean constraint types. The result is a compact, modifiable reference implementation that lets researchers and practitioners build domain-specific SAT extensions quickly.

## Key points
- MiniSat's original C++ source is under 600 lines, excluding comments, and is freely downloadable.
- The API centres on a few calls: `newVar()`, `addClause()`, `simplifyDB()` and `solve(assumptions)`. After a satisfiable run, the model is available in a public vector.
- Solving under unit assumptions is undone after each call. Making the early non-incremental Satzoo comply with this interface required only 5 extra lines of code.
- General constraints plug into all three solver layers: representation, inference (propagation) and search (conflict analysis). Optional undo lists support constraints that must be updated on backtracking.
- An appendix lists Satzoo features omitted from MiniSat. Satzoo won two categories of the SAT 2003 Competition. The omitted features include:
  - an initial burst of random variable orders;
  - a static variable ordering used for at least 5000 conflicts, which the authors consider the most important omission;
  - roughly 1% random branching;
  - equivalent-variable substitution;
  - pseudo-boolean constraints.

*Our summary of the paper, in our own words — not its text. The work belongs to its authors; read it at the links above.*

## Institutions

- [Chalmers University of Technology](https://md.research.elamur.ai/free/en/universities/chalmers-university-of-technology/) — University, Gothenburg, Sweden · 15 works · 3,169 citations

📚 Shelves (3): [🖥️ Computer Science](https://md.research.elamur.ai/free/en/shelves/computer-science/) · 19,503 works · [🧮 Computational Theory and Mathematics](https://md.research.elamur.ai/free/en/shelves/computer-science/computational-theory-and-mathematics/) · 496 works · [🌐 Computer Networks and Communications](https://md.research.elamur.ai/free/en/shelves/computer-science/computer-networks-and-communications/) · 115 works

## Cite

Cite as: Niklas Eén and Niklas Sörensson. 2003. An Extensible SAT-solver. SAT 2003, LNCS 2919, 502–518.

The paper itself, not this page. BibTeX from the library's record of the work.

```bibtex
@inproceedings{een2003extensible,
  title = {{An Extensible SAT-solver}},
  author = {Niklas Eén and Niklas Sörensson},
  booktitle = {SAT 2003, LNCS 2919, 502–518},
  year = {2003},
  doi = {10.1007/978-3-540-24605-3\_37},
  url = {https://doi.org/10.1007/978-3-540-24605-3_37}
}
```

- [← previous Feature-Rich Part-of-Speech Tagging with a Cyclic Dependency Network](https://md.research.elamur.ai/free/en/papers/toutanova-2003-feature-rich-part-speech-tagging/)
- [next → Head-Driven Statistical Models for Natural Language Parsing](https://md.research.elamur.ai/free/en/papers/collins-2003-head-driven-statistical-models-natural/)
- [↑ back to papers of 2003](https://md.research.elamur.ai/free/en/papers/2003/)

*Updated 3 November 2026*