Open
Graph Drawing
Framework

 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)
 
bool addClause (Lit p, Lit q)
 
bool addClause (Lit p, Lit q, Lit r)
 
bool addClause_ (vec< Lit > &ps)
 
bool addEmptyClause ()
 
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)
 
bool addClause (Lit p, Lit q)
 
bool addClause (Lit p, Lit q, Lit r)
 
bool addClause_ (vec< Lit > &ps)
 
bool addEmptyClause ()
 
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_adjust_inc
 
int learntsize_adjust_start_confl
 
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)
 
void claDecayActivity ()
 
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< Litadd_tmp
 
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
 
int learntsize_adjust_cnt
 
double learntsize_adjust_confl
 
double max_learnts
 
bool ok
 
Heap< VarOrderLtorder_heap
 
vec< char > polarity
 
double progress_estimate
 
int64_t propagation_budget
 
int qhead
 
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
 

Additional Inherited Members

- 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.

Constructor & Destructor Documentation

◆ SimpSolver()

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

◆ ~SimpSolver()

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

Member Function Documentation

◆ addClause() [1/4]

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

Definition at line 181 of file SimpSolver.h.

◆ addClause() [2/4]

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

Definition at line 183 of file SimpSolver.h.

◆ addClause() [3/4]

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

Definition at line 184 of file SimpSolver.h.

◆ addClause() [4/4]

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

Definition at line 185 of file SimpSolver.h.

◆ addClause_()

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

◆ addEmptyClause()

bool Minisat::Internal::SimpSolver::addEmptyClause ( )
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.

Member Data Documentation

◆ 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<ElimLt> Minisat::Internal::SimpSolver::elim_heap
protected

Definition at line 135 of file SimpSolver.h.

◆ elimclauses

vec<uint32_t> Minisat::Internal::SimpSolver::elimclauses
protected

Definition at line 130 of file SimpSolver.h.

◆ eliminated

vec<char> 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<char> 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<int> 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<Var, vec<CRef>, 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<CRef> Minisat::Internal::SimpSolver::subsumption_queue
protected

Definition at line 136 of file SimpSolver.h.

◆ touched

vec<char> 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: