https://github.com/sarsko/CreuSAT Skip to content Sign up * Product + Features + Mobile + Actions + Codespaces + Packages + Security + Code review + Issues + Integrations + GitHub Sponsors + Customer stories * Team * Enterprise * Explore + Explore GitHub + Learn and contribute + Topics + Collections + Trending + Skills + GitHub Sponsors + Open source guides + Connect with others + The ReadME Project + Events + Community forum + GitHub Education + GitHub Stars program * Marketplace * Pricing + Plans + Compare plans + Contact Sales + Education [ ] * # In this repository All GitHub | Jump to | * No suggested jump to results * # In this repository All GitHub | Jump to | * # In this user All GitHub | Jump to | * # In this repository All GitHub | Jump to | Sign in Sign up {{ message }} sarsko / CreuSAT Public * Notifications * Fork 2 * Star 222 CreuSAT - A formally verified SAT solver written in Rust and verified with Creusot. License MIT license 222 stars 2 forks Star Notifications * Code * Issues 3 * Pull requests 0 * Actions * Projects 0 * Wiki * Security * Insights More * Code * Issues * Pull requests * Actions * Projects * Wiki * Security * Insights sarsko/CreuSAT This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository. master Switch branches/tags [ ] Branches Tags Could not load branches Nothing to show {{ refName }} default View all branches Could not load tags Nothing to show {{ refName }} default View all tags 21 branches 0 tags Code Latest commit @sarsko sarsko Create LICENSE ... 89fed03 Jun 17, 2022 Create LICENSE 89fed03 Git stats * 481 commits Files Permalink Failed to load latest commit information. Type Name Latest commit message Commit time .github/workflows Fix CI once and forall May 31, 2022 CreuSAT Update proof Jun 6, 2022 Friday Slight reorg in Friday Jun 13, 2022 JigSAT Run cargo fmt May 31, 2022 Robinson Some updates to Robinson Jun 11, 2022 mlcfgs Slight reorg in Friday Jun 13, 2022 prelude Add prelude and ide May 30, 2022 tests Port Robinson and Friday to new Creusot May 30, 2022 .gitattributes Update .gitattributes Apr 15, 2022 .gitignore Some updates to Robinson Jun 11, 2022 Cargo.lock Update proof Jun 6, 2022 Cargo.toml Fix merge errors May 28, 2022 LICENSE Create LICENSE Jun 17, 2022 Makefile.toml Revamp the post_unit predicate. Broke a lot of stuff May 31, 2022 README.md Remove trailing \ Jun 17, 2022 SarekSkotam_thesis.pdf Add thesis Jun 16, 2022 ide Add prelude and ide May 30, 2022 rust-toolchain Use new ghost code May 26, 2022 rustfmt.toml Undo single line cargo fmt May 20, 2022 View code [ ] CreuSAT What is this? What does that mean? Ah, nice. What features does it have? How do I run it? How do I prove the solver? Creusot seems really cool! How can I learn it? Overview of the repository README.md CreuSAT What is this? A SAT solver which is written in Rust. It is formally verified using Creusot What does that mean? 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. Ah, nice. What features does it have? 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) How do I run it? 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. How do I prove the solver? I would recommend following the instructions in the Creusot directory for instructions on how to get Why3 and Creusot up and running. To prove it you'll need to do the following: 1. Install Rust 2. Install Creusot. Clone it, and then run cargo install --path creusot. 3. Install Why3. I recommend following the guide in the Creusot repository. 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). If the Why3 IDE appears, then it should work to press 3 and wait a bit. If you are doing the proof from scratch, then you will need to wait a while. The following cargo make commands are supported: * prove-CreuSAT/p : Generate the MLCFG for CreuSAT and run the Why3 IDE. * prove-Robinson : Generate the MLCFG for Friday and run the Why3 IDE. * prove-Friday : Generate the MLCFG for Friday and run the Why3 IDE. * clean : Cleans all generated CFG and Why3 session files. + clean-CreuSAT : Clean just the CreuSAT files. + clean-Robinson : Clean just the Robinson files. + clean-Friday : Clean just the Friday files. * StarExec : Generate a creusat.zip file ready to be uploaded to the StarExec clusters * StarExec-JigSAT : Generate a jigsat.zip file ready to be uploaded to the StarExec clusters Creusot seems really cool! How can I learn it? There are a bunch of tests in the Creusot directory 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. Overview of the repository Overview of the repository: /CreuSAT - The source code for CreuSAT /Friday - A fully verified and super naive SAT solver. /JigSAT - An unverified solver based on CreuSAT. Used for experimenting. /Robinson - A fully verified DPLL-based solver. /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. About CreuSAT - A formally verified SAT solver written in Rust and verified with Creusot. Topics rust proof verification rust-lang formal-methods sat-solver minisat formal-verification sat automated-reasoning satisfiability deductive-reasoning Resources Readme License MIT license Stars 222 stars Watchers 4 watching Forks 2 forks Releases No releases published Packages 0 No packages published Contributors 2 * @sarsko sarsko Sarek Hoverstad Skotam * @xldenis xldenis Xavier Denis Languages * Rust 99.9% * Shell 0.1% * (c) 2022 GitHub, Inc. * Terms * Privacy * Security * Status * Docs * Contact GitHub * Pricing * API * Training * Blog * About You can't perform that action at this time. You signed in with another tab or window. Reload to refresh your session. You signed out in another tab or window. Reload to refresh your session.