# OpenGraph DrawingFramework

v. 2022.02 (Dogwood)

Minisat::Internal::SimpSolver Class Reference

#include <ogdf/lib/minisat/simp/SimpSolver.h>

Inheritance diagram for Minisat::Internal::SimpSolver:

## Classes

struct  ClauseDeleted

struct  ElimLt

## Public Member Functions

SimpSolver ()

~SimpSolver ()

bool addClause (const vec< Lit > &ps)

bool addClause (Lit p, Lit q)

bool addClause (Lit p, Lit q, Lit r)

bool addClause_ (vec< Lit > &ps)

bool eliminate (bool turn_off_elim=false)

virtual void garbageCollect () override

bool isEliminated (Var v) const

Var newVar (bool polarity=true, bool dvar=true)

void setFrozen (Var v, bool b)

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

bool solve (const vec< Lit > &assumps, 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)

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

bool substitute (Var v, Lit x)

Public Member Functions inherited from Minisat::Internal::Solver
Solver ()

virtual ~Solver ()

bool addClause (const vec< Lit > &ps)

bool addClause (Lit p, Lit q)

bool addClause (Lit p, Lit q, Lit r)

bool addClause_ (vec< Lit > &ps)

void budgetOff ()

void checkGarbage ()

void checkGarbage (double gf)

void clearInterrupt ()

void interrupt ()

lbool modelValue (Lit p) const

lbool modelValue (Var x) const

int nAssigns () const

int nClauses () const

Var newVar (bool polarity=true, bool dvar=true)

int nFreeVars () const

int nLearnts () const

int nVars () const

bool okay () const

void setConfBudget (int64_t x)

void setDecisionVar (Var v, bool b)

void setPolarity (Var v, bool b)

void setPropBudget (int64_t x)

bool simplify ()

bool solve ()

bool solve (const vec< Lit > &assumps)

bool solve (double t, SolverStatus &st)

bool solve (Lit p)

bool solve (Lit p, Lit q)

bool solve (Lit p, Lit q, Lit r)

lbool solveLimited (const vec< Lit > &assumps)

void toDimacs (const char *file)

void toDimacs (const char *file, const vec< Lit > &assumps)

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 (std::ostream &out, Clause &c, vec< Var > &map, Var &max)

void toDimacs (std::ostream &out, const vec< Lit > &assumps)

lbool value (Lit p) const

lbool value (Var x) const

## Public Attributes

int asymm_lits

int clause_lim

int eliminated_vars

int grow

int merges

double simp_garbage_frac

int subsumption_lim

bool use_asymm

bool use_elim

bool use_rcheck

Public Attributes inherited from Minisat::Internal::Solver
int ccmin_mode

double clause_decay

uint64_t clauses_literals

vec< Litconflict

uint64_t conflicts

uint64_t dec_vars

uint64_t decisions

double garbage_frac

uint64_t learnts_literals

double learntsize_factor

double learntsize_inc

bool luby_restart

uint64_t max_literals

vec< lboolmodel

int phase_saving

uint64_t propagations

double random_seed

double random_var_freq

int restart_first

double restart_inc

uint64_t rnd_decisions

bool rnd_init_act

bool rnd_pol

uint64_t solves

uint64_t starts

uint64_t tot_literals

double var_decay

int verbosity

## Protected Member Functions

bool asymm (Var v, CRef cr)

bool asymmVar (Var v)

bool backwardSubsumptionCheck (bool verbose=false)

void cleanUpClauses ()

bool eliminateVar (Var v)

void extendModel ()

void gatherTouchedClauses ()

bool implied (const vec< Lit > &c)

bool merge (const Clause &_ps, const Clause &_qs, Var v, int &size)

bool merge (const Clause &_ps, const Clause &_qs, Var v, vec< Lit > &out_clause)

void relocAll (ClauseAllocator &to)

void removeClause (CRef cr)

lbool solve_ (bool do_simp=true, bool turn_off_simp=false)

bool strengthenClause (CRef cr, Lit l)

void updateElimHeap (Var v)

Protected Member Functions inherited from Minisat::Internal::Solver
uint32_t abstractLevel (Var x) const

void analyze (CRef confl, vec< Lit > &out_learnt, int &out_btlevel)

void analyzeFinal (Lit p, vec< Lit > &out_conflict)

void attachClause (CRef cr)

void cancelUntil (int level)

void claBumpActivity (Clause &c)

int decisionLevel () const

void detachClause (CRef cr, bool strict=false)

bool enqueue (Lit p, CRef from=CRef_Undef)

void insertVarOrder (Var x)

int level (Var x) const

bool litRedundant (Lit p, uint32_t abstract_levels)

bool locked (const Clause &c) const

void newDecisionLevel ()

Lit pickBranchLit ()

double progressEstimate () const

CRef propagate ()

CRef reason (Var x) const

void rebuildOrderHeap ()

void reduceDB ()

void relocAll (ClauseAllocator &to)

void removeClause (CRef cr)

void removeSatisfied (vec< CRef > &cs)

bool satisfied (const Clause &c) const

lbool search (int nof_conflicts)

lbool search (int nof_conflicts, double &time)

lbool solve_ ()

lbool solve_ (double &t)

void uncheckedEnqueue (Lit p, CRef from=CRef_Undef)

void varBumpActivity (Var v)

void varBumpActivity (Var v, double inc)

void varDecayActivity ()

bool withinBudget () const

## Protected Attributes

int bwdsub_assigns

CRef bwdsub_tmpunit

Heap< ElimLtelim_heap

vec< uint32_t > elimclauses

vec< char > eliminated

int elimorder

vec< char > frozen

vec< int > n_occ

int n_touched

OccLists< Var, vec< CRef >, ClauseDeletedoccurs

Queue< CRefsubsumption_queue

vec< char > touched

bool use_simplification

Protected Attributes inherited from Minisat::Internal::Solver
vec< double > activity

vec< Litanalyze_stack

vec< Litanalyze_toclear

vec< lboolassigns

vec< Litassumptions

bool asynch_interrupt

ClauseAllocator ca

double cla_inc

vec< CRefclauses

int64_t conflict_budget

vec< char > decision

vec< CReflearnts

double max_learnts

bool ok

Heap< VarOrderLtorder_heap

vec< char > polarity

double progress_estimate

int64_t propagation_budget

bool remove_satisfied

vec< char > seen

int simpDB_assigns

int64_t simpDB_props

vec< Littrail

vec< int > trail_lim

double var_inc

vec< VarDatavardata

OccLists< Lit, vec< Watcher >, WatcherDeletedwatches

Public Types inherited from Minisat::Internal::Solver
enum  AnswerType { A_TRUE, A_FALSE, A_UNDEF }

Static Protected Member Functions inherited from Minisat::Internal::Solver
static double drand (double &seed)

static int irand (double &seed, int size)

static VarData mkVarData (CRef cr, int l)

## Detailed Description

Definition at line 33 of file SimpSolver.h.

## ◆ SimpSolver()

 Minisat::Internal::SimpSolver::SimpSolver ( )

## ◆ ~SimpSolver()

 Minisat::Internal::SimpSolver::~SimpSolver ( )

## Member Function Documentation

 bool Minisat::Internal::SimpSolver::addClause ( const vec< Lit > & ps )
inline

Definition at line 181 of file SimpSolver.h.

 bool Minisat::Internal::SimpSolver::addClause ( Lit p )
inline

Definition at line 183 of file SimpSolver.h.

 bool Minisat::Internal::SimpSolver::addClause ( Lit p, Lit q )
inline

Definition at line 184 of file SimpSolver.h.

 bool Minisat::Internal::SimpSolver::addClause ( Lit p, Lit q, Lit r )
inline

Definition at line 185 of file SimpSolver.h.

 bool Minisat::Internal::SimpSolver::addClause_ ( vec< Lit > & ps )

inline

Definition at line 182 of file SimpSolver.h.

## ◆ asymm()

 bool Minisat::Internal::SimpSolver::asymm ( Var v, CRef cr )
protected

## ◆ asymmVar()

 bool Minisat::Internal::SimpSolver::asymmVar ( Var v )
protected

## ◆ backwardSubsumptionCheck()

 bool Minisat::Internal::SimpSolver::backwardSubsumptionCheck ( bool verbose = false )
protected

## ◆ cleanUpClauses()

 void Minisat::Internal::SimpSolver::cleanUpClauses ( )
protected

## ◆ eliminate()

 bool Minisat::Internal::SimpSolver::eliminate ( bool turn_off_elim = false )

## ◆ eliminateVar()

 bool Minisat::Internal::SimpSolver::eliminateVar ( Var v )
protected

## ◆ extendModel()

 void Minisat::Internal::SimpSolver::extendModel ( )
protected

## ◆ garbageCollect()

 virtual void Minisat::Internal::SimpSolver::garbageCollect ( )
overridevirtual

Reimplemented from Minisat::Internal::Solver.

## ◆ gatherTouchedClauses()

 void Minisat::Internal::SimpSolver::gatherTouchedClauses ( )
protected

## ◆ implied()

 bool Minisat::Internal::SimpSolver::implied ( const vec< Lit > & c )
protected

## ◆ isEliminated()

 bool Minisat::Internal::SimpSolver::isEliminated ( Var v ) const
inline

Definition at line 171 of file SimpSolver.h.

## ◆ merge() [1/2]

 bool Minisat::Internal::SimpSolver::merge ( const Clause & _ps, const Clause & _qs, Var v, int & size )
protected

## ◆ merge() [2/2]

 bool Minisat::Internal::SimpSolver::merge ( const Clause & _ps, const Clause & _qs, Var v, vec< Lit > & out_clause )
protected

## ◆ newVar()

 Var Minisat::Internal::SimpSolver::newVar ( bool polarity = true, bool dvar = true )

## ◆ relocAll()

 void Minisat::Internal::SimpSolver::relocAll ( ClauseAllocator & to )
protected

## ◆ removeClause()

 void Minisat::Internal::SimpSolver::removeClause ( CRef cr )
protected

## ◆ setFrozen()

 void Minisat::Internal::SimpSolver::setFrozen ( Var v, bool b )
inline

Definition at line 186 of file SimpSolver.h.

## ◆ solve() [1/5]

 bool Minisat::Internal::SimpSolver::solve ( bool do_simp = true, bool turn_off_simp = false )
inline

Definition at line 188 of file SimpSolver.h.

## ◆ solve() [2/5]

 bool Minisat::Internal::SimpSolver::solve ( const vec< Lit > & assumps, bool do_simp = true, bool turn_off_simp = false )
inline

Definition at line 192 of file SimpSolver.h.

## ◆ solve() [3/5]

 bool Minisat::Internal::SimpSolver::solve ( Lit p, bool do_simp = true, bool turn_off_simp = false )
inline

Definition at line 189 of file SimpSolver.h.

## ◆ solve() [4/5]

 bool Minisat::Internal::SimpSolver::solve ( Lit p, Lit q, bool do_simp = true, bool turn_off_simp = false )
inline

Definition at line 190 of file SimpSolver.h.

## ◆ solve() [5/5]

 bool Minisat::Internal::SimpSolver::solve ( Lit p, Lit q, Lit r, bool do_simp = true, bool turn_off_simp = false )
inline

Definition at line 191 of file SimpSolver.h.

## ◆ solve_()

 lbool Minisat::Internal::SimpSolver::solve_ ( bool do_simp = true, bool turn_off_simp = false )
protected

## ◆ solveLimited()

 lbool Minisat::Internal::SimpSolver::solveLimited ( const vec< Lit > & assumps, bool do_simp = true, bool turn_off_simp = false )
inline

Definition at line 195 of file SimpSolver.h.

## ◆ strengthenClause()

 bool Minisat::Internal::SimpSolver::strengthenClause ( CRef cr, Lit l )
protected

## ◆ substitute()

 bool Minisat::Internal::SimpSolver::substitute ( Var v, Lit x )

## ◆ updateElimHeap()

 void Minisat::Internal::SimpSolver::updateElimHeap ( Var v )
inlineprotected

Definition at line 172 of file SimpSolver.h.

## ◆ asymm_lits

 int Minisat::Internal::SimpSolver::asymm_lits

Definition at line 96 of file SimpSolver.h.

## ◆ bwdsub_assigns

 int Minisat::Internal::SimpSolver::bwdsub_assigns
protected

Definition at line 139 of file SimpSolver.h.

## ◆ bwdsub_tmpunit

 CRef Minisat::Internal::SimpSolver::bwdsub_tmpunit
protected

Definition at line 144 of file SimpSolver.h.

## ◆ clause_lim

 int Minisat::Internal::SimpSolver::clause_lim

Definition at line 84 of file SimpSolver.h.

## ◆ elim_heap

 Heap Minisat::Internal::SimpSolver::elim_heap
protected

Definition at line 135 of file SimpSolver.h.

## ◆ elimclauses

 vec Minisat::Internal::SimpSolver::elimclauses
protected

Definition at line 130 of file SimpSolver.h.

## ◆ eliminated

 vec Minisat::Internal::SimpSolver::eliminated
protected

Definition at line 138 of file SimpSolver.h.

## ◆ eliminated_vars

 int Minisat::Internal::SimpSolver::eliminated_vars

Definition at line 97 of file SimpSolver.h.

## ◆ elimorder

 int Minisat::Internal::SimpSolver::elimorder
protected

Definition at line 128 of file SimpSolver.h.

## ◆ frozen

 vec Minisat::Internal::SimpSolver::frozen
protected

Definition at line 137 of file SimpSolver.h.

## ◆ grow

 int Minisat::Internal::SimpSolver::grow

Definition at line 83 of file SimpSolver.h.

## ◆ merges

 int Minisat::Internal::SimpSolver::merges

Definition at line 95 of file SimpSolver.h.

## ◆ n_occ

 vec Minisat::Internal::SimpSolver::n_occ
protected

Definition at line 134 of file SimpSolver.h.

## ◆ n_touched

 int Minisat::Internal::SimpSolver::n_touched
protected

Definition at line 140 of file SimpSolver.h.

## ◆ occurs

 OccLists, ClauseDeleted> Minisat::Internal::SimpSolver::occurs
protected

Definition at line 133 of file SimpSolver.h.

## ◆ simp_garbage_frac

 double Minisat::Internal::SimpSolver::simp_garbage_frac

Definition at line 87 of file SimpSolver.h.

## ◆ subsumption_lim

 int Minisat::Internal::SimpSolver::subsumption_lim

Definition at line 86 of file SimpSolver.h.

## ◆ subsumption_queue

 Queue Minisat::Internal::SimpSolver::subsumption_queue
protected

Definition at line 136 of file SimpSolver.h.

## ◆ touched

 vec Minisat::Internal::SimpSolver::touched
protected

Definition at line 131 of file SimpSolver.h.

## ◆ use_asymm

 bool Minisat::Internal::SimpSolver::use_asymm

Definition at line 89 of file SimpSolver.h.

## ◆ use_elim

 bool Minisat::Internal::SimpSolver::use_elim

Definition at line 91 of file SimpSolver.h.

## ◆ use_rcheck

 bool Minisat::Internal::SimpSolver::use_rcheck

Definition at line 90 of file SimpSolver.h.

## ◆ use_simplification

 bool Minisat::Internal::SimpSolver::use_simplification
protected

Definition at line 129 of file SimpSolver.h.

The documentation for this class was generated from the following file: