Preprocessing and simplification

MiniSat includes powerful preprocessing techniques that can dramatically reduce problem size and solving time. These techniques are available through the SimpSolver class.

SimpSolver overview

The simplifying solver extends the base solver with preprocessing capabilities:

#include "minisat/simp/SimpSolver.h"

Minisat::SimpSolver solver;

// Add clauses...

// Solve with preprocessing (default)
bool result = solver.solve();

SimpSolver is a drop-in replacement for Solver. All base functionality remains available.

Variable elimination

Variable elimination removes variables by bounded resolution, potentially simplifying the formula.

How it works

For a variable x appearing in clauses:

Compute all resolvents between positive and negative occurrences
If total clauses decrease (or increase within bounds), eliminate x
Replace all clauses containing x with resolvents
Store elimination information for model reconstruction

Eliminated variables are automatically reconstructed in the model if a solution is found.

Enabling variable elimination

use_elim

boolean

default:"true"

Master switch for variable elimination

solver.use_elim = true;  // Enable (default)
solver.use_elim = false; // Disable

Command-line: -elim or -no-elim

Elimination parameters

clause_lim

integer

default:"20"

Maximum resolvent clause lengthRange: -1 (no limit) or positive integerVariables producing resolvents longer than this are not eliminated.

solver.clause_lim = 20;  // Default
solver.clause_lim = -1;  // No limit (may explode)

Command-line: -cl-lim=20

grow

integer

default:"0"

Allowed clause count increaseNumber of additional clauses elimination may produce.

solver.grow = 0;   // Only eliminate if clauses decrease
solver.grow = 10;  // Allow up to 10 new clauses

Command-line: -grow=0

subsumption_lim

integer

default:"1000"

Subsumption check size limitRange: -1 (no limit) or positive integerSkip subsumption checks against clauses larger than this.

solver.subsumption_lim = 1000;  // Default
solver.subsumption_lim = -1;    // Check all clauses

Command-line: -sub-lim=1000

Calling elimination explicitly

Minisat::SimpSolver solver;

// Add all clauses first...

// Perform elimination
bool ok = solver.eliminate();

if (!ok) {
    printf("Unsatisfiable after preprocessing\n");
} else {
    // Solve the simplified problem
    bool result = solver.solve();
}

eliminate

method

Perform variable elimination

bool eliminate(bool turn_off_elim = false)

Returns false if formula becomes unsatisfiable
turn_off_elim: Disable elimination for future calls
Automatically called by solve() unless disabled

Asymmetric branching

Asymmetric branching strengthens clauses by removing literals that are implied by the remaining literals.

use_asymm

boolean

default:"false"

Enable asymmetric branching

solver.use_asymm = true;  // Enable
solver.use_asymm = false; // Disable (default)

Command-line: -asymm or -no-asymm

Asymmetric branching is expensive. Enable only for hard instances where preprocessing is critical.

Example

Given clause (a ∨ b ∨ c) and formula implying (¬a ∧ ¬b) → ¬c: Asymmetric branching detects that c is implied by ¬a ∧ ¬b, so the clause can be strengthened to (a ∨ b), removing c.

Subsumption and self-subsuming resolution

Subsumption removes redundant clauses:

Subsumption: Clause C₁ subsumes C₂ if C₁ ⊆ C₂. Then C₂ is redundant.
Self-subsuming resolution: Strengthen clauses by resolution when result subsumes original.

use_rcheck

boolean

default:"false"

Check if clauses are already implied

solver.use_rcheck = true;  // Enable
solver.use_rcheck = false; // Disable (default)

Command-line: -rcheck or -no-rcheck

This is very expensive and mostly subsumed by subsumption checks. Enable only for experimental purposes.

Freezing variables

Prevent specific variables from being eliminated:

Minisat::SimpSolver solver;

Var x = solver.newVar();
Var y = solver.newVar();
Var z = solver.newVar();

// Freeze variable x
solver.setFrozen(x, true);

// x will not be eliminated during preprocessing
solver.eliminate();

// Unfreeze for future eliminations
solver.setFrozen(x, false);

setFrozen

method

Freeze or unfreeze a variable

void setFrozen(Var v, bool b)

v: Variable to freeze
b: true to freeze, false to unfreeze
Frozen variables are never eliminated

Alternative freeze interface

// Freeze multiple variables
solver.freezeVar(x);
solver.freezeVar(y);

// Do something...

// Thaw all frozen variables
solver.thaw();

Freeze output or important variables that must appear in the final model.

Preprocessing workflow

Typical preprocessing workflow with SimpSolver:

#include "minisat/simp/SimpSolver.h"

Minisat::SimpSolver solver;

// Configure preprocessing
solver.use_elim = true;
solver.clause_lim = 30;
solver.grow = 5;
solver.use_asymm = false;

// Add all clauses
for (auto& clause : clauses) {
    vec<Lit> lits;
    for (int lit : clause) {
        lits.push(mkLit(abs(lit)-1, lit < 0));
    }
    solver.addClause(lits);
}

// Freeze important variables
for (Var v : output_vars) {
    solver.setFrozen(v, true);
}

printf("Before: %d vars, %d clauses\n", 
       solver.nVars(), solver.nClauses());

// Preprocess
if (!solver.eliminate()) {
    printf("UNSAT after preprocessing\n");
    return;
}

printf("After: %d vars, %d clauses (eliminated %d)\n",
       solver.nVars(), solver.nClauses(), 
       solver.eliminated_vars);

// Solve simplified formula
bool result = solver.solve();

// Model automatically includes eliminated variables
if (result) {
    for (Var v = 0; v < solver.nVars(); v++) {
        printf("v%d = %d\n", v, solver.model[v] == l_True);
    }
}

Controlling solve-time simplification

Control whether solve() performs simplification:

// Solve with simplification (default)
bool result = solver.solve(true, false);

// Solve without simplification
bool result = solver.solve(false, false);

// Solve and turn off simplification permanently
bool result = solver.solve(true, true);

solve

method

Solve with simplification control

bool solve(bool do_simp = true, bool turn_off_simp = false)

do_simp: Perform simplification before solving
turn_off_simp: Disable simplification for future calls

Exporting simplified formulas

Export the simplified formula to DIMACS format:

minisat_simp -dimacs=output.cnf input.cnf

Command-line workflow:

# Simplify without solving
minisat_simp -pre -no-solve -dimacs=simplified.cnf input.cnf

# Solve with external solver
external_solver simplified.cnf

dimacs

string

Output file for simplified formulaIf specified, simplified formula is written in DIMACS format after preprocessing.Command-line: -dimacs=output.cnf

Statistics

Track preprocessing effectiveness:

Minisat::SimpSolver solver;

// Preprocess...
solver.eliminate();

// Check statistics
printf("Eliminated variables: %d\n", solver.eliminated_vars);
printf("Asymmetric literals removed: %d\n", solver.asymm_lits);
printf("Clause merges: %d\n", solver.merges);

eliminated_vars
asymm_lits
merges

Number of variables eliminated through bounded resolution.

Best practices

Use SimpSolver

Always prefer SimpSolver over Solver unless you have specific reasons not to preprocess.

Freeze outputs

Freeze output or interface variables to keep them in the model.

Tune clause limit

Adjust clause_lim based on problem structure. Lower for bounded growth, higher for aggressive elimination.

Disable for incremental

Turn off simplification (turn_off_simp=true) when using incremental solving.

Advanced: Checking elimination status

Minisat::SimpSolver solver;

// After preprocessing...
solver.eliminate();

// Check if specific variable was eliminated
for (Var v = 0; v < solver.nVars(); v++) {
    if (solver.isEliminated(v)) {
        printf("Variable %d was eliminated\n", v);
    }
}

isEliminated

method

Check if a variable was eliminated

bool isEliminated(Var v) const

Returns true if variable v was eliminated during preprocessing.

Performance considerations

Preprocessing is a tradeoff: it takes time upfront but can dramatically reduce solving time.

When preprocessing helps

Structured problems: Industrial instances with many equivalences
Large formulas: Problems where size reduction is significant
Hard instances: When solving time dominates preprocessing time

When to skip preprocessing

Easy problems: Quick solves where preprocessing overhead isn’t worth it
Incremental solving: Adding clauses repeatedly makes preprocessing ineffective
Real-time constraints: When preprocessing time is unacceptable

Garbage collection

Preprocessing can generate memory fragmentation. Control garbage collection:

simp_garbage_frac

double

default:"0.5"

GC trigger threshold during simplification

solver.simp_garbage_frac = 0.5;  // GC at 50% waste (default)
solver.simp_garbage_frac = 0.2;  // GC at 20% waste (more frequent)

Command-line: -simp-gc-frac=0.5

Lower values trigger GC more frequently, reducing memory usage but increasing overhead.

Configuration

All solver configuration options

Performance

Optimize for speed

Get Started

Core Concepts

Advanced Usage

Examples

Preprocessing and simplification

SimpSolver overview

Variable elimination

How it works

Enabling variable elimination

Elimination parameters

Calling elimination explicitly

Asymmetric branching

Example

Subsumption and self-subsuming resolution

Freezing variables

Alternative freeze interface

Preprocessing workflow

Controlling solve-time simplification

Exporting simplified formulas

Statistics

Best practices

Use SimpSolver

Freeze outputs

Tune clause limit

Disable for incremental

Advanced: Checking elimination status

Performance considerations

When preprocessing helps

When to skip preprocessing

Garbage collection

Configuration

Performance

Build docs developers (and LLMs) love

Get Started

Core Concepts

Advanced Usage

Examples

​SimpSolver overview

​Variable elimination

​How it works

​Enabling variable elimination

​Elimination parameters

​Calling elimination explicitly

​Asymmetric branching

​Example

​Subsumption and self-subsuming resolution

​Freezing variables

​Alternative freeze interface

​Preprocessing workflow

​Controlling solve-time simplification

​Exporting simplified formulas

​Statistics

​Best practices

Use SimpSolver

Freeze outputs

Tune clause limit

Disable for incremental

​Advanced: Checking elimination status

​Performance considerations

​When preprocessing helps

​When to skip preprocessing

​Garbage collection

​Related topics

Configuration

Performance

Build docs developers (and LLMs) love

SimpSolver overview

Variable elimination

How it works

Enabling variable elimination

Elimination parameters

Calling elimination explicitly

Asymmetric branching

Example

Subsumption and self-subsuming resolution

Freezing variables

Alternative freeze interface

Preprocessing workflow

Controlling solve-time simplification

Exporting simplified formulas

Statistics

Best practices

Advanced: Checking elimination status

Performance considerations

When preprocessing helps

When to skip preprocessing

Garbage collection

Related topics