by Niklas Eén, Niklas Sörensson
Applications of MiniSat
- Paradox — A Finite Model Finder for First Order Logic
- Translates to SAT, and uses MiniSat as a backend.
- The MathSat page
- A project to build a framework for "Satisfiability Modulo Theories" (SMT), in which MiniSat is used.
- sKizzo — A QBF Solver
- sKizzo is a hybrid QBF solver that uses several techniques
of mainly symbolic, but also search-based nature. MiniSat is
used as a possible backend for propositional reasoning.
- The ARIO SMT Solver
- Another framework for SMT, developed at University of Michigan. MiniSat is rumored to be in there somewhere too.
- DPvis — Visualizing the Davis-Putnam Procedure
- A really cool visualizer for CNFs and for DPLL-search, put on top of MiniSat.
- ABC: A System for Sequential Synthesis and Verification
- Developed by the Berkeley Logic Synthesis and Verification Group. It uses the C version of MiniSat.
- A minisat-based SAT solver for an extension of CNF (with propositional inductive definitions,
aggregates, pseudoboolean constraints).
- IDP — a finite domain model generator for FO(.)
- Propositionalises FO(.) theories (typed first order logic with inductive definitions,
aggregates, bounded arithmetic) and applies minisat(ID).
General SAT related links
- SAT Live
- Currently the most active web forum for SAT.
- The Propositional Satisfiability Web Site
- Contains more links to material, in particular to the SAT conference.