Solver - MiniSat

The Solver class is the main interface for SAT solving in MiniSat. It implements the Conflict-Driven Clause Learning (CDCL) algorithm with activity-based variable ordering and clause learning.

Constructor and destructor

Solver()

Creates a new solver instance with default configuration.

Solver();

~Solver()

Virtual destructor for cleanup.

virtual ~Solver();

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. Can be l_True, l_False, or l_Undef for no preference.

dvar

bool

default:"true"

Whether the variable should be a decision variable (eligible for selection in the decision heuristic).

return

Var

The newly created variable identifier.

releaseVar()

Makes a literal true and promises to never refer to the variable again.

void releaseVar(Lit l);

Lit

required

The literal to release.

After calling this method, the variable should never be referenced again in the solver.

addClause()

Adds a clause to the solver. Multiple overloads are available for different clause sizes.

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 (for unit, binary, ternary, and quaternary clauses).

Lit

Second literal (for binary, ternary, and quaternary clauses).

Lit

Third literal (for ternary and quaternary clauses).

Lit

Fourth literal (for quaternary clauses).

return

bool

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

addEmptyClause()

Adds the empty clause, making the solver contradictory.

bool addEmptyClause();

return

bool

Returns false (the formula becomes unsatisfiable).

addClause_()

Adds a clause to the solver without making superfluous internal copy.

bool addClause_(vec<Lit>& ps);

vec<Lit>&

required

Vector of literals forming the clause. Will be modified by this method.

return

bool

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

This method modifies the passed vector for efficiency. Use the const reference version if you need to preserve the original vector.

Solving

solve()

Searches for a satisfying assignment. Multiple overloads support different assumption sets.

bool solve();
bool solve(Lit p);
bool solve(Lit p, Lit q);
bool solve(Lit p, Lit q, Lit r);
bool solve(const vec<Lit>& assumps);

Lit

First assumption literal.

Lit

Second assumption literal.

Lit

Third assumption literal.

assumps

const vec<Lit>&

Vector of assumption literals that must be satisfied.

return

bool

Returns true if the formula is satisfiable under the given assumptions, false otherwise.

If satisfiable, the model can be read from the model member variable.

solveLimited()

Searches for a model with resource constraints.

lbool solveLimited(const vec<Lit>& assumps);

assumps

const vec<Lit>&

required

Vector of assumption literals.

return

lbool

Returns l_True if satisfiable, l_False if unsatisfiable, or l_Undef if the search was interrupted due to resource limits.

simplify()

Removes already satisfied clauses.

bool simplify();

return

bool

Returns false if the formula is unsatisfiable, true otherwise.

okay()

Checks if the solver is in a consistent state.

bool okay() const;

return

bool

Returns false if the solver is in a conflicting state, true otherwise.

implies()

Checks logical implications under assumptions.

bool implies(const vec<Lit>& assumps, vec<Lit>& out);

assumps

const vec<Lit>&

required

Vector of assumptions.

out

vec<Lit>&

required

Output vector for implied literals.

return

bool

Returns true if implications were found.

Variable mode

setPolarity()

Declares which polarity the decision heuristic should use for a variable.

void setPolarity(Var v, lbool b);

Var

required

The variable to configure.

lbool

required

The preferred polarity: l_True, l_False, or l_Undef.

Requires the polarity mode to be set to ‘polarity_user’ in solver configuration.

setDecisionVar()

Declares if a variable should be eligible for selection in the decision heuristic.

void setDecisionVar(Var v, bool b);

Var

required

The variable to configure.

bool

required

true to make the variable a decision variable, false to exclude it from decisions.

Read state

value()

Gets the current value of a variable or literal.

lbool value(Var x) const;
lbool value(Lit p) const;

Var

Variable to query.

Lit

Literal to query.

return

lbool

Current assignment: l_True, l_False, or l_Undef if unassigned.

modelValue()

Gets the value of a variable or literal in the last model.

lbool modelValue(Var x) const;
lbool modelValue(Lit p) const;

Var

Variable to query.

Lit

Literal to query.

return

lbool

Value in the last model: l_True or l_False.

The last call to solve() must have been satisfiable before calling this method.

nAssigns()

Gets the current number of assigned literals.

int nAssigns() const;

return

int

Number of assigned literals.

nClauses()

Gets the current number of original clauses.

int nClauses() const;

return

int

Number of original clauses.

nLearnts()

Gets the current number of learnt clauses.

int nLearnts() const;

return

int

Number of learnt clauses.

nVars()

Gets the current number of variables.

int nVars() const;

return

int

Total number of variables in the solver.

nFreeVars()

Gets the number of free (unassigned) variables.

int nFreeVars() const;

return

int

Number of unassigned variables.

printStats()

Prints current statistics to standard output.

void printStats() const;

Resource constraints

setConfBudget()

Sets a conflict budget for the solver.

void setConfBudget(int64_t x);

int64_t

required

Maximum number of conflicts allowed.

setPropBudget()

Sets a propagation budget for the solver.

void setPropBudget(int64_t x);

int64_t

required

Maximum number of propagations allowed.

budgetOff()

Disables all resource budgets.

void budgetOff();

interrupt()

Triggers a potentially asynchronous interruption of the solver.

void interrupt();

This method can be called from another thread to interrupt a running search.

clearInterrupt()

Clears the interrupt indicator flag.

void clearInterrupt();

Clause iteration

clausesBegin() / clausesEnd()

Iterators for traversing original clauses.

ClauseIterator clausesBegin() const;
ClauseIterator clausesEnd() const;

return

ClauseIterator

Iterator pointing to the beginning or end of the clause list.

trailBegin() / trailEnd()

Iterators for traversing top-level assignments.

TrailIterator trailBegin() const;
TrailIterator trailEnd() const;

return

TrailIterator

Iterator pointing to the beginning or end of the assignment trail.

DIMACS output

toDimacs()

Writes the CNF formula to a file in DIMACS format.

void toDimacs(const char* file);
void toDimacs(const char* file, Lit p);
void toDimacs(const char* file, Lit p, Lit q);
void toDimacs(const char* file, Lit p, Lit q, Lit r);
void toDimacs(const char* file, const vec<Lit>& assumps);
void toDimacs(FILE* f, const vec<Lit>& assumps);
void toDimacs(FILE* f, Clause& c, vec<Var>& map, Var& max);

file

const char*

Path to the output file.

FILE*

Open file handle for output.

Lit

First assumption literal.

Lit

Second assumption literal.

Lit

Third assumption literal.

assumps

const vec<Lit>&

Vector of assumptions to include.

Clause&

Specific clause to write.

map

vec<Var>&

Variable mapping.

max

Var&

Maximum variable.

Memory management

garbageCollect()

Performs garbage collection on internal clause storage.

virtual void garbageCollect();

checkGarbage()

Checks if garbage collection should be triggered.

void checkGarbage();
void checkGarbage(double gf);

double

Garbage fraction threshold. Collection is triggered when wasted memory exceeds this fraction.

Public member variables

Result variables

model

vec<lbool>

If the problem is satisfiable, this vector contains the model with variable assignments.

conflict

LSet

If unsatisfiable under assumptions, this represents the final conflict clause expressed in the assumptions.

Configuration parameters

verbosity

int

Controls output verbosity level.

var_decay

double

Variable activity decay factor (default 0.95).

clause_decay

double

Clause activity decay factor (default 0.999).

random_var_freq

double

Frequency of random variable selection (default 0.0).

random_seed

double

Random seed for the solver.

luby_restart

bool

Use Luby restart sequence if true.

ccmin_mode

int

Conflict clause minimization mode: 0=none, 1=basic, 2=deep.

phase_saving

int

Phase saving level: 0=none, 1=limited, 2=full.

rnd_pol

bool

Use random polarities for branching heuristics.

rnd_init_act

bool

Initialize variable activities with small random values.

garbage_frac

double

Fraction of wasted memory allowed before triggering garbage collection.

min_learnts_lim

int

Minimum learnt clause limit.

restart_first

int

Initial restart limit (default 100).

restart_inc

double

Restart limit multiplier for each restart (default 1.5).

learntsize_factor

double

Initial learnt clause limit as factor of original clauses (default 1/3).

learntsize_inc

double

Learnt clause limit multiplier for each restart (default 1.1).

learntsize_adjust_start_confl

int

Conflict count to start adjusting learnt clause limit.

learntsize_adjust_inc

double

Adjustment increment for learnt clause limit.

Statistics

solves

uint64_t

Number of solve calls.

starts

uint64_t

Number of search restarts.

decisions

uint64_t

Number of decisions made.

rnd_decisions

uint64_t

Number of random decisions.

propagations

uint64_t

Number of propagations performed.

conflicts

uint64_t

Number of conflicts encountered.

dec_vars

uint64_t

Number of decision variables.

num_clauses

uint64_t

Total number of original clauses.

num_learnts

uint64_t

Total number of learnt clauses.

clauses_literals

uint64_t

Total literals in original clauses.

learnts_literals

uint64_t

Total literals in learnt clauses.

max_literals

uint64_t

Maximum literals encountered.

tot_literals

uint64_t

Total literals processed.

Core API

Data Structures

Utilities

​Constructor and destructor

​Solver()

​~Solver()

​Problem specification

​newVar()

​releaseVar()

​addClause()

​addEmptyClause()

​addClause_()

​Solving

​solve()

​solveLimited()

​simplify()

​okay()

​implies()

​Variable mode

​setPolarity()

​setDecisionVar()

​Read state

​value()

​modelValue()

​nAssigns()

​nClauses()

​nLearnts()

​nVars()

​nFreeVars()

​printStats()

​Resource constraints

​setConfBudget()

​setPropBudget()

​budgetOff()

​interrupt()

​clearInterrupt()

​Clause iteration

​clausesBegin() / clausesEnd()

​trailBegin() / trailEnd()

​DIMACS output

​toDimacs()

​Memory management

​garbageCollect()

​checkGarbage()

​Public member variables

​Result variables

​Configuration parameters

​Statistics

Build docs developers (and LLMs) love

Constructor and destructor

Solver()

~Solver()

Problem specification

newVar()

releaseVar()

addClause()

addEmptyClause()

addClause_()

Solving

solve()

solveLimited()

simplify()

okay()

implies()

Variable mode

setPolarity()

setDecisionVar()

Read state

value()

modelValue()

nAssigns()

nClauses()

nLearnts()

nVars()

nFreeVars()

printStats()

Resource constraints

setConfBudget()

setPropBudget()

budgetOff()

interrupt()

clearInterrupt()

Clause iteration

clausesBegin() / clausesEnd()

trailBegin() / trailEnd()

DIMACS output

toDimacs()

Memory management

garbageCollect()

checkGarbage()

Public member variables

Result variables

Configuration parameters

Statistics