Repository files navigation

ASAT solver which is written in Rust.It is formally verified usingCreusot.

It means that it solves theBoolean satisfiability problem (also known as SAT) andthat if it states that the formula is satisfiable (SAT), then weknow (read: it is proven) that the formula is SAT, and if it states that the formulais unsatisfiable (UNSAT), then weknow (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 toget 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 formattedDIMACS CNF file.

Remember do add the--release as incargo test --release [TEST_TO_RUN], otherwise it will be built in debug mode, which isslow.

You'll need to install Creusot. This is best done by following the instructions in theCreusot 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 withcding into the directory of the solver you'd like to verifiy, and then runcargo creusot why3 ide. After a bit the Why3 IDE should appear. There you'll (hopefully) be able to choose the root note and press3. 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 usingCargo 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 press4). 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 tweakwhy3.conf a bit. Feel free to reach out to me or open an issue if you experience any issues.

The followingcargo 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 theCreusot repository which I recommend looking at.

You could also check outFriday andRobinson for a couple of verified solverswhich are both easier to grok algorithmically and proof-wise.

Oh, and yeah, read thethesis. 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 ofprelude from the Creusot directory. Included here to makecargo 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},}