CRYPTOMINISAT5(1)

🫶 CRYPTOMINISAT5(1) 🫶

okay bestie, welcome to the User Commands manual page for cryptominisat5 version 5.17.0. it's giving solver lore, and we're keeping every single detail exactly as the original says. no cap, no skipping 💅

---

✨ NAME ✨

cryptominisat5 — manual page for cryptominisat5 5.17.0. iconic, honestly 🎀

---

🌸 SYNOPSIS 🌸

bestie, here's the whole invocation vibe, copied exactly so nothing gets lost:

cryptominisat [--help] [--version] [--xlrup {1,2}] [--maxtime VAR]
[--maxconfl VAR] [--threads VAR] [--maxsol VAR] [--polar VAR]
[--nobansol] [--debuglib VAR] [--printsol VAR] [--clearinter VAR]
[--zero-exit-status] [--sampling VAR] [--assump VAR] [--dumpresult VAR]
[--verb VAR] [--prefix VAR] [--seed VAR] [--mult VAR] [--nextm VAR]
[--memoutmult VAR] [--scc VAR] [--restart VAR] [--restartint VAR]
[--restartmargin VAR] [--emagluefast VAR] [--emaglueslow VAR]
[--stabilize VAR] [--stabilizeint VAR] [--stabilizefactor VAR]
[--stabilizemaxint VAR] [--reluctant VAR] [--reluctantmax VAR] [--reduce
VAR] [--reduceint VAR] [--reducetarget VAR] [--reducelow VAR]
[--reducehigh VAR] [--reducerounds VAR] [--reducekeepused VAR]
[--eagersubsume VAR] [--reducetier1glue VAR] [--reducetier2glue VAR]
[--dyntiers VAR] [--flush VAR] [--flushfactor VAR] [--flushint VAR]
[--branchstr VAR] [--sls VAR] [--walknonstable VAR] [--walkseedphase
VAR] [--walkinitially VAR] [--walkxorweight VAR] [--walkmineff VAR]
[--walkmaxeff VAR] [--walkreleff VAR] [--slsmaxmem VAR]
[--ccnrneighmaxsz VAR] [--backboneccnrlim VAR] [--rephase VAR]
[--rephaseint VAR] [--phase VAR] [--lucky VAR] [--target VAR]
[--transred VAR] [--intree VAR] [--fullprobe VAR] [--fullprobemaxm VAR]
[--intreemaxm VAR] [--intreeeff VAR] [--absbudget VAR] [--otfhyper VAR]
[--hyperkeepconfl 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] [--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] [--varelim
VAR] [--varelimto VAR] [--varelimover VAR] [--emptyelim VAR]
[--varelimmaxmb VAR] [--eratio VAR] [--varelimocclim VAR]
[--varelimprodlim VAR] [--varelimschedtouched VAR] [--weakenclsmaxsz
VAR] [--varelimclsmaxsz VAR] [--varelimclslim VAR] [--varelimirregocclim
VAR] [--varelimirregconfl VAR] [--varelimirregunit VAR] [--varelimprod
VAR] [--varelimsum VAR] [--varelimcheckres VAR] [--occrelocatelim VAR]
[--xor VAR] [--maxxorsize VAR] [--xorfindtout VAR] [--maxxormat VAR]
[--gates VAR] [--printgatedot VAR] [--gatefindto VAR] [--recur VAR]
[--moreminim VAR] [--moremoreminim VAR] [--moremorealways VAR]
[--decbased VAR] [--bumpreasondepth VAR] [--shrink VAR] [--otfs VAR]
[--diffdeclevelchrono VAR] [--chronoreusetrail VAR] [--restartreusetrail
VAR] [--verbstat VAR] [--verbrestart VAR] [--verballrestarts VAR]
[--restartprint VAR] [--distill VAR] [--distillbin VAR] [--distillbineff
VAR] [--distillmaxm VAR] [--distillincconf VAR] [--distillminconf VAR]
[--distillredreleff VAR] [--distillirredreleff VAR] [--distillmineffm
VAR] [--distillschedmax VAR] [--distillinst VAR] [--xorgatemaxsize VAR]
[--distillremlevel VAR] [--distillirredalsoremratio VAR]
[--distillirrednoremratio VAR] [--oraclemult VAR] [--oraclegetlearnts
VAR] [--oracleremovedislearnt VAR] [--oraclefindbins VAR] [--congruence
VAR] [--congruenceandsz VAR] [--congruencexorsz VAR] [--sweep VAR]
[--sweeptimelimM VAR] [--sweepeff VAR] [--sweepmineffm VAR] [--sweepvars
VAR] [--sweepclauses VAR] [--sweepdepth VAR] [--sweepfliprounds VAR]
[--renumber VAR] [--mustconsolidate VAR] [--savemem VAR] [--mustrenumber
VAR] [--fullwatchconseveryn VAR] [--strmaxt VAR] [--implicitmanip VAR]
[--implsubsto VAR] [--implstrto VAR] [--cardfind VAR] [--sync VAR]
[--printtimes VAR] [--maxsccdepth VAR] [--maxmatrixrows VAR]
[--maxmatrixcols VAR] [--autodisablegauss VAR] [--minmatrixrows VAR]
[--maxnummatrices VAR] [--gaussusefulcutoff VAR] [--gaussmincalls VAR]
[--gausscheckevery VAR] files

---

💖 DESCRIPTION 💖

okay so this is the part where the manual spills the whole menu. first the positional bit, then every optional argument, with all the defaults, ranges, and nargs details kept exactly as given. it's a lot, but we're not leaving anything out 🦋

🎀 Positional arguments 🎀

• files — input file and proof output (XLRUP by default, see --xlrup) [nargs: 0 or more]

💅 Optional arguments 💅

• -h, --help — shows help message and exits. the classic "bestie, just tell me what to do" move.
• -v, --version — Print version information.
• --xlrup — Encoding of the XLRUP proof, checkable directly by cake_xlrup. 1 = text (cake_xlrup --no-binary), 2 = binary [1..2] [nargs=0..1] [default: 1].
• --maxtime — Stop solving after this much time (s).
• --maxconfl — Stop solving after this many conflicts.
• -t, --threads — Number of threads [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,weight,auto} Selects polarity mode. 'true'/'false' -> always branch positive/negative. 'weight' -> random, biased by the per-variable weight. 'auto' -> CaDiCaL's saved/target/best phases with rephasing [nargs=0..1] [default: "auto"].
• --nobansol — Don't ban the solution once it's found.
• --debuglib — Parse special comments to run solve/simplify during parsing of CNF.
• -s, --printsol — Print assignment if solution is SAT [nargs=0..1] [default: 1].
• --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.
• --sampling — Set sampling vars such as '1,84,44'. Can also be set via CNF using 'c p show 1 84 44 0'.
• --assump — Assumptions file [nargs=0..1] [default: ""].
• --dumpresult — Write solution(s) to this file.
• --verb — [0-10] Verbosity of solver. 0 = only solution [nargs=0..1] [default: 1].
• --prefix — Prefix of every comment line printed [nargs=0..1] [default: "c "].
• -r, --seed — [0..] Random seed [nargs=0..1] [default: 0].
• -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].
• --scc — Find equivalent literals through SCC and replace them [nargs=0..1] [default: 1].
• --restart — Enable restarts [nargs=0..1] [default: 1].
• --restartint — Minimum number of conflicts between restarts [nargs=0..1] [default: 2].
• --restartmargin — Percent the fast glue EMA must be above the slow one to restart [nargs=0..1] [default: 10].
• --emagluefast — Window size of the fast glue EMA [nargs=0..1] [default: 33].
• --emaglueslow — Window size of the slow glue EMA [nargs=0..1] [default: 100000].
• --stabilize — Alternate stable (reluctant doubling) and focused (glue EMA) phases [nargs=0..1] [default: 1].
• --stabilizeint — Length of first stabilizing phase, in conflicts [nargs=0..1] [default: 1000].
• --stabilizefactor — Multiplier of stabilizing phase length at each phase change [nargs=0..1] [default: 2].
• --stabilizemaxint — Maximum stabilizing phase length [nargs=0..1] [default: 2000000000].
• --reluctant — Reluctant doubling base period for stable-phase restarts, 0 = never restart there [nargs=0..1] [default: 1024].
• --reluctantmax — Maximum reluctant doubling period multiplier [nargs=0..1] [default: 1048576].
• --reduce — Enable learnt clause DB reduction [nargs=0..1] [default: 1].
• --reduceint — Base reduce interval, in conflicts [nargs=0..1] [default: 1000].
• --reducetarget — Percent of unused reduce candidates removed per reduce [nargs=0..1] [default: 75].
• --reducelow — Fraction per mille of reduce candidates removed at the first reduce, rising towards --reducehigh as kissat. Set >= reducehigh to use --reducetarget [nargs=0..1] [default: 750].
• --reducehigh — Asymptotic fraction per mille of reduce candidates removed [nargs=0..1] [default: 750].
• --reducerounds — Number of reduces a learnt clause is kept for after it was learnt or last used [nargs=0..1] [default: 2].
• --reducekeepused — Keep every learnt clause used since the last reduce, as CaDiCaL. 0: kissat, tier3 is always a candidate [nargs=0..1] [default: 1].
• --eagersubsume — Demote the last learnt clauses subsumed by a new one, as kissat [nargs=0..1] [default: 1].
• --reducetier1glue — Glue at/below which learnt clauses are kept forever [nargs=0..1] [default: 2].
• --reducetier2glue — Glue at/below which learnt clauses get a double life [nargs=0..1] [default: 6].
• --dyntiers — Recompute tier1/tier2 glue limits from glue usage at each reduce, as kissat [nargs=0..1] [default: 0].
• --flush — Once in a while flush ALL unused redundant clauses [nargs=0..1] [default: 0].
• --flushfactor — Flush interval multiplier [nargs=0..1] [default: 3].
• --flushint — Initial flush interval, in conflicts [nargs=0..1] [default: 100000].
• --branchstr — Branch strategy string that switches between different branch strategies while solving e.g. 'vsids1+vsids2' [nargs=0..1] [default: "vmtf+vsids"].
• --sls — Run local search ('walk') during rephasing [nargs=0..1] [default: 1].
• --walknonstable — Run local search during focused phases too [nargs=0..1] [default: 1].
• --walkseedphase — Start local search off the CDCL phases, as CaDiCaL does [nargs=0..1] [default: 0].
• --walkinitially — Local search rounds to run before simplifying and searching, 0=none [nargs=0..1] [default: 2].
• --walkxorweight — Weight of XOR constraints in yalsat's break values, times 100 (range 0-1000) [nargs=0..1] [default: 500].
• --walkmineff — Minimum local search effort, in yalsat mems [nargs=0..1] [default: 1000000].
• --walkmaxeff — Maximum local search effort, in yalsat mems [nargs=0..1] [default: 100000000].
• --walkreleff — Local search effort per mille of the search propagations done so far [nargs=0..1] [default: 20].
• --slsmaxmem — max MB you're willing to hand the local search solver. If passing the formula over would need more than this, it just... skips local search entirely, no drama 💅 [nargs=0..1] [default: 500]
• --ccnrneighmaxsz — CCNR won't build neighbor edges for clauses longer than this. Why? because the neighborhood is quadratic in clause size, so one (1) huge clause costs GBs and makes every flip of its vars charge thousands of mems 😭 [nargs=0..1] [default: 256]
• --backboneccnrlim — mems budget, in millions, for each of the CCNR local search tries that pre-filter backbone candidates. Set it too low and no model gets found, which means cadiback is stuck testing every variable 🙈 [nargs=0..1] [default: 300]
• --rephase — turns on resetting the saved phases ✨ [nargs=0..1] [default: 1]
• --rephaseint — rephase interval, in conflicts. The interval grows arithmetically, icon behavior 📈 [nargs=0..1] [default: 1000]
• --phase — default decision polarity [nargs=0..1] [default: 1]
• --lucky — go searching for lucky phases before the CDCL loop even starts 🍀 [nargs=0..1] [default: 1]
• --target — decide on target phases: 0 = never, 1 = stable phases only, 2 = always [nargs=0..1] [default: 1]
• --transred — remove useless binary clauses (transitive reduction), bye bye clutter 🧹 [nargs=0..1] [default: 1]
• --intree — carry out intree-based probing [nargs=0..1] [default: 1]
• --fullprobe — regularly probe both polarities of variables during search [nargs=0..1] [default: 0]
• --fullprobemaxm — time in mega-bogoprops to perform full probing [nargs=0..1] [default: 20]
• --intreemaxm — time in mega-bogoprops to perform intree probing [nargs=0..1] [default: 400]
• --intreeeff — intree probing budget as a fraction of all propagations since its last call [nargs=0..1] [default: 0.8]
• --absbudget — makes intree, distill-bin and irred distill-long budgets absolute instead of relative to search effort [nargs=0..1] [default: false]
• --otfhyper — perform hyper-binary resolution during probing [nargs=0..1] [default: 1]
• --hyperkeepconfl — how many conflicts an unused intree hyper-bin gets kept for before it's dropped [nargs=0..1] [default: 15000]
• --schedsimp — perform simplification rounds. If it's 0, we literally never perform any [nargs=0..1] [default: 1]
• --presimp — perform simplification at the very start [nargs=0..1] [default: 1]
• --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 simplifications 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 [nargs=0..1] [default: "scc-vrepl,sub-impl,occ-backw-sub-str,occ-clean-implicit,occ-sweep,occ-bve,occ-ternary-res,occ-xor,must-scc-vrepl,card-find,cl-consolidate,scc-vrepl,renumber,"]
• --preschedule — schedule for simplification at startup [nargs=0..1] [default: "sub-impl, occ-backw-sub,scc-vrepl,occ-sweep, occ-bve,occ-xor,must-scc-vrepl"]
• --occsimp — perform occurrence-list-based optimisations (variable elimination, subsumption, bounded variable addition...) [nargs=0..1] [default: 1]
• --confbtwsimp — start the 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 the paper 'Look-Ahead Versus Look-Back for Satisfiability Problems' 📚 [nargs=0..1] [default: 100]
• --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 go beyond this many MB [nargs=0..1] [default: 600]
• --occirredmaxmb — don't allow irredundant occur size to go 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 weakening 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: 0]
• --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 the 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]
• --varelimocclim — don't try to eliminate a variable whose more frequent polarity occurs more than this many times. 0 = no limit [nargs=0..1] [default: 0]
• --varelimprodlim — don't try to eliminate a variable whose pos*neg occurrence product is over this [nargs=0..1] [default: 10000]
• --varelimschedtouched — only schedule for elimination the vars whose clauses changed since BVE last looked (CaDiCaL's Flags::elim). 0 = schedule every eligible var [nargs=0..1] [default: 0]
• --weakenclsmaxsz — don't weaken a clause longer than this during BVE. 0 = no limit [nargs=0..1] [default: 0]
• --varelimclsmaxsz — don't try to eliminate a variable that occurs in a clause longer than this. 0 = no limit [nargs=0..1] [default: 0]
• --varelimclslim — maximum resolvent size during BVE, -1 = no limit [nargs=0..1] [default: 100]
• --varelimirregocclim — don't run kitten-based irregular gate finding if the variable has more occurrences than this 🐱 [nargs=0..1] [default: 100]
• --varelimirregconfl — Picosat conflict budget for one irregular gate query during BVE [nargs=0..1] [default: 300]
• --varelimirregunit — turn a one-sided irregular-gate core into a unit instead of a gate [nargs=0..1] [default: 1]
• --varelimprod — weight of pos*neg in the BVE ordering score [nargs=0..1] [default: 1]
• --varelimsum — weight of pos+neg in the BVE ordering score [nargs=0..1] [default: 1]
• --varelimcheckres — BVE should check whether resolvents subsume others and check for exact size increase [nargs=0..1] [default: 0]
• --occrelocatelim — when strengthening removes a literal whose occurrence list is longer than this, move the clause to a new place instead of searching the list [nargs=0..1] [default: 1000]
• --xor — discover long XORs [nargs=0..1] [default: 1]
• --maxxorsize — maximum XOR size to find [nargs=0..1] [default: 12]
• --xorfindtout — time limit for finding XORs [nargs=0..1] [default: 400]
• --maxxormat — maximum matrix size (=num elements) that we should try to echelonize [nargs=0..1] [default: 400]
• --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]
• --bumpreasondepth — bump vars in reasons of learnt clause lits up to this depth. 0 = off [nargs=0..1] [default: 1]
• --shrink — All-UIP shrinking of learnt clauses [nargs=0..1] [default: 1]
• --otfs — on-the-fly strengthening of clauses during conflict analysis [nargs=0..1] [default: 1]
• --diffdeclevelchrono — if the difference in decision level is more than this, perform chronological backtracking instead of non-chronological backtracking. Giving -1 means it's never turned on (overrides '--confltochrono -1' in this case) ⏳ [nargs=0..1] [default: 20]
• --chronoreusetrail — on backjump, only backtrack to the level of the best-ranked var above the jump level [nargs=0..1] [default: 1]
• --restartreusetrail — on restart, keep decisions that would be re-made anyway [nargs=0..1] [default: 1]
• --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]
• --restartprint — prints those little restart status lines at least every N conflicts, so you can watch the solver do its thing [nargs=0..1] [default: 8192]
• --distill — periodically runs clause distillation, like a lil spa day for your clauses ✨ [nargs=0..1] [default: 1]
• --distillbin — same spa day, but specifically for binary clauses [nargs=0..1] [default: 1]
• --distillbineff — how much budget binary clause distillation gets, as a fraction of all propagations since its last call [nargs=0..1] [default: 0.02]
• --distillmaxm — the max number of Mega-bogoprops (~time, bestie, it's a time proxy) to spend on vivifying/distilling long cls by enqueueing and propagating [nargs=0..1] [default: 200]
• --distillincconf — multiplier for the current number of conflicts for OTF distill [nargs=0..1] [default: 0.1]
• --distillminconf — minimum number of conflicts between OTF distill runs [nargs=0..1] [default: 10000]
• --distillredreleff — per-mille of all bogoprops since the last call to spend distilling red cls [nargs=0..1] [default: 70]
• --distillirredreleff — per-mille of all bogoprops since the last call to spend distilling irred cls [nargs=0..1] [default: 30]
• --distillmineffm — the floor of the distill effort reference, measured in mega-bogoprops [nargs=0..1] [default: 10]
• --distillschedmax — max clauses scheduled per distill pass [nargs=0..1] [default: 20000]
• --distillinst — tries to remove the last literal during distillation 👀 [nargs=0..1] [default: 1]
• --xorgatemaxsize — the largest clause XOR-gate finding will consider, before the log2 occurrence cap kicks in [nargs=0..1] [default: 12]
• --distillremlevel — clause removal during distillation. 0 = never, 1 = only on a real conflict, 2 = also when a literal is positively implied [nargs=0..1] [default: 2]
• --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]
• --oraclemult — time multiplier for all oracle-based cutoffs (that's oracle-vivif* and oracle-sparsify*, iykyk) [nargs=0..1] [default: 1]
• --oraclegetlearnts — keeps the clauses the oracle learnt during vivification as redundant clauses [nargs=0..1] [default: 0]
• --oracleremovedislearnt — clauses removed by the oracle get re-added as redundant instead of being deleted [nargs=0..1] [default: 0]
• --oraclefindbins — [0..] effort spent looking for binary clauses during oracle vivification. 0 = off [nargs=0..1] [default: 0]
• --congruence — congruence closure over AND/XOR gates (this is the congruence schedule token, bestie) [nargs=0..1] [default: 1]
• --congruenceandsz — max clause size of AND gates for congruence closure [nargs=0..1] [default: 64]
• --congruencexorsz — max clause size of XOR gates for congruence closure [nargs=0..1] [default: 4]
• --sweep — performs SAT sweeping with kitten (occ-sweep), iconic behaviour honestly [nargs=0..1] [default: 1]
• --sweeptimelimM — tick limit cap for one occ-sweep run, in millions [nargs=0..1] [default: 150]
• --sweepeff — occ-sweep budget as a fraction of all bogoprops since its last call [nargs=0..1] [default: 0.1]
• --sweepmineffm — floor of the occ-sweep budget, in mega-ticks [nargs=0..1] [default: 10]
• --sweepvars — starting number of variables in a sweeping environment [nargs=0..1] [default: 256]
• --sweepclauses — starting number of clauses in a sweeping environment [nargs=0..1] [default: 1024]
• --sweepdepth — starting depth of a sweeping environment [nargs=0..1] [default: 2]
• --sweepfliprounds — rounds of model flipping during sweeping [nargs=0..1] [default: 1]
• --renumber — renumbers variables to increase CPU cache efficiency, lowkey genius [nargs=0..1] [default: 1]
• --mustconsolidate — always consolidate, even if it's not useful. This is used for debugging ONLY 🚨 [nargs=0..1] [default: 0]
• --savemem — saves memory by deallocating variable space after renumbering. Only works if renumbering is active, so no renumber = no savings [nargs=0..1] [default: 1]
• --mustrenumber — treats all renumber strategies as must-renumber [nargs=0..1] [default: 0]
• --fullwatchconseveryn — consolidates 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 — subsumes and strengthens 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 — finds cardinality constraints 🔍 [nargs=0..1] [default: 0]
• --sync — sync threads every N conflicts [nargs=0..1] [default: 7000]
• --printtimes — prints the time each simplification run took. 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: 30000]
• --maxmatrixrows — sets the maximum no. of rows for a gaussian matrix. Too large matrices should be discarded for reasons of efficiency [nargs=0..1] [default: 100000]
• --maxmatrixcols — sets the maximum no. of columns for a gaussian matrix. Too large matrices should be discarded for reasons of efficiency [nargs=0..1] [default: 100000]
• --autodisablegauss — automatically disables gauss when it's performing badly 💀 [nargs=0..1] [default: true]
• --minmatrixrows — sets the minimum no. of rows for a gaussian matrix. Normally, too small matrices are discarded for reasons of efficiency [nargs=0..1] [default: 10]
• --maxnummatrices — maximum number of matrices to treat. [nargs=0..1] [default: 1000000]
• --gaussusefulcutoff — turns off Gauss if less than this many usefulness ratio is recorded [nargs=0..1] [default: 0.1]
• --gaussmincalls — only considers disabling a matrix after this many Gauss calls [nargs=0..1] [default: 200]
• --gausscheckevery — checks whether to disable a matrix every this many conflicts [nargs=0..1] [default: 1024]

---

🌈 SEE ALSO 🌈

So the full documentation for cryptominisat5 is maintained as a Texinfo manual. If info and cryptominisat5 are properly installed at your site, this command:

info cryptominisat5

should give you access to the complete manual. Go off, bestie 📖✨

---

And that's the whole vibe check, fr fr — you made it to the end! 🎀 This gorgeous little page is from cryptominisat5 5.17.0, dated October 2026, and it's giving main character energy in the CRYPTOMINISAT5(1) section. Slay, read the manual, and go solve something iconically 💅💖