.\" DO NOT MODIFY THIS FILE!  It was generated by help2man 1.49.3.
.TH CRYPTOMINISAT5 "1" "January 2023" "cryptominisat5 5.11.4" "User Commands"
.SH NAME
cryptominisat5 \- manual page for cryptominisat5 5.11.4
.SH DESCRIPTION
USAGE 1: \fI\,/build/cryptominisat\-BygSg2/cryptominisat\-5.11\/\fP.4+dfsg1/cryptominisat5 [options] inputfile [frat\-trim\-file]
USAGE 2: \fI\,/build/cryptominisat\-BygSg2/cryptominisat\-5.11\/\fP.4+dfsg1/cryptominisat5 \fB\-\-preproc\fR 1 [options] inputfile simplified\-cnf\-file
USAGE 2: \fI\,/build/cryptominisat\-BygSg2/cryptominisat\-5.11\/\fP.4+dfsg1/cryptominisat5 \fB\-\-preproc\fR 2 [options] solution\-file
.IP
where input is plain or gzipped DIMACS.
.SS "Main options:"
.TP
\fB\-h\fR [ \fB\-\-help\fR ]
Print simple help
.TP
\fB\-\-hhelp\fR
Print extensive help
.TP
\fB\-v\fR [ \fB\-\-version\fR ]
Print version info
.TP
\fB\-\-verb\fR arg (=1)
[0\-10] Verbosity of solver. 0 = only solution
.TP
\fB\-r\fR [ \fB\-\-random\fR ] arg (=0)
[0..] Random seed
.TP
\fB\-t\fR [ \fB\-\-threads\fR ] arg (=1)
Number of threads
.TP
\fB\-\-maxtime\fR arg
Stop solving after this much time (s)
.TP
\fB\-\-maxconfl\fR arg
Stop solving after this many conflicts
.TP
\fB\-m\fR [ \fB\-\-mult\fR ] arg (=3)
Time multiplier for all simplification cutoffs
.TP
\fB\-\-nextm\fR arg (=1)
Global multiplier when the next inprocessing
should take place
.TP
\fB\-\-memoutmult\fR arg (=1)
Multiplier for memory\-out checks on inprocessing
functions. It limits things such as
clause\-link\-in. Useful when you have limited
memory but still want to do some inprocessing
.SH "SEE ALSO"
The full documentation for
.B cryptominisat5
is maintained as a Texinfo manual.  If the
.B info
and
.B cryptominisat5
programs are properly installed at your site, the command
.IP
.B info cryptominisat5
.PP
should give you access to the complete manual.