--- name: "cryptominisat" section: "1" platform: "linux" package: "cryptominisat" version: "5.11.21+dfsg1-2" release: "Debian 13 (Trixie)" platforms: ["linux"] url: "https://new.carta.tech/cryptominisat5" --- # cryptominisat(1) manual page for cryptominisat5 5.11.21 Part of [cryptominisat5(1)](/cryptominisat5/1.md). ## NAME cryptominisat5 - manual page for cryptominisat5 5.11.21 ## SYNOPSIS **cryptominisat5** \[*--help*\] \[*--version*\] \[*--help VAR*\] \[*--version*\] \[*--verb VAR*\] \[*--maxtime VAR*\] \[*--maxconfl VAR*\] \[*--random VAR*\] \[*--threads VAR*\] \[*--mult VAR*\] \[*--nextm VAR*\] \[*--memoutmult VAR*\] \[*--maxsol VAR*\] \[*--polar VAR*\] \[*--scc VAR*\] \[*--restart VAR*\] \[*--rstfirst VAR*\] \[*--gluehist VAR*\] \[*--lwrbndblkrest VAR*\] \[*--locgmult VAR*\] \[*--ratiogluegeom VAR*\] \[*--blockingglue VAR*\] \[*--gluecut0 VAR*\] \[*--gluecut1 VAR*\] \[*--adjustglue VAR*\] \[*--everylev1 VAR*\] \[*--everylev2 VAR*\] \[*--lev1usewithin VAR*\] \[*--branchstr VAR*\] \[*--nobansol*\] \[*--debuglib VAR*\] \[*--breakid VAR*\] \[*--breakideveryn VAR*\] \[*--breakidmaxlits VAR*\] \[*--breakidmaxcls VAR*\] \[*--breakidmaxvars VAR*\] \[*--breakidtime VAR*\] \[*--breakidcls VAR*\] \[*--breakidmatrix VAR*\] \[*--sls VAR*\] \[*--slstype VAR*\] \[*--slsmaxmem VAR*\] \[*--slseveryn VAR*\] \[*--yalsatmems VAR*\] \[*--walksatruns VAR*\] \[*--slsgetphase VAR*\] \[*--slsccnraspire VAR*\] \[*--slstobump VAR*\] \[*--slstobumpmaxpervar VAR*\] \[*--slsbumptype VAR*\] \[*--transred VAR*\] \[*--intree VAR*\] \[*--intreemaxm VAR*\] \[*--otfhyper VAR*\] \[*--schedsimp VAR*\] \[*--presimp VAR*\] \[*--allpresimp VAR*\] \[*--nonstop VAR*\] \[*--maxnumsimppersolve VAR*\] \[*--schedule VAR*\] \[*--preschedule VAR*\] \[*--occsimp VAR*\] \[*--confbtwsimp VAR*\] \[*--confbtwsimpinc VAR*\] \[*--tern VAR*\] \[*--terntimelim VAR*\] \[*--ternkeep VAR*\] \[*--terncreate VAR*\] \[*--ternbincreate VAR*\] \[*--occredmax VAR*\] \[*--occredmaxmb VAR*\] \[*--occirredmaxmb VAR*\] \[*--strengthen VAR*\] \[*--weakentimelim VAR*\] \[*--substimelim VAR*\] \[*--substimelimbinratio VAR*\] \[*--substimelimlongratio VAR*\] \[*--strstimelim VAR*\] \[*--sublonggothrough VAR*\] \[*--bva VAR*\] \[*--bvaeveryn VAR*\] \[*--bvalim VAR*\] \[*--bva2lit VAR*\] \[*--bvato VAR*\] \[*--varelim VAR*\] \[*--varelimto VAR*\] \[*--varelimover VAR*\] \[*--emptyelim VAR*\] \[*--varelimmaxmb VAR*\] \[*--eratio VAR*\] \[*--varelimcheckres VAR*\] \[*--xor VAR*\] \[*--maxxorsize VAR*\] \[*--xorfindtout VAR*\] \[*--varsperxorcut VAR*\] \[*--maxxormat VAR*\] \[*--forcepreservexors VAR*\] \[*--gates VAR*\] \[*--printgatedot VAR*\] \[*--gatefindto VAR*\] \[*--recur VAR*\] \[*--moreminim VAR*\] \[*--moremoreminim VAR*\] \[*--moremorealways VAR*\] \[*--decbased VAR*\] \[*--updateglueonanalysis VAR*\] \[*--maxgluehistltlimited VAR*\] \[*--diffdeclevelchrono VAR*\] \[*--verbstat VAR*\] \[*--verbrestart VAR*\] \[*--verballrestarts VAR*\] \[*--printsol,s VAR*\] \[*--restartprint VAR*\] \[*--distill VAR*\] \[*--distillbin VAR*\] \[*--distillmaxm VAR*\] \[*--distillincconf VAR*\] \[*--distillminconf VAR*\] \[*--distilltier0ratio VAR*\] \[*--distilltier1ratio VAR*\] \[*--distillirredalsoremratio VAR*\] \[*--distillirrednoremratio VAR*\] \[*--distillshuffleeveryn VAR*\] \[*--distillsort VAR*\] \[*--renumber VAR*\] \[*--mustconsolidate VAR*\] \[*--savemem VAR*\] \[*--mustrenumber VAR*\] \[*--fullwatchconseveryn VAR*\] \[*--strmaxt VAR*\] \[*--implicitmanip VAR*\] \[*--implsubsto VAR*\] \[*--implstrto VAR*\] \[*--cardfind VAR*\] \[*--sync VAR*\] \[*--clearinter VAR*\] \[*--zero-exit-status*\] \[*--printtimes VAR*\] \[*--maxsccdepth VAR*\] \[*--simfrat VAR*\] \[*--sampling VAR*\] \[*--onlysampling*\] \[*--assump VAR*\] \[*--maxmatrixrows VAR*\] \[*--maxmatrixcols VAR*\] \[*--autodisablegauss VAR*\] \[*--minmatrixrows VAR*\] \[*--maxnummatrices VAR*\] \[*--detachxor VAR*\] \[*--useallmatrixes VAR*\] \[*--detachverb VAR*\] \[*--gaussusefulcutoff VAR*\] \[*--dumpresult VAR*\] *files* ## DESCRIPTION A universal, fast SAT solver with XOR and Gaussian Elimination support. Input can be either plain or gzipped DIMACS with XOR extension cryptominisat5 \[options\] inputfile \[frat-file\] ### Positional arguments: - files input file and FRAT output \[nargs: 0 or more\] ### Optional arguments: - **-h**, **--help** shows help message and exits - **-v**, **--version** prints version information and exits - **-h**, **--help** Print extensive help \[nargs=0..1\] \[default: false\] - **-v**, **--version** Print version info - **--verb** \[0-10\] Verbosity of solver. 0 = only solution \[nargs=0..1\] \[default: 1\] - **--maxtime** Stop solving after this much time (s) - **--maxconfl** Stop solving after this many conflicts - **-r**, **--random** \[0..\] Random seed \[nargs=0..1\] \[default: 0\] - **-t**, **--threads** Number of threads \[nargs=0..1\] \[default: 1\] - **-m**, **--mult** Time multiplier for all simplification cutoffs \[nargs=0..1\] \[default: 3\] - **--nextm** Global multiplier when the next inprocessing should take place \[nargs=0..1\] \[default: 1\] - **--memoutmult** 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 \[nargs=0..1\] \[default: 1\] - **--maxsol** Search for given amount of solutions. Thanks to Jannis Harder for the decision-based banning idea \[nargs=0..1\] \[default: 1\] - **--polar** {true,false,rnd,auto,stable} Selects polarity mode. 'true' -\> selects only positive polarity when branching. 'false' -\> selects only negative polarity when branching. 'auto' -\> selects last polarity used (also called 'caching') \[nargs=0..1\] \[default: "auto"\] - **--scc** Find equivalent literals through SCC and replace them \[nargs=0..1\] \[default: 1\] - **--restart** {geom, glue, luby} Restart strategy to follow. \[nargs=0..1\] \[default: "auto"\] - **--rstfirst** The size of the base restart \[nargs=0..1\] \[default: 100\] - **--gluehist** The size of the moving window for short-term glue history of redundant clauses. If higher, the minimal number of conflicts between restarts is longer \[nargs=0..1\] \[default: 50\] - **--lwrbndblkrest** Lower bound on blocking restart **--** don't block before this many conflicts \[nargs=0..1\] \[default: 10000\] - **--locgmult** The multiplier used to determine if we should restart during glue-based restart \[nargs=0..1\] \[default: 0.8\] - **--ratiogluegeom** Ratio of glue vs geometric restarts **--** more is more glue \[nargs=0..1\] \[default: 5\] - **--blockingglue** Do blocking restart for glues \[nargs=0..1\] \[default: 1\] - **--gluecut0** Glue value for lev 0 ('keep') cut \[nargs=0..1\] \[default: 3\] - **--gluecut1** Glue value for lev 1 cut ('give another shot' \[nargs=0..1\] \[default: 6\] - **--adjustglue** If more than this % of clauses is LOW glue (level 0) then lower the glue cutoff by 1 **--** once and never again \[nargs=0..1\] \[default: 0.7\] - **--everylev1** Reduce lev1 clauses every N \[nargs=0..1\] \[default: 10000\] - **--everylev2** Reduce lev2 clauses every N \[nargs=0..1\] \[default: 15000\] - **--lev1usewithin** Learnt clause must be used in lev1 within this timeframe or be dropped to lev2 \[nargs=0..1\] \[default: 70000\] - **--branchstr** Branch strategy string that switches between different branch strategies while solving e.g. 'vsids1+vsids2' \[nargs=0..1\] \[default: "vmtf+vsids"\] - **--nobansol** Don't ban the solution once it's found - **--debuglib** Parse special comments to run solve/simplify during parsing of CNF - **--breakid** Run BreakID to break symmetries. \[nargs=0..1\] \[default: true\] - **--breakideveryn** Run BreakID every N simplification iterations \[nargs=0..1\] \[default: 5\] - **--breakidmaxlits** Maximum number of literals in thousands. If exceeded, BreakID will not run \[nargs=0..1\] \[default: 3500\] - **--breakidmaxcls** Maximum number of clauses in thousands. If exceeded, BreakID will not run \[nargs=0..1\] \[default: 600\] - **--breakidmaxvars** Maximum number of variables in thousands. If exceeded, BreakID will not run \[nargs=0..1\] \[default: 300\] - **--breakidtime** Maximum number of steps taken during automorphism finding. \[nargs=0..1\] \[default: 2000\] - **--breakidcls** Maximum number of breaking clauses per permutation. \[nargs=0..1\] \[default: 50\] - **--breakidmatrix** Detect matrix row interchangability \[nargs=0..1\] \[default: true\] - **--sls** Run SLS during simplification \[nargs=0..1\] \[default: 1\] - **--slstype** Which SLS to run. Allowed values: walksat, yalsat, ccnr, ccnr\_yalsat \[nargs=0..1\] \[default: "ccnr"\] - **--slsmaxmem** Maximum number of MB to give to SLS solver. Doesn't run SLS solver if the memory usage would be more than this. \[nargs=0..1\] \[default: 500\] - **--slseveryn** Run SLS solver every N simplifications only \[nargs=0..1\] \[default: 2\] - **--yalsatmems** Run Yalsat with this many mems\*million timeout. Limits time of yalsat run \[nargs=0..1\] \[default: 10\] - **--walksatruns** Max 'runs' for WalkSAT. Limits time of WalkSAT run \[nargs=0..1\] \[default: 50\] - **--slsgetphase** Get phase from SLS solver, set as new phase for CDCL \[nargs=0..1\] \[default: 1\] - **--slsccnraspire** Turn aspiration on/off for CCANR \[nargs=0..1\] \[default: 1\] - **--slstobump** How many variables to bump in CCNR \[nargs=0..1\] \[default: 100\] - **--slstobumpmaxpervar** How many times to bump an individual variable's activity in CCNR \[nargs=0..1\] \[default: 100\] - **--slsbumptype** How to calculate what variable to bump. 1 = clause-based, 2 = var-flip-based, 3 = var-score-based \[nargs=0..1\] \[default: 6\] - **--transred** Remove useless binary clauses (transitive reduction) \[nargs=0..1\] \[default: 1\] - **--intree** Carry out intree-based probing \[nargs=0..1\] \[default: 1\] - **--intreemaxm** Time in mega-bogoprops to perform intree probing \[nargs=0..1\] \[default: 400\] - **--otfhyper** Perform hyper-binary resolution during probing \[nargs=0..1\] \[default: 1\] - **--schedsimp** Perform simplification rounds. If 0, we never perform any. \[nargs=0..1\] \[default: 1\] - **--presimp** Perform simplification at the very start \[nargs=0..1\] \[default: 0\] - **--allpresimp** Perform simplification at EVERY start **--** only matters in library mode \[nargs=0..1\] \[default: 0\] - **-n**, **--nonstop** Never stop the search() process in class SATSolver \[nargs=0..1\] \[default: 0\] - **--maxnumsimppersolve** Maximum number of simplifiactions to perform for every solve() call. After this, no more inprocessing will take place. \[nargs=0..1\] \[default: 25\] - **--schedule** Schedule for simplification during run - **--preschedule** Schedule for simplification at startup - **--occsimp** Perform occurrence-list-based optimisations (variable elimination, subsumption, bounded variable addition...) \[nargs=0..1\] \[default: 1\] - **--confbtwsimp** Start first simplification after this many conflicts \[nargs=0..1\] \[default: 40000\] - **--confbtwsimpinc** Simp rounds increment by this power of N \[nargs=0..1\] \[default: 1.4\] - **--tern** Perform Ternary resolution \[nargs=0..1\] \[default: true\] - **--terntimelim** Time-out in bogoprops M of ternary resolution as per paper 'Look-Ahead Versus Look-Back for Satisfiability Problems' \[nargs=0..1\] \[default: 100\] - **--ternkeep** Keep ternary resolution clauses only if they are touched within this multiple of 'lev1usewithin' \[nargs=0..1\] \[default: 5\] - **--terncreate** Create only this multiple (of linked in cls) ternary resolution clauses per simp run \[nargs=0..1\] \[default: 0.3\] - **--ternbincreate** Allow ternary resolving to generate binary clauses \[nargs=0..1\] \[default: 0\] - **--occredmax** Don't add to occur list any redundant clause larger than this \[nargs=0..1\] \[default: 50\] - **--occredmaxmb** Don't allow redundant occur size to be beyond this many MB \[nargs=0..1\] \[default: 600\] - **--occirredmaxmb** Don't allow irredundant occur size to be beyond this many MB \[nargs=0..1\] \[default: 2500\] - **--strengthen** Perform clause contraction through self-subsuming resolution as part of the occurrence-subsumption system \[nargs=0..1\] \[default: 1\] - **--weakentimelim** Time-out in bogoprops M of weakeaning used \[nargs=0..1\] \[default: 300\] - **--substimelim** Time-out in bogoprops M of subsumption of long clauses with long clauses, after computing occur \[nargs=0..1\] \[default: 300\] - **--substimelimbinratio** Ratio of subsumption time limit to spend on sub&str long clauses with bin \[nargs=0..1\] \[default: 0.1\] - **--substimelimlongratio** Ratio of subsumption time limit to spend on sub long clauses with long \[nargs=0..1\] \[default: 0.9\] - **--strstimelim** Time-out in bogoprops M of strengthening of long clauses with long clauses, after computing occur \[nargs=0..1\] \[default: 300\] - **--sublonggothrough** How many times go through subsume \[nargs=0..1\] \[default: 1\] - **--bva** Perform bounded variable addition \[nargs=0..1\] \[default: 1\] - **--bvaeveryn** Perform BVA only every N occ-simplify calls \[nargs=0..1\] \[default: 7\] - **--bvalim** Maximum number of variables to add by BVA per call \[nargs=0..1\] \[default: 250000\] - **--bva2lit** BVA with 2-lit difference hack, too. Beware, this reduces the effectiveness of 1-lit diff \[nargs=0..1\] \[default: 1\] - **--bvato** BVA time limit in bogoprops M \[nargs=0..1\] \[default: 50\] - **--varelim** Perform variable elimination as per Een and Biere \[nargs=0..1\] \[default: 1\] - **--varelimto** Var elimination bogoprops M time limit \[nargs=0..1\] \[default: 750\] - **--varelimover** Do BVE until the resulting no. of clause increase is less than X. Only power of 2 makes sense, i.e. 2,4,8... \[nargs=0..1\] \[default: 16\] - **--emptyelim** Perform empty resolvent elimination using bit-map trick \[nargs=0..1\] \[default: 1\] - **--varelimmaxmb** Maximum extra MB of memory to use for new clauses during varelim \[nargs=0..1\] \[default: 1000\] - **--eratio** Eliminate this ratio of free variables at most per variable elimination iteration \[nargs=0..1\] \[default: 1.6\] - **--varelimcheckres** BVE should check whether resolvents subsume others and check for exact size increase \[nargs=0..1\] \[default: 0\] - **--xor** Discover long XORs \[nargs=0..1\] \[default: 1\] - **--maxxorsize** Maximum XOR size to find \[nargs=0..1\] \[default: 7\] - **--xorfindtout** Time limit for finding XORs \[nargs=0..1\] \[default: 400\] - **--varsperxorcut** Number of \_real\_ variables per XOR when cutting them. So 2 will have XORs of size 4 because 1 = connecting to previous, 1 = connecting to next, 2 in the midde. If the XOR is 4 long, it will be just one 4-long XOR, no connectors \[nargs=0..1\] \[default: 2\] - **--maxxormat** Maximum matrix size (=num elements) that we should try to echelonize \[nargs=0..1\] \[default: 400\] - **--forcepreservexors** Force preserving XORs when they have been found. Easier to make sure XORs are not lost through simplifiactions such as strenghtening \[nargs=0..1\] \[default: 1\] - **--gates** Find gates. \[nargs=0..1\] \[default: 0\] - **--printgatedot** Print gate structure regularly to file 'gatesX.dot' \[nargs=0..1\] \[default: 0\] - **--gatefindto** Max time in bogoprops M to find gates \[nargs=0..1\] \[default: 200\] - **--recur** Perform recursive minimisation \[nargs=0..1\] \[default: 1\] - **--moreminim** Perform strong minimisation at conflict gen. \[nargs=0..1\] \[default: 1\] - **--moremoreminim** Perform even stronger minimisation at conflict gen. \[nargs=0..1\] \[default: 2\] - **--moremorealways** Always strong-minimise clause \[nargs=0..1\] \[default: 0\] - **--decbased** Create decision-based conflict clauses when the UIP clause is too large \[nargs=0..1\] \[default: 1\] - **--updateglueonanalysis** Update glues while analyzing \[nargs=0..1\] \[default: 1\] - **--maxgluehistltlimited** Maximum glue used by glue-based restart strategy when populating glue history. \[nargs=0..1\] \[default: 50\] - **--diffdeclevelchrono** Difference in decision level is more than this, perform chonological backtracking instead of non-chronological backtracking. Giving **-1** means it is never turned on (overrides '--confltochrono **-1**' in this case). \[nargs=0..1\] \[default: 20\] - **--verbstat** Change verbosity of statistics at the end of the solving \[0..3\] \[nargs=0..1\] \[default: 2\] - **--verbrestart** Print more thorough, but different stats \[nargs=0..1\] \[default: 0\] - **--verballrestarts** Print a line for every restart \[nargs=0..1\] \[default: 0\] - **--printsol**,s Print assignment if solution is SAT \[nargs=0..1\] \[default: 1\] - **--restartprint** Print restart status lines at least every N conflicts \[nargs=0..1\] \[default: 8192\] - **--distill** Regularly execute clause distillation \[nargs=0..1\] \[default: 1\] - **--distillbin** Regularly execute clause distillation \[nargs=0..1\] \[default: 1\] - **--distillmaxm** Maximum number of Mega-bogoprops(~time) to spend on vivifying/distilling long cls by enqueueing and propagating \[nargs=0..1\] \[default: 20\] - **--distillincconf** Multiplier for current number of conflicts OTF distill \[nargs=0..1\] \[default: 0.1\] - **--distillminconf** Minimum number of conflicts between OTF distill \[nargs=0..1\] \[default: 10000\] - **--distilltier0ratio** How much of tier 0 to distill \[nargs=0..1\] \[default: 10\] - **--distilltier1ratio** How much of tier 1 to distill \[nargs=0..1\] \[default: 0.03\] - **--distillirredalsoremratio** How much of irred to distill when doing also removal \[nargs=0..1\] \[default: 1.2\] - **--distillirrednoremratio** How much of irred to distill when doing no removal \[nargs=0..1\] \[default: 1\] - **--distillshuffleeveryn** Shuffle to-be-distilled clauses every N cases randomly \[nargs=0..1\] \[default: 3\] - **--distillsort** Distill sorting type \[nargs=0..1\] \[default: 1\] - **--renumber** Renumber variables to increase CPU cache efficiency \[nargs=0..1\] \[default: 1\] - **--mustconsolidate** Always consolidate, even if not useful. This is used for debugging ONLY \[nargs=0..1\] \[default: 0\] - **--savemem** Save memory by deallocating variable space after renumbering. Only works if renumbering is active. \[nargs=0..1\] \[default: 1\] - **--mustrenumber** Treat all 'renumber' strategies as 'must-renumber' \[nargs=0..1\] \[default: 0\] - **--fullwatchconseveryn** Consolidate watchlists fully once every N conflicts. Scheduled during simplification rounds. \[nargs=0..1\] \[default: 4000000\] - **--strmaxt** Maximum MBP to spend on distilling long irred cls through watches \[nargs=0..1\] \[default: 20\] - **--implicitmanip** Subsume and strengthen implicit clauses with each other \[nargs=0..1\] \[default: 1\] - **--implsubsto** Timeout (in bogoprop Millions) of implicit subsumption \[nargs=0..1\] \[default: 100\] - **--implstrto** Timeout (in bogoprop Millions) of implicit strengthening \[nargs=0..1\] \[default: 200\] - **--cardfind** Find cardinality constraints \[nargs=0..1\] \[default: 0\] - **--sync** Sync threads every N conflicts \[nargs=0..1\] \[default: 7000\] - **--clearinter** Interrupt threads cleanly, all the time \[nargs=0..1\] \[default: 0\] - **--zero-exit-status** Exit with status zero in case the solving has finished without an issue - **--printtimes** Print time it took for each simplification run. If set to 0, logs are easier to compare \[nargs=0..1\] \[default: 1\] - **--maxsccdepth** The maximum for scc search depth \[nargs=0..1\] \[default: 10000\] - **--simfrat** Simulate FRAT \[nargs=0..1\] \[default: 0\] - **--sampling** Sampling vars, separated by comma \[nargs=0..1\] \[default: ""\] - **--onlysampling** Print and ban(!) solutions' vars only in 'c ind' or as **--sampling** '...' - **--assump** Assumptions file \[nargs=0..1\] \[default: ""\] - **--maxmatrixrows** Set maximum no. of rows for gaussian matrix. Too large matricesshould bee discarded for reasons of efficiency \[nargs=0..1\] \[default: 2000\] - **--maxmatrixcols** Set maximum no. of columns for gaussian matrix. Too large matricesshould bee discarded for reasons of efficiency \[nargs=0..1\] \[default: 1000\] - **--autodisablegauss** Automatically disable gauss when performing badly \[nargs=0..1\] \[default: true\] - **--minmatrixrows** Set minimum no. of rows for gaussian matrix. Normally, too small matrices are discarded for reasons of efficiency \[nargs=0..1\] \[default: 3\] - **--maxnummatrices** Maximum number of matrices to treat. \[nargs=0..1\] \[default: 5\] - **--detachxor** Detach and reattach XORs \[nargs=0..1\] \[default: false\] - **--useallmatrixes** Force using all matrices \[nargs=0..1\] \[default: false\] - **--detachverb** If set, verbosity for XOR detach code is upped, ignoring normal verbosity \[nargs=0..1\] \[default: 0\] - **--gaussusefulcutoff** Turn off Gauss if less than this many usefulenss ratio is recorded \[nargs=0..1\] \[default: 0.2\] - **--dumpresult** Write solution(s) to this file ### Normal run schedules: - Default schedule: scc-vrepl,sub-impl,breakid,occ-backw-sub-str,occ-clean-implicit,occ-bve,occ-bva,occ-ternary-res,occ-xor,card-find,cl-consolidate,scc-vrepl,renumber,bosphorus,louvain-comms - Schedule at startup: sub-impl, occ-backw-sub,scc-vrepl,breakid, occ-bve,occ-xor ## 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.