SimpSolver

The SimpSolver class extends the core Solver with variable elimination and formula simplification capabilities. It implements preprocessing techniques including variable elimination, subsumption, and asymmetric branching to simplify the CNF formula before solving.

Constructor and destructor

SimpSolver()

Creates a new simplifying solver instance.

SimpSolver();

~SimpSolver()

Destructor for cleanup.

~SimpSolver();

Problem specification

newVar()

Adds a new variable to the solver.

Var newVar(lbool upol = l_Undef, bool dvar = true);

upol

lbool

default:"l_Undef"

User preferred polarity for the variable.

dvar

bool

default:"true"

Whether the variable should be a decision variable.

return

Var

The newly created variable identifier.

releaseVar()

Releases a variable from the solver.

void releaseVar(Lit l);

Lit

required

The literal to release.

addClause()

Adds a clause to the solver. Multiple overloads available.

bool addClause(const vec<Lit>& ps);
bool addClause(Lit p);
bool addClause(Lit p, Lit q);
bool addClause(Lit p, Lit q, Lit r);
bool addClause(Lit p, Lit q, Lit r, Lit s);

const vec<Lit>&

Vector of literals forming the clause.

Lit

First literal.

Lit

Second literal.

Lit

Third literal.

Lit

Fourth literal.

return

bool

Returns false if the clause makes the formula unsatisfiable, true otherwise.

addEmptyClause()

Adds the empty clause to the solver.

bool addEmptyClause();

return

bool

Returns false (makes the formula unsatisfiable).

addClause_()

Adds a clause without making an internal copy.

bool addClause_(vec<Lit>& ps);

vec<Lit>&

required

Vector of literals that will be modified.

return

bool

Returns false if unsatisfiable, true otherwise.

substitute()

Replaces all occurrences of a variable with a literal.

bool substitute(Var v, Lit x);

Var

required

Variable to replace.

Lit

required

Literal to substitute in place of the variable.

return

bool

Returns false if substitution causes a contradiction, true otherwise.

This operation may cause the formula to become unsatisfiable.

Variable mode

setFrozen()

Sets whether a variable can be eliminated.

void setFrozen(Var v, bool b);

Var

required

Variable to configure.

bool

required

If true, the variable will not be eliminated during preprocessing.

Frozen variables are protected from elimination but can still be assigned and used in solving.

isEliminated()

Checks if a variable has been eliminated.

bool isEliminated(Var v) const;

Var

required

Variable to check.

return

bool

Returns true if the variable has been eliminated, false otherwise.

freezeVar()

Freezes a variable so it will not be eliminated.

void freezeVar(Var v);

Var

required

Variable to freeze.

This is an alternative interface to setFrozen() that only freezes variables.

thaw()

Thaws all frozen variables.

void thaw();

After calling this method, previously frozen variables may be eliminated in subsequent simplification.

Solving

solve()

Searches for a satisfying assignment with optional simplification.

bool solve(bool do_simp = true, bool turn_off_simp = false);
bool solve(Lit p, bool do_simp = true, bool turn_off_simp = false);
bool solve(Lit p, Lit q, bool do_simp = true, bool turn_off_simp = false);
bool solve(Lit p, Lit q, Lit r, bool do_simp = true, bool turn_off_simp = false);
bool solve(const vec<Lit>& assumps, bool do_simp = true, bool turn_off_simp = false);

Lit

First assumption literal.

Lit

Second assumption literal.

Lit

Third assumption literal.

assumps

const vec<Lit>&

Vector of assumption literals.

do_simp

bool

default:"true"

Whether to perform simplification before solving.

turn_off_simp

bool

default:"false"

Whether to disable simplification after this solve call.

return

bool

Returns true if satisfiable, false otherwise.

Setting do_simp=true will run variable elimination and other preprocessing techniques before the main search.

solveLimited()

Searches with resource constraints and optional simplification.

lbool solveLimited(const vec<Lit>& assumps, bool do_simp = true, bool turn_off_simp = false);

assumps

const vec<Lit>&

required

Vector of assumption literals.

do_simp

bool

default:"true"

Whether to perform simplification.

turn_off_simp

bool

default:"false"

Whether to disable simplification after this call.

return

lbool

Returns l_True if satisfiable, l_False if unsatisfiable, l_Undef if interrupted.

eliminate()

Performs variable elimination based simplification.

bool eliminate(bool turn_off_elim = false);

turn_off_elim

bool

default:"false"

Whether to disable elimination after this call.

return

bool

Returns false if the formula becomes unsatisfiable during elimination, true otherwise.

This method eliminates variables by resolution when it does not significantly increase formula size.

Memory management

garbageCollect()

Performs garbage collection on internal storage.

virtual void garbageCollect();

This overrides the base Solver method to handle additional data structures used for simplification.

Configuration parameters

Elimination and simplification options

grow

int

default:"0"

Allows a variable elimination step to grow the formula by this many clauses.

clause_lim

int

default:"-1"

Variables are not eliminated if resolution produces a clause longer than this limit. Set to -1 for no limit.

subsumption_lim

int

default:"-1"

Do not check subsumption against clauses larger than this. Set to -1 for no limit.

simp_garbage_frac

double

Garbage collection threshold during simplification (distinct from normal solving).

Feature flags

use_asymm

bool

Enable asymmetric branching to shrink clauses.

use_rcheck

bool

Enable redundancy checking (checks if a clause is already implied). Expensive but powerful.

use_elim

bool

Enable variable elimination.

extend_model

bool

Flag indicating whether the user needs to access the full model including eliminated variables.

If extend_model is false, the model will only contain values for non-eliminated variables.

Statistics

merges

int

Number of clause merges performed during variable elimination.

asymm_lits

int

Number of literals removed by asymmetric branching.

eliminated_vars

int

Total number of variables eliminated by preprocessing.

Usage example

SimpSolver solver;

// Create variables
Var a = solver.newVar();
Var b = solver.newVar();
Var c = solver.newVar();

// Add clauses
solver.addClause(mkLit(a), mkLit(b));
solver.addClause(mkLit(a, true), mkLit(c));
solver.addClause(mkLit(b, true), mkLit(c, true));

// Freeze important variables if needed
solver.freezeVar(a);

// Solve with simplification
if (solver.solve(true, false)) {
    // Access model
    lbool val_a = solver.modelValue(a);
    lbool val_b = solver.modelValue(b);
    lbool val_c = solver.modelValue(c);
}

// Thaw variables for future elimination
solver.thaw();

Core API

Data Structures

Utilities

Constructor and destructor

SimpSolver()

~SimpSolver()

Problem specification

newVar()

releaseVar()

addClause()

addEmptyClause()

addClause_()

substitute()

Variable mode

setFrozen()

isEliminated()

freezeVar()

thaw()

Solving

solve()

solveLimited()

eliminate()

Memory management

garbageCollect()

Configuration parameters

Elimination and simplification options

Feature flags

Statistics

Usage example

Build docs developers (and LLMs) love

Core API

Data Structures

Utilities

​Constructor and destructor

​SimpSolver()

​~SimpSolver()

​Problem specification

​newVar()

​releaseVar()

​addClause()

​addEmptyClause()

​addClause_()

​substitute()

​Variable mode

​setFrozen()

​isEliminated()

​freezeVar()

​thaw()

​Solving

​solve()

​solveLimited()

​eliminate()

​Memory management

​garbageCollect()

​Configuration parameters

​Elimination and simplification options

​Feature flags

​Statistics

​Usage example

Build docs developers (and LLMs) love

Constructor and destructor

SimpSolver()

~SimpSolver()

Problem specification

newVar()

releaseVar()

addClause()

addEmptyClause()

addClause_()

substitute()

Variable mode

setFrozen()

isEliminated()

freezeVar()

thaw()

Solving

solve()

solveLimited()

eliminate()

Memory management

garbageCollect()

Configuration parameters

Elimination and simplification options

Feature flags

Statistics

Usage example