table of contents
| CRYPTOMINISAT5(1) | User Commands | CRYPTOMINISAT5(1) |
NAME¶
cryptominisat5 - manual page for cryptominisat5 5.11.4
DESCRIPTION¶
USAGE 1: /build/cryptominisat-BygSg2/cryptominisat-5.11.4+dfsg1/cryptominisat5 [options] inputfile [frat-trim-file] USAGE 2: /build/cryptominisat-BygSg2/cryptominisat-5.11.4+dfsg1/cryptominisat5 --preproc 1 [options] inputfile simplified-cnf-file USAGE 2: /build/cryptominisat-BygSg2/cryptominisat-5.11.4+dfsg1/cryptominisat5 --preproc 2 [options] solution-file
- where input is plain or gzipped DIMACS.
Main options:¶
- -h [ --help ]
- Print simple help
- --hhelp
- Print extensive help
- -v [ --version ]
- Print version info
- --verb arg (=1)
- [0-10] Verbosity of solver. 0 = only solution
- -r [ --random ] arg (=0)
- [0..] Random seed
- -t [ --threads ] arg (=1)
- Number of threads
- --maxtime arg
- Stop solving after this much time (s)
- --maxconfl arg
- Stop solving after this many conflicts
- -m [ --mult ] arg (=3)
- Time multiplier for all simplification cutoffs
- --nextm arg (=1)
- Global multiplier when the next inprocessing should take place
- --memoutmult 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
SEE ALSO¶
The full documentation for cryptominisat5 is maintained as a Texinfo manual. If the info and cryptominisat5 programs are properly installed at your site, the command
- info cryptominisat5
should give you access to the complete manual.
| January 2023 | cryptominisat5 5.11.4 |