path: root/src/prop/cryptominisat/man/cryptominisat.1

.TH "CRYPTOMINISAT" "1" "@VERSION@" "Mate Soos" "User Commands"
.SH "NAME"
cryptominisat \- conflict-driven SAT solver
.SH "SYNOPSIS"
.B cryptominisat
[\fIOPTIONS\fP] <\fIinput\-file\fP> <\fIoutput\-file\fP>
.SH "DESCRIPTION"
.PP
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"

.SH "OPTIONS"
.TP
\fB\-\-polarity\-mode\fP = \fI{true,false,rnd,auto}\fP [default: auto]
Selects the polarity mode.  Auto is the Jeroslow&Wang method.
.TP
\fB\-\-rnd\-freq\fP = <\fInum\fP> [0-1] How often should decision variables
be picked randomly.
.TP
\fB\-\-verbosity\fP = <\fInum\fP> [0-2] Verbosity 1 is default. Verbosity 0
only prints the results, and verbosity 2 prints many useful debug info.
.TP
\fB\-\-randomize\fP = <\fIseed\fP> [0 - 2^32-1]
Sets the random seed, used for picking decision variables (default = 0).
.TP
\fB\-\-restrict\fP = <\fInum\fP> [1 - varnum]
When picking random variables to branch on, pick one that is in the \fInum\fP
most active vars useful for cryptographic problems, where the question is the
key, which is usually small (e.g., 80 bits).
.TP
\fB\-\-gaussuntil\fP = <\fInum\fP>
Depth until which Gaussian elimination is active.  Giving 0 switches off
Gaussian elimination.
.TP
\fB\-\-restarts\fP = <\fInum\fP> [1 - 2^32-1]
No more than the given number of restarts will be performed during search.
.TP
\fB\-\-nonormxorfind\fP
Don't find and collect >2-long xor-clauses from regular clauses.
.TP
\fB\-\-nobinxorfind\fP
Don't find and collect 2-long xor-clauses from regular clauses.
.TP
\fB\-\-noregbxorfind\fP
Don't regularly find and collect 2-long xor-clauses from regular clauses.
.TP
\fB\-\-doextendedscc\fP
Do strongly connected component finding using non-existent binary clauses.
Makes binary XOR findig slower, but somewhat more accurate.
.TP
\fB\-\-noconglomerate\fP
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"
.TP
\fB\-\-nosimplify\fP
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%)
.TP
\fB\-\-greedyunbound\fP
Greedily unbound variables that are not needed for the final satisfying
assignement.
.TP
\fB\-\-debuglib\fP
Solve at specific \fBc Solver::solve()\fP points in the CNF file.  Used to
debug file generated by Solver's \fBneedLibraryCNFFile()\fP function.
.TP
\fB\-\-debugnewvar\fP
Add new vars at specific \fBc Solver::newVar()\fP points in the CNF file.
Used to debug file generated by Solver's \fBneedLibraryCNFFile()\fP function.
.TP
\fB\-\-novarreplace\fP
Don't perform variable replacement.  Needed for programmable solver feature.
.TP
\fB\-\-restart\fP = \fI{auto, static, dynamic}\fP
Which kind of restart strategy to follow. Default is \fIauto\fP.
.TP
\fB\-\-dumplearnts\fP = <\fIfilename\fP>
If interrupted or reached restart limit, dump the learnt clauses to the
specified file.  Maximum size of dumped clauses can be specified with the
\fB\-\-maxdumplearnts\fP option.
.TP
\fB\-\-maxdumplearnts\fP = [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.
.TP
\fB\-\-dumporig\fP = <\fIfilename\fP>
If interrupted or reached restart limit, dump the original problem instance,
simplified to the current point.
.TP
\fB\-\-alsoread\fP = <\fIfilename\fP>
Also read this file in.  Can be used to re-read dumped learnts, for example.
.TP
\fB\-\-maxsolutions\fP = <\fInum\fP>
Search for given amount of solutions.  Can only be used in single-threaded
mode (\fB--threads=1\fP).
.TP
\fB\-\-pavgbranch\fP
Print average branch depth.
.TP
\fB\-\-nofailedlit\fP
Don't search for failed literals, and don't search for literals propagated
both by \fIvarX\fP and \fI-varX\fP.
.TP
\fB\-\-noheuleprocess\fP
Don't try to minimise XORs by XOR-ing them together.  Algorithm as per
global/local substitution in Heule's thesis.
.TP
\fB\-\-nosatelite\fP
Don't do clause subsumption, clause strengthening and variable elimination
(implies \fB\-\-novarelim\fP and \fB\-\-nosubsume1\fP).
.TP
\fB\-\-noxorsubs\fP
Don't try to subsume xor-clauses.
.TP
\fB\-\-nosolprint\fP
Don't print the satisfying assignment if the solution is SAT.
.TP
\fB\-\-novarelim\fP
Don't perform variable elimination as per Een and Biere.
.TP
\fB\-\-nosubsume1\fP
Don't perform clause contraction through resolution.
.TP
\fB\-\-noparthandler\fP
Don't find and solve subroblems with subsolvers.
.TP
\fB\-\-nomatrixfind\fP
Don't find distinct matrixes.  Put all xors into one big matrix.
.TP
\fB\-\-noordercol\fP
Don't order variables in the columns of Gaussian elimination.  Effectively
disables iterative reduction of the matrix.
.TP
\fB\-\-noiterreduce\fP
Don't reduce iteratively the matrix that is updated.
.TP
\fB\-\-maxmatrixrows\fP = [0 - 2^32-1]
Set maximum number of rows for gaussian matrix.  Too large matrixes should be
discarded for reasons of efficiency.  Default: 1000.
.TP
\fB\-\-minmatrixrows\fP = [0 - 2^32-1]
Set minimum number of rows for gaussian matrix.  Normally, too small matrixes
are discarded for reasons of efficiency.  Default: 20.
.TP
\fB\-\-savematrix\fP = [0 - 2^32-1]
Save matrix every Nth decision level.  Default: 2.
.TP
\fB\-\-maxnummatrixes\fP = [0 - 2^32-1]
Maximum number of matrixes to treat.  Default: 3.
.TP
\fB\-\-nohyperbinres\fP
Don't add binary clauses when doing failed lit probing.
.TP
\fB\-\-noremovebins\fP
Don't remove useless binary clauses.
.TP
\fB\-\-noremlbins\fP
Don't remove useless learnt binary clauses.
.TP
\fB\-\-nosubswithbins\fP
Don't subsume with binary clauses.
.TP
\fB\-\-nosubswithnbins\fP
Don't subsume with non-existent binary clauses.
.TP
\fB\-\-noclausevivif\fP
Don't perform clause vivification.
.TP
\fB\-\-nosortwatched\fP
Don't sort watches according to size: bin, tri, etc.
.TP
\fB\-\-nolfminim\fP
Don't do on-the-fly self-subsuming resolution (called 'strong minimisation' in
PrecoSat).
.TP
\fB\-\-nocalcreach\fP
Don't calculate reachability and interfere with variable decisions accordingly.
.TP
\fB\-\-nobxor\fP
Don't find equivalent literals during failed literal search.
.TP
\fB\-\-norecotfssr\fP
Don't perform recursive/transitive OTF self-subsuming resolution.
.TP
\fB\-\-nocacheotfssr\fP
Don't cache 1-level equeue.  Less memory used, but disables trans OTFSSR,
adv. clause vivifier, etc.  Throw the clause away on backtrack.
.TP
\fB\-\-threads\fP = <\fInum\fP>
Number of threads (default is 1).
.SH "EXIT STATUS"
.PP
The output is a solution, together with some timing information.
The exit status indicates the following:
.IP 10
The problem is satisfiable.
.IP 15
The problem's satisfiability was not determined.
.IP 20
The problem is unsatisfiable.
.SH AUTHOR
Mate Soos (soos@srlabs.de)
.SH "SEE ALSO"
The DIMACS input format can be looked up here:

http://www.satcompetition.org/2009/format-benchmarks2009.html