MINISAT(1)

💖 MINISAT(1) — the minisat page, but make it make sense 💖

okay bestie, sit down, hydrate, because we're reading the minisat manual page together and it's actually SO good. this is from the General Commands Manual section, and it's about a fast and lightweight SAT solver. yes. we're doing boolean satisfiability today. it's giving STEM baddie. 🧚✨

🌸 NAME 🌸

minisat — fast and lightweight SAT solver. that's it, that's the whole name section, she's concise and she knows it 💅

🦋 SYNOPSIS 🦋

minisat [options] input-file result-output-file

okay so here's the deal: minisat takes as input a plain or gzipped DIMACS formatted file. whether that problem is satisfiable gets told to you two ways — through standard output and through the return value. two receipts, one answer. periodt. 🎀

✨ DESCRIPTION ✨

this page documents briefly the minisat command, so don't come for it for being short, it's doing exactly what it promised. 💖

MiniSat is a minimalistic, open-source SAT solver, built to help researchers and developers alike get started on SAT. and babes, she didn't just participate — she won all the industrial categories of the SAT 2005 competition. 👑 iconic behaviour. so MiniSat is a great starting point both for future research in SAT and for applications that use SAT.

now, the science bit, because you deserve to know: even though the satisfiability problem of Boolean formulas (SAT) is NP complete, SAT solvers are often able to decide it in a reasonable time frame. and because every other NP complete problem is reducible to SAT, these solvers have lowkey become a general purpose tool for that whole class of problems. it's giving "one solver to rule them all" energy fr fr. 🔥

🎀 OPTIONS 🎀

one bullet per option, no skipping, we're eating the whole plate:

• --help, --help-verb — shows a summary of the options (and --help-verb gives you the verbose version, because sometimes you want the whole essay 💅).
• -pre, -no-pre — turn preprocessing on (that's the default, bestie) or off.
• -verb {0,1,2} — sets how chatty the informational output is. set it to 0 for silent mode (girl is not talking), defaults to 1.
• -cpu-lim <unsigned> — puts a limit on CPU time in seconds, defaults to 2147483647.
• -mem-lim <unsigned> — puts a limit on memory usage in MB, defaults to 2147483647.
• -dimacs <output-file> — prints the (possibly preprocessed) input problem in DIMACS format and then stops. like, prints and dips. 🫶
• -luby, -no-luby — enable (default) or disable the Luby restart sequence.
• -rnd-init, -no-rnd-init — randomize the initial activity values. defaults to off, so she's predictable unless you ask otherwise.
• -gc-frac <double> — the fraction of wasted memory allowed before a garbage collection gets triggered. non-negative, defaults to 0.2.
• -rinc <double> — the page literally just lists this one with no description, so that's all we got, no cap. 🙈
• -var-decay <double> — variable activity decay factor, 0 <= value <= 1, defaults to 0.95.
• -cla-decay <double> — clause activity decay factor, 0 <= value <= 1, defaults to 0.999.
• -rnd-freq <double> — how often the decision heuristic tries to pick a random variable, 0 <= value <= 1, defaults to 0.
• -rnd-seed <double> — the random seed for random variable selection, non-negative, defaults to 9.16483e+07.
• -phase-saving {0,1,2} — controls the level of phase saving: 0=none, 1=limited, 2=full. defaults to 2 (full send, always).
• -ccmin-mode {0,1,2} — controls conflict clause minimization: 0=none, 1=basic, 2=deep. defaults to 2.
• -rfirst <int> — the base restart interval, positive, defaults to 100.
• -rcheck, -no-rcheck — enable the (costly) or disable the (default) checking for redundant clauses. yes the costly one is opt-in, she's not doing that for free. 💀
• -asymm, -no-asymm — shrink clauses by asymmetric branching. disabled by default.
• -elim, -no-elim — perform variable elimination. enabled by default.
• -simp-gc-frac <double> — the fraction of wasted memory allowed before a garbage collection is triggered during simplification. non-negative, defaults to 0.5.
• -sub-lim <int> — don't check if subsumption is against a clause larger than this value, -1 <= value, defaults to 1000. -1 means no limit.
• -cl-lim <int> — variables are not eliminated if they produce a resolvent with a length above this limit, -1 <= value, defaults to 20. -1 means no limit.
• -grow <int> — number of additional clauses that may be introduced when eliminating a variable. defaults to 0.

🌈 EXIT CODES 🌈

okay this part actually matters, write it down bestie, the vibes are in the numbers:

• 0 — if parsing the command line options fails, usage information is requested, or output of the input problem in DIMACS format succeeds.
• 1 — if interrupted by SIGINT or if an input file cannot be read.
• 3 — if parsing the input fails.
• 10 — if found satisfiable. 🎉
• 20 — if found unsatisfiable.

lowkey obsessed with how 0 covers both "you asked for help" and "you typed it wrong". she contains multitudes.

💜 AUTHOR 💜

minisat was written by Niklas Een, Niklas Sorensson. ✨

this manual page was written by Michael Tautschnig <mt@debian.org>, for the Debian project (but may be used by others). shoutout, we love a documentation queen. 🫶

⭐ SEE ALSO ⭐

nope, there isn't one — this page keeps her circle small. 😌

and that's the whole page, you ate it. 💅✨ this was the minisat manual page, September 3, 2011 edition, bestie — go solve something NP complete, i believe in you. 🎀🦋💖