Newest version HERE.
Build instructions HERE.
Source is available here. File a bug report or create pull requests.
Referencing in Pulibcations
Always reference our SAT 2009 conference paper.
BibTex record HERE.
Features
CryptoMiniSat is a modern, multi-threaded, feature-rich, simplifying SAT solver. Highlights:
- Instance simplification at every point of the search (inprocessing)
- Many configurable parameters to tune to specific need
- Collection of statistical data to sqlite database
- Clean C++ and python interfaces
Techniques Used
Here is a non-exhaustive list of techniques used in CryptoMiniSat 4:
- Variable elimination and replacement, strengthening, subsumption, vivification
- On-the-fly stamping, literal caching, hyper-binary resolution and transitive reduction during failed literal probing
- Bounded variable addition with hack to allow 2-literal diff
- DRAT-based unsatisfiable proof logging
- XOR recovery and manipulation (NOTE: uses the M4RI library that is GPL, if you want LGPL, compile without it)
- Precise time- and memory tracking. No time or memory-outs on weird CNFs
- Precise usefulness tracking of all clauses
- Clause usefulness-based redundant clause removal. Glues are not used by default, but glues are tracked and can be used (command line option)
- Variable renumbering and variable number hiding. Thanks to this, XOR clauses are cut and the added variables are always consistently displayed to the user.
- SQL-based data logging and AJAX-based powerful data display
- And of course many-many more
Use
Command-line use
1 2 3 4 5 6 7 |
$ ./cryptominisat --verb 0 problem.cnf s SATISFIABLE v 1 2 -3 0 $ cat problem.cnf p cnf 3 2 1 2 3 0 -3 0 |
which means that the problem has 3 variables and 2 clauses. The problem is satisfiable and a solution is v1 = True, v2 = True, v3 = False. There are 3 solutions:
1 2 3 4 5 6 7 8 |
$ ./cryptominisat --verb 0 --maxsol 10 problem.cnf s SATISFIABLE v 1 2 -3 0 s SATISFIABLE v 1 -2 -3 0 s SATISFIABLE v -1 2 -3 0 s UNSATISFIABLE |
This lists all the solutions and then finishes with “UNSATISFIABLE” meaning there are certainly no more solutions than those listed.
Python interface
It’s intuitive and fun to use:
1 2 3 4 5 6 7 8 9 10 11 |
>>> from pycryptosat import Solver >>> s = Solver() >>> s.add_clause([-1]) >>> s.add_clause([1, 2]) >>> sat, solution = s.solve() >>> print sat True >>> print solution[1] False >>> print solution[2] True |
C++ interface
Usage is pretty simple, and the header files have been significantly cleaned up:
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 |
#include <cryptominisat4/cryptominisat.h> #include <assert.h> #include <vector> using std::vector; using namespace CMSat; int main() { Solver solver; solver.set_num_threads(4); vector<Lit> clause; //adds "1 0" clause.push_back(Lit(0, false)); solver.add_clause(clause); //adds "-2 0" clause.clear(); clause.push_back(Lit(1, true)); solver.add_clause(clause); //adds "-1 2 3 0" clause.clear(); clause.push_back(Lit(0, true)); clause.push_back(Lit(1, false)); clause.push_back(Lit(2, false)); solver.add_clause(clause); lbool ret = solver.solve(); assert(ret == l_True); assert(solver.get_model()[0] == l_True); assert(solver.get_model()[1] == l_False); assert(solver.get_model()[2] == l_True); return 0; } |