cryptominisat man page

cryptominisat — conflict-driven SAT solver

Synopsis

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

Description

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

p cnf VARS CLAUSES

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"

Options

--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.
--nonormxorfind
Don't find and collect >2-long xor-clauses from regular clauses.
--nobinxorfind
Don't find and collect 2-long xor-clauses from regular clauses.
--noregbxorfind
Don't regularly find and collect 2-long xor-clauses from regular clauses.
--doextendedscc
Do strongly connected component finding using non-existent binary clauses. Makes binary XOR findig slower, but somewhat more accurate.
--noconglomerate
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"
--nosimplify
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%)
--greedyunbound
Greedily unbound variables that are not needed for the final satisfying assignement.
--debuglib
Solve at specific c Solver::solve() points in the CNF file. Used to debug file generated by Solver's needLibraryCNFFile() function.
--debugnewvar
Add new vars at specific c Solver::newVar() points in the CNF file. Used to debug file generated by Solver's needLibraryCNFFile() function.
--novarreplace
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).
--pavgbranch
Print average branch depth.
--nofailedlit
Don't search for failed literals, and don't search for literals propagated both by varX and -varX.
--noheuleprocess
Don't try to minimise XORs by XOR-ing them together. Algorithm as per global/local substitution in Heule's thesis.
--nosatelite
Don't do clause subsumption, clause strengthening and variable elimination (implies --novarelim and --nosubsume1).
--noxorsubs
Don't try to subsume xor-clauses.
--nosolprint
Don't print the satisfying assignment if the solution is SAT.
--novarelim
Don't perform variable elimination as per Een and Biere.
--nosubsume1
Don't perform clause contraction through resolution.
--noparthandler
Don't find and solve subroblems with subsolvers.
--nomatrixfind
Don't find distinct matrixes. Put all xors into one big matrix.
--noordercol
Don't order variables in the columns of Gaussian elimination. Effectively disables iterative reduction of the matrix.
--noiterreduce
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.
--nohyperbinres
Don't add binary clauses when doing failed lit probing.
--noremovebins
Don't remove useless binary clauses.
--noremlbins
Don't remove useless learnt binary clauses.
--nosubswithbins
Don't subsume with binary clauses.
--nosubswithnbins
Don't subsume with non-existent binary clauses.
--noclausevivif
Don't perform clause vivification.
--nosortwatched
Don't sort watches according to size: bin, tri, etc.
--nolfminim
Don't do on-the-fly self-subsuming resolution (called 'strong minimisation' in PrecoSat).
--nocalcreach
Don't calculate reachability and interfere with variable decisions accordingly.
--nobxor
Don't find equivalent literals during failed literal search.
--norecotfssr
Don't perform recursive/transitive OTF self-subsuming resolution.
--nocacheotfssr
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:

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

Author

Mate Soos (soos@srlabs.de)

See Also

The DIMACS input format can be looked up here:

http://www.satcompetition.org/2009/form…

Info

@VERSION@ Mate Soos User Commands