Satisfiability modulo theories
Links
- CVC4 - Efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems.
- Z3 - Theorem prover from Microsoft Research. (Programming Z3) (Docs)
- Online Z3 Guide
- Solving Wordle with Z3 (HN)
- Getting Started with Z3
- VPEXPANDB on NEON with Z3 (2022)
- z3.wasm - WASM builds of the Z3 SMT solver.
- Modern SAT solvers: fast, neat and underused (part 3 of N) (HN)
- Set Constraints, Pattern Match Analysis, and SMT (2019)
- Modern SAT solvers: fast, neat and underused (part 1.5 of N) (2019) (HN)
- SATNet - Bridging deep learning and logical reasoning using a differentiable satisfiability solver.
- MC2 - Modular SMT solver in OCaml, based on the MCSat calculus.
- Verifying the DPLL Algorithm in Dafny
- Simple Fixpoint Iteration To Solve Parity Games
- SAT solver written in Rust
- NeuroSAT - Learning a SAT Solver from Single-Bit Supervision.
- CryptoMiniSat SAT solver
- SAT solver on top of regex matcher
- SAT/SMT by Example - Extensive and diverse collection of problems that can be encoded as SAT or SMT problems, and discusses their encodings in detail.
- Kissat SAT Solver (HN)
- Can Computers Solve the Collatz Conjecture? (2020) (Lobsters) (HN)
- SMT Solvers, Integer Linear Programming (2019)
- SBV - SMT Based Verification in Haskell. (Changes)
- A Time Leap Challenge for Sat Solving (2020) (HN)
- Yin-Yang - Tool for stress-testing SMT solvers. (HN) (Code)
- G2SAT: Learning to Generate SAT Formulas
- PySAT - Toolkit for SAT-based prototyping in Python. (Docs)
- ipasir.h - Standard Interface for Incremental Satisfiability Solving.
- microsat
- Saturday - Small SAT solver in Go.
- Kind 2 - Multi-engine, parallel, SMT-based automatic model checker for safety properties of Lustre programs. (Web)
- Sat/SMT by Example (2021)
- Programming in Z3 by learning to think like a compiler (HN)
- Z3 Tutorial
- Fun examples of Z3 (2021)
- Teaching Your SMT Solver Probability Theory (2019)
- dReal - SMT Solver for Nonlinear Theories of Reals. (Web)
- Proof P = NP was accidentally published in TOCT (HN)
- PicoSAT.jl - Julia bindings to the SAT solver picosat.
- Generative Type-Aware Mutation for Testing SMT Solvers (2021) (Tweet)
- Mikino - Simple induction and BMC engine.
- rsmt2 - Generic library to interact with SMT-LIB 2 compliant solvers running in a separate system process, such as Z3 and CVC4.
- SMBC - Experimental model finder/SMT solver for functional programming.
- Cvc5: Versatile and Industrial-Strength SMT Solver (2022)
- JavaSMT - Unified Java API for SMT solvers.
- Yices 2 - Solver for Satisfiability Modulo Theories (SMT) problems. (Web)
- Factorio SAT - Enhancing the Factorio experience with SAT solvers.
- ParaFROST - Parallel SAT Solver with GPU Accelerated Inprocessing.
- DRSAT - Daniel's Rusty SAT solver.
- SATurne - Purely functional verified SAT solver which produces proofs.
- SMT Lean - Tactics for discharging Lean goals into SMT solvers.
- CreuSAT - Formally verified SAT solver written in Rust. (Lobsters)
- CaDiCaL Simplified Satisfiability Solver
- MSAT - OCaml library that features a modular SAT-solver and some extensions (including SMT), derived from Alt-Ergo Zero.
- Pono - Performant, adaptable, and extensible SMT-based model checker implemented in C++.
- Go-Z3 - Go Bindings to the Z3 Theorem Prover.
- Finding JIT Optimizer Bugs using SMT Solvers and Fuzzing (2022) (HN)
- NeuroSAT - Neuro-symbolic approaches to the SAT problem.
- Kissat SAT Solver - Keep it simple and clean bare metal SAT solver in C.
- Why SAT Is Hard (2023)
- Checking Firewall Equivalence with Z3 (2018) (Lobsters)
- The Silent (R)evolution of SAT (2023) (HN)
- Modern SAT solvers: fast, neat and underused (2018) (HN)
- easy-smt - Easy way to interact with an SMT solver.
- GPU accelerated SMT constraint solving (2021)
- A new memory-safe SAT solver for package management in Rust (port of libsolv) (2023)