Open
Graph Drawing
Framework

 v. 2023.09 (Elderberry)
 

Minisat::Formula Class Reference

The Formula class. More...

#include <ogdf/external/Minisat.h>

+ Inheritance diagram for Minisat::Formula:

Public Member Functions

 Formula ()
 
virtual ~Formula ()
 
template<class Iteratable >
void addClause (const Iteratable &literals)
 Add a clause given by a list of literals. More...
 
void clauseAddLiteral (unsigned int clausePos, Internal::Var signedVar)
 adds a literal to a clause and moves clause to the end of list More...
 
void finalizeClause (const clause cl)
 adds a clause to the formula's solver. If not all variables are known, missing ones are generated auomatically More...
 
bool finalizeNotExtensibleClause (const clause cl)
 adds a clause to the formula's solver if all variables are known More...
 
ClausegetClause (const int pos)
 returns a clause at position pos in Formula More...
 
int getClauseCount ()
 count of learned clauses More...
 
int getProblemClauseCount ()
 count of problem clauses More...
 
Internal::Var getVarFromLit (const Internal::Lit &lit)
 
int getVariableCount ()
 returns varable count currently in solver More...
 
ClausenewClause ()
 creates a new clause within the formula. If not all variables are known, missing ones are generated auomatically More...
 
void newVar ()
 add a new variable to the formula More...
 
void newVars (unsigned int Count)
 add multiple new variables to the formula More...
 
bool readDimacs (const char *filename)
 read a formula from a DIMACS file More...
 
bool readDimacs (const string &filename)
 read a formula from a DIMACS file More...
 
bool readDimacs (std::istream &in)
 read a formula in DIMACS format More...
 
void removeClause (int i)
 removes a complete clause More...
 
void reset ()
 delete all clauses and variables More...
 
bool solve (Model &ReturnModel)
 tries to solve the formula More...
 
bool solve (Model &ReturnModel, double &timeLimit)
 tries to solve the formula with a time limit in milliseconds More...
 
bool writeDimacs (const char *filename)
 write a formula to a DIMACS file More...
 
bool writeDimacs (const string &filename)
 write a formula to a DIMACS file More...
 
bool writeDimacs (std::ostream &f)
 write a formula in DIMACS format More...
 

Private Member Functions

void free ()
 
- Private 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 ()
 
virtual void garbageCollect ()
 
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
 
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
 

Private Attributes

std::vector< Clause * > m_Clauses
 
std::stringstream m_messages
 
- Private 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
 
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

- Private Types inherited from Minisat::Internal::Solver
enum  AnswerType { A_TRUE, A_FALSE, A_UNDEF }
 
- Static Private 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

The Formula class.

Variables and Clauses are added to the Formula. The clauses can be resolved to solve a SAT problem. Variables are linear indexed.

Definition at line 213 of file Minisat.h.

Constructor & Destructor Documentation

◆ Formula()

Minisat::Formula::Formula ( )
inline

Definition at line 221 of file Minisat.h.

◆ ~Formula()

virtual Minisat::Formula::~Formula ( )
inlinevirtual

Definition at line 223 of file Minisat.h.

Member Function Documentation

◆ addClause()

template<class Iteratable >
void Minisat::Formula::addClause ( const Iteratable &  literals)
inline

Add a clause given by a list of literals.

Definition at line 250 of file Minisat.h.

◆ clauseAddLiteral()

void Minisat::Formula::clauseAddLiteral ( unsigned int  clausePos,
Internal::Var  signedVar 
)
inline

adds a literal to a clause and moves clause to the end of list

Definition at line 299 of file Minisat.h.

◆ finalizeClause()

void Minisat::Formula::finalizeClause ( const clause  cl)

adds a clause to the formula's solver. If not all variables are known, missing ones are generated auomatically

Parameters
clis a reference to the clause to be added to the formula

◆ finalizeNotExtensibleClause()

bool Minisat::Formula::finalizeNotExtensibleClause ( const clause  cl)

adds a clause to the formula's solver if all variables are known

Parameters
clis a reference to an existing clause within the formula
Returns
true if the clause was successfully added to the formula's solver, else return false and the clause is NOT added to the formula's solver

◆ free()

void Minisat::Formula::free ( )
private

◆ getClause()

Clause* Minisat::Formula::getClause ( const int  pos)

returns a clause at position pos in Formula

◆ getClauseCount()

int Minisat::Formula::getClauseCount ( )
inline

count of learned clauses

Definition at line 275 of file Minisat.h.

◆ getProblemClauseCount()

int Minisat::Formula::getProblemClauseCount ( )
inline

count of problem clauses

Definition at line 272 of file Minisat.h.

◆ getVarFromLit()

Internal::Var Minisat::Formula::getVarFromLit ( const Internal::Lit lit)
inline

Definition at line 295 of file Minisat.h.

◆ getVariableCount()

int Minisat::Formula::getVariableCount ( )
inline

returns varable count currently in solver

Definition at line 278 of file Minisat.h.

◆ newClause()

Clause* Minisat::Formula::newClause ( )

creates a new clause within the formula. If not all variables are known, missing ones are generated auomatically

Returns
a Pointer to the created Clause object

◆ newVar()

void Minisat::Formula::newVar ( )
inline

add a new variable to the formula

Definition at line 226 of file Minisat.h.

◆ newVars()

void Minisat::Formula::newVars ( unsigned int  Count)
inline

add multiple new variables to the formula

Definition at line 229 of file Minisat.h.

◆ readDimacs() [1/3]

bool Minisat::Formula::readDimacs ( const char *  filename)

read a formula from a DIMACS file

◆ readDimacs() [2/3]

bool Minisat::Formula::readDimacs ( const string &  filename)

read a formula from a DIMACS file

◆ readDimacs() [3/3]

bool Minisat::Formula::readDimacs ( std::istream &  in)

read a formula in DIMACS format

◆ removeClause()

void Minisat::Formula::removeClause ( int  i)

removes a complete clause

◆ reset()

void Minisat::Formula::reset ( )

delete all clauses and variables

◆ solve() [1/2]

bool Minisat::Formula::solve ( Model ReturnModel)

tries to solve the formula

Parameters
ReturnModelis the model output
Returns
true if the problem is satisfiable and writes the output model to param

◆ solve() [2/2]

bool Minisat::Formula::solve ( Model ReturnModel,
double &  timeLimit 
)

tries to solve the formula with a time limit in milliseconds

Parameters
ReturnModelis the model output
timeLimitis the time limit in milliseconds
Returns
true if the problem is satisfiable and writes the output model to param

◆ writeDimacs() [1/3]

bool Minisat::Formula::writeDimacs ( const char *  filename)

write a formula to a DIMACS file

◆ writeDimacs() [2/3]

bool Minisat::Formula::writeDimacs ( const string &  filename)

write a formula to a DIMACS file

◆ writeDimacs() [3/3]

bool Minisat::Formula::writeDimacs ( std::ostream &  f)

write a formula in DIMACS format

Member Data Documentation

◆ m_Clauses

std::vector<Clause*> Minisat::Formula::m_Clauses
private

Definition at line 216 of file Minisat.h.

◆ m_messages

std::stringstream Minisat::Formula::m_messages
private

Definition at line 215 of file Minisat.h.


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