cryptominisat man page

cryptominisat — conflict-driven SAT solver


cryptominisat [Options] <input-file> <output-file>


CryptoMiniSat is a SAT solver, solving problems given in CNF, or conjunctive normal form. CryptoMiniSat retains much of the API of MiniSat, but offers more versatility and better speed on many problems.

The program is a classical conflict-driven solver, with variable activities, clause learning and clause deletion. It however incorporates a number of advanced CNF simplification functionalities which should help the speed of solving. Further, it incorporates some advanced memory-management features that should help in getting the most out of modern CPU caches.

The input format is that of DIMACS CNF, i.e. a header of the form


where VARS is the number of variables, and CLAUSES is the number of clauses in the problem. It then lists the set of clauses such as:

1 -2 0

which is equivalent to the 2-long clause "v1 OR NOT v2 = TRUE"


--polarity-mode = {true,false,rnd,auto} [default: auto]
Selects the polarity mode. Auto is the Jeroslow&Wang method.
--rnd-freq = <num> [0-1] How often should decision variables
be picked randomly.
--verbosity = <num> [0-2] Verbosity 1 is default. Verbosity 0
only prints the results, and verbosity 2 prints many useful debug info.
--randomize = <seed> [0 - 2^32-1]
Sets the random seed, used for picking decision variables (default = 0).
--restrict = <num> [1 - varnum]
When picking random variables to branch on, pick one that is in the num most active vars useful for cryptographic problems, where the question is the key, which is usually small (e.g., 80 bits).
--gaussuntil = <num>
Depth until which Gaussian elimination is active. Giving 0 switches off Gaussian elimination.
--restarts = <num> [1 - 2^32-1]
No more than the given number of restarts will be performed during search.
Don't find and collect >2-long xor-clauses from regular clauses.
Don't find and collect 2-long xor-clauses from regular clauses.
Don't regularly find and collect 2-long xor-clauses from regular clauses.
Do strongly connected component finding using non-existent binary clauses. Makes binary XOR findig slower, but somewhat more accurate.
Don't conglomerate 2 xor clauses when one var is dependent. This allows for elimination of variable y if it is only in the two XOR clauses "y XOR a XOR b" and "y XOR c XOR d"
Don't do regular simplification rounds. These simplification rounds greatly simplify the CNF, but cost time. If your problem is very small, it may be only a waste of time to execute these simplification rounds. Typically, however, these simplification methods save significant amount of time (>60%)
Greedily unbound variables that are not needed for the final satisfying assignement.
Solve at specific c Solver::solve() points in the CNF file. Used to debug file generated by Solver's needLibraryCNFFile() function.
Add new vars at specific c Solver::newVar() points in the CNF file. Used to debug file generated by Solver's needLibraryCNFFile() function.
Don't perform variable replacement. Needed for programmable solver feature.
--restart = {auto, static, dynamic}
Which kind of restart strategy to follow. Default is auto.
--dumplearnts = <filename>
If interrupted or reached restart limit, dump the learnt clauses to the specified file. Maximum size of dumped clauses can be specified with the --maxdumplearnts option.
--maxdumplearnts = [0 - 2^32-1]
When dumping the learnts to file, what should be maximum length of the clause dumped. Useful to make the resulting file smaller. Default is 2^32-1. Note: 2-long XORs are always dumped.
--dumporig = <filename>
If interrupted or reached restart limit, dump the original problem instance, simplified to the current point.
--alsoread = <filename>
Also read this file in. Can be used to re-read dumped learnts, for example.
--maxsolutions = <num>
Search for given amount of solutions. Can only be used in single-threaded mode (--threads=1).
Print average branch depth.
Don't search for failed literals, and don't search for literals propagated both by varX and -varX.
Don't try to minimise XORs by XOR-ing them together. Algorithm as per global/local substitution in Heule's thesis.
Don't do clause subsumption, clause strengthening and variable elimination (implies --novarelim and --nosubsume1).
Don't try to subsume xor-clauses.
Don't print the satisfying assignment if the solution is SAT.
Don't perform variable elimination as per Een and Biere.
Don't perform clause contraction through resolution.
Don't find and solve subroblems with subsolvers.
Don't find distinct matrixes. Put all xors into one big matrix.
Don't order variables in the columns of Gaussian elimination. Effectively disables iterative reduction of the matrix.
Don't reduce iteratively the matrix that is updated.
--maxmatrixrows = [0 - 2^32-1]
Set maximum number of rows for gaussian matrix. Too large matrixes should be discarded for reasons of efficiency. Default: 1000.
--minmatrixrows = [0 - 2^32-1]
Set minimum number of rows for gaussian matrix. Normally, too small matrixes are discarded for reasons of efficiency. Default: 20.
--savematrix = [0 - 2^32-1]
Save matrix every Nth decision level. Default: 2.
--maxnummatrixes = [0 - 2^32-1]
Maximum number of matrixes to treat. Default: 3.
Don't add binary clauses when doing failed lit probing.
Don't remove useless binary clauses.
Don't remove useless learnt binary clauses.
Don't subsume with binary clauses.
Don't subsume with non-existent binary clauses.
Don't perform clause vivification.
Don't sort watches according to size: bin, tri, etc.
Don't do on-the-fly self-subsuming resolution (called 'strong minimisation' in PrecoSat).
Don't calculate reachability and interfere with variable decisions accordingly.
Don't find equivalent literals during failed literal search.
Don't perform recursive/transitive OTF self-subsuming resolution.
Don't cache 1-level equeue. Less memory used, but disables trans OTFSSR, adv. clause vivifier, etc. Throw the clause away on backtrack.
--threads = <num>
Number of threads (default is 1).

Exit Status

The output is a solution, together with some timing information. The exit status indicates the following:

The problem is satisfiable.
The problem's satisfiability was not determined.
The problem is unsatisfiable.


Mate Soos (soos@srlabs.de)

See Also

The DIMACS input format can be looked up here: