Skip to main content
MiniSat provides extensive configuration options to fine-tune solver behavior. Options can be specified via command-line arguments or programmatically through the API.

​
Command-line options

All command-line options follow the format -option-name=value for valued options or -option-name/-no-option-name for boolean flags.

​
Main options

​
verb
integer
default:"1"
Verbosity level controlling output detail
  • 0: Silent mode (no output)
  • 1: Some output (default)
  • 2: Detailed output with statistics
​
strict
boolean
default:"false"
Validate DIMACS header during parsingEnable with -strict, disable with -no-strict

​
Core solver options

​
var-decay
double
default:"0.95"
Variable activity decay factorRange: (0, 1) (exclusive)Controls how quickly variable activities decay. Higher values (closer to 1) decay more slowly, maintaining variable priorities longer.
​
cla-decay
double
default:"0.999"
Clause activity decay factorRange: (0, 1) (exclusive)Controls how quickly clause activities decay. Affects learned clause deletion strategy.
​
rnd-freq
double
default:"0"
Random variable selection frequencyRange: [0, 1]Probability of choosing a random variable instead of using the activity heuristic. Set to 0 to disable randomization.
​
rnd-seed
double
default:"91648253"
Random seed for variable selectionUsed when rnd-freq > 0 or rnd-init is enabled.
​
ccmin-mode
integer
default:"2"
Conflict clause minimization mode
  • 0: No minimization
  • 1: Basic minimization
  • 2: Deep minimization (default)
Higher values produce smaller learned clauses but require more computation.
​
phase-saving
integer
default:"2"
Phase saving level
  • 0: No phase saving
  • 1: Limited phase saving
  • 2: Full phase saving (default)
Phase saving remembers previous variable assignments to guide future decisions.
​
rnd-init
boolean
default:"false"
Randomize initial variable activitiesWhen enabled, variables start with small random activity values instead of zero.
​
luby
boolean
default:"true"
Use Luby restart sequenceEnable Luby restart sequence instead of geometric sequence. Luby restarts provide theoretical guarantees.
​
rfirst
integer
default:"100"
Base restart intervalRange: [1, INT32_MAX]Number of conflicts before first restart.
​
rinc
double
default:"2"
Restart interval increase factorRange: [1, ∞)For geometric restarts (when Luby is disabled), multiply restart interval by this factor.
​
gc-frac
double
default:"0.20"
Garbage collection memory fractionRange: (0, ∞)Trigger garbage collection when wasted memory exceeds this fraction of total memory.
​
min-learnts
integer
default:"0"
Minimum learned clause limitLower bound on the number of learned clauses to keep.

​
Preprocessing options

These options are only available when using SimpSolver (the simplifying solver).
​
pre
boolean
default:"true"
Enable preprocessingMaster switch for all preprocessing. Disable with -no-pre to skip variable elimination.
​
elim
boolean
default:"true"
Perform variable eliminationEnable bounded variable elimination during preprocessing.
​
asymm
boolean
default:"false"
Shrink clauses by asymmetric branchingMore aggressive preprocessing that can reduce clause sizes.
​
rcheck
boolean
default:"false"
Check if clauses are already implied
This option is costly and subsumes subsumption checks.
​
grow
integer
default:"0"
Clause growth limit for eliminationAllow variable elimination to increase total clause count by this amount.
​
cl-lim
integer
default:"20"
Resolvent clause length limitRange: [-1, INT32_MAX] (-1 means no limit)Variables are not eliminated if resulting resolvent exceeds this length.
​
sub-lim
integer
default:"1000"
Subsumption check size limitRange: [-1, INT32_MAX] (-1 means no limit)Skip subsumption checks against clauses larger than this.
​
simp-gc-frac
double
default:"0.5"
Garbage collection fraction during simplificationSeparate GC threshold used during preprocessing phase.

​
Programmatic configuration

You can configure the solver through the API by setting public member variables: 
#include "minisat/core/Solver.h"

Minisat::Solver solver;

// Configure restart strategy
solver.luby_restart = true;
solver.restart_first = 100;
solver.restart_inc = 2.0;

// Configure phase saving
solver.phase_saving = 2;

// Configure variable/clause decay
solver.var_decay = 0.95;
solver.clause_decay = 0.999;

// Configure conflict clause minimization
solver.ccmin_mode = 2;

// Add clauses and solve
For preprocessing options, use SimpSolver instead of Solver:
#include "minisat/simp/SimpSolver.h"

Minisat::SimpSolver solver;
solver.use_elim = true;
solver.clause_lim = 20;

​
Option categories

Options are organized into logical categories:
Control how the solver makes branching decisions:
  • var-decay: Variable activity decay
  • rnd-freq: Random decision frequency
  • phase-saving: Remember previous assignments
  • rnd-init: Randomize initial activities

​
Best practices

Default settings work well for most problems. Only adjust options if you have specific performance issues or domain knowledge.

​
When to adjust options

  • Industrial instances: Increase phase-saving to 2 (default) for structured problems
  • Random instances: Try phase-saving = 0 and increased rnd-freq
  • Large problems: Increase gc-frac to reduce GC overhead
  • Memory-constrained: Decrease gc-frac and min-learnts

​
Debugging configurations

Increase verbosity to understand solver behavior: 
minisat -verb=2 input.cnf output.txt
This shows:
  • Problem statistics
  • Simplification results
  • Search progress
  • Restart and deletion events

Resource limits

Set CPU and memory constraints

Preprocessing

Deep dive into simplification techniques

Build docs developers (and LLMs) love

Get started for freeTalk to us