A SAT solver which is written in Rust. It is formally verified using Creusot.
It means that it solves the Boolean satisfiability problem (also known as SAT) and that if it states that the formula is satisfiable (SAT), then we know (read: it is proven) that the formula is SAT, and if it states that the formula is unsatisfiable (UNSAT), then we know (read: it is proven) that the formula is UNSAT. Also, the solver is statically proven to be free of runtime panics, which means that it cannot crash.
It currently has the following features:
- Clause analysis with clause learning.
- Unit propagation.
- Two watched literals (2WL) with blocking literals and circular search.
- The variable move-to-front (VMTF) decision heuristic.
- Phase saving.
- Backtracking of the trail to asserting level.
- Exponential moving averages (EMA) based restarts.
- Clause deletion (without garbage collection).
Firstly you'll need to get Rust.
Then afterwards, the solver can be built with:
cargo build
and tested with:
cargo test
and run with
cargo run -- --file [PATH_TO_FILE]
where the provided file must be a correctly formatted DIMACS CNF file.
Remember do add the --release
as in cargo test --release [TEST_TO_RUN]
, otherwise it will be built in debug mode, which is slow.
You'll need to install Creusot. This is best done by following the instructions in the Creusot repository.
Once that is done then you could previously use Cargo Make. That is currently broken, and I have yet to fix it, so you'll for now have to do with cd
ing into the directory of the solver you'd like to verifiy, and then run cargo creusot why3 ide
. After a bit the Why3 IDE should appear. There you'll (hopefully) be able to choose the root note and press 3. If you successfully installed Creusot and the Why3 toolchain then SMT solvers will be dispatched to prove the various Verification Conditions, and at some point everything will be marked with a green checkmark.
CreuSAT is using Cargo Make to make building easier. It can be installed by running:
cargo install --force cargo-make
After installing Cargo Make, simply run:
cargo make prove-CreuSAT
And hopefully the Why3 IDE will appear. If not, then most likely something is not installed or pathed correctly, or I have given the wrong instructions (sorry).
Once you are in the Why3 IDE, you may click "Tools -> Strategies -> PROVE EVERYTHING" (or press 4). This should Just Work™ and have everything proved in ~5 minutes on decently modern hardware (I am using a 2019 MacBook Pro). If you have slower hardware, you may need to tweak why3.conf a bit. Feel free to reach out to me or open an issue if you experience any issues.
The following cargo make
commands are supported:
prove-CreuSAT
/p
: Generate the MLCFG forCreuSAT
and run the Whygs3 IDE.prove-Robinson
: Generate the MLCFG forRobinson
and run the Why3 IDE.prove-Friday
: Generate the MLCFG forFriday
and run the Why3 IDE.clean
: Cleans all generated CFG and Why3 session files.clean-CreuSAT
: Clean just theCreuSAT
files.clean-Robinson
: Clean just theRobinson
files.clean-Friday
: Clean just theFriday
files.
StarExec
: Generate acreusat.zip
file ready to be uploaded to the StarExec clusters.StarExec-JigSAT
: Generate ajigsat.zip
file ready to be uploaded to the StarExec clusters.
There are a bunch of tests in the Creusot repository which I recommend looking at.
You could also check out Friday and Robinson for a couple of verified solvers which are both easier to grok algorithmically and proof-wise.
Oh, and yeah, read the thesis. You don't have to read the whole thing, but it has a pretty good introduction to Creusot, program verification, and SAT solving. At least I think it is pretty good, and I've also gotten feedback from people not all that familiar with these kinds of things that it is fairly accessible.
The interesting stuff:
/SarekSkotåm_thesis.pdf - The thesis itself.
/CreuSAT - The source code for CreuSAT.
/Robinson - A fully verified DPLL-based solver.
/Friday - A fully verified and super naive SAT solver.
The playground stuff:
/NewDB - A playground to be used to iron out the new clause database design.
/JigSAT - An unverified solver based on CreuSAT. Used for experimenting with optimizations.
/Scratch - A (temporary-ish) scratch space which I use to experiment with proof stuff.
The boring stuff:
/mlcfgs - Output directory for generated mlcfg Why3 session files.
/prelude - Copy of prelude from the Creusot directory. Included here to make cargo make
happy.
/tests - Directory for tests.
To cite, you may use the following:
BibLaTeX:
@thesis{skotam_creusat_2022,
title = {{CreuSAT}, Using {Rust} and {Creusot} to create the world’s fastest deductively verified {SAT} solver},
url = {https://www.duo.uio.no/handle/10852/96757},
institution = {University of Oslo},
type = {Master's Thesis},
author = {Skotåm, Sarek Høverstad},
date = {2022},
}
BibTeX:
@mastersthesis{skotam_creusat_2022,
title = {{CreuSAT}, Using {Rust} and {Creusot} to create the world’s fastest deductively verified {SAT} solver},
url = {https://www.duo.uio.no/handle/10852/96757},
school = {University of Oslo},
author = {Skotåm, Sarek Høverstad},
year = {2022},
}