🔬 microsat

A tiny (microscopic) DPLL SAT-solver written in Rust. This is not meant to be:

1. A particularly fast solver
2. A particularly extensible solver
3. A particularly useful solver

But instead serves as a proof-of-concept for what a small, readable, and understandable DPLL SAT Solver could look like in Rust.

This project originated as a project for Brown's CSCI2951-O Foundations of Prescriptive Analysis.

Authors:

• Rob Scheidegger
• Hammad Izhar

Benchmarks

Although microsat isn't intended to be used as a fast SAT-solver, I felt it appropriate to compare it at a basic level to the project, minisat (a small CDCL SAT solver that disrupted the SAT solver scene many years back). Times were for release-compiled variants of microsat and minisat on the same computer, for all of the examples in examples/cnf:

As you can see, microsat does pretty remarkably well in this benchmark, despite being much smaller than the already small minisat. Further, it is important to note that for any reasonably large instance (eg. larger than the 1040 variable, 3668 clause file in examples/cnf, which is the largest in this benchmark), so in a way, this benchmark is clearly cheating (but fascinating regardless).