20 lines
1017 B
Plaintext
20 lines
1017 B
Plaintext
MiniSat is a minimalistic, open-source Boolean satisfiability problem
|
|
(SAT) solver, developed to help researchers and developers alike to get
|
|
started on SAT.
|
|
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.
|
|
|
|
The OpenBSD package of MiniSAT installs two binaries:
|
|
minisat = A core version of the solver.
|
|
minisats = An extended solver with simplification capabilities.
|