Minisat

Jul 20, 2023

Minimalistic, open-source SAT solver

MiniSat is a minimalistic, open-source SAT solver, developed to help researchers and developers alike to get started on SAT. It is released under the MIT licence, and is currently used in a number of projects.

Some key features of MiniSat

  • Easy to modify. MiniSat is small and well-documented, and possibly also well-designed, making it an ideal starting point for adapting SAT based techniques to domain specific problems.

  • Highly efficient. Winning all the industrial categories of the SAT 2005 competition, MiniSat is a good starting point both for future research in SAT, and for applications using SAT.

  • Designed for integration. MiniSat supports incremental SAT and has mechanisms for adding non-clausal constraints. By virtue of being easy to modify, it is a good choice for integrating as a backend to another tool, such as a model checker or a more generic constraint solver.



Checkout these related ports:
  • Zn_poly - C library for polynomial arithmetic
  • Zimpl - Language to translate the LP models into .lp or .mps
  • Zegrapher - Software for plotting mathematical objects
  • Zarray - Dynamically typed N-D expression system based on xtensor
  • Z3 - Z3 Theorem Prover
  • Yices - SMT solver
  • Yacas - Yet Another Computer Algebra System
  • Xtensor - Multi-dimensional arrays with broadcasting and lazy computing
  • Xtensor-python - Python bindings for xtensor
  • Xtensor-io - Xtensor plugin to read/write images, audio files, numpy npz and HDF5
  • Xtensor-blas - BLAS extension to xtensor
  • Xspread - Spreadsheet program for X and terminals
  • Xppaut - Graphical tool for solving differential equations, etc
  • Xplot - X11 plotting package
  • Xlife++ - XLiFE++ eXtended Library of Finite Elements in C++