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
$ ./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:
$ ./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:
>>> 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:
#include
#include
#include
using std::vector;
using namespace CMSat;
int main()
{
Solver solver;
solver.set_num_threads(4);
vector 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;
}