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

void	clauseAddLiteral (unsigned int clausePos, Internal::Var signedVar)
	adds a literal to a clause and moves clause to the end of list

void	finalizeClause (const clause cl)
	adds a clause to the formula's solver. If not all variables are known, missing ones are generated auomatically

bool	finalizeNotExtensibleClause (const clause cl)
	adds a clause to the formula's solver if all variables are known

Clause *	getClause (const int pos)
	returns a clause at position pos in Formula

int	getClauseCount ()
	count of learned clauses

int	getProblemClauseCount ()
	count of problem clauses

Internal::Var	getVarFromLit (const Internal::Lit &lit)

int	getVariableCount ()
	returns varable count currently in solver

Clause *	newClause ()
	creates a new clause within the formula. If not all variables are known, missing ones are generated auomatically

void	newVar ()
	add a new variable to the formula

void	newVars (unsigned int Count)
	add multiple new variables to the formula

bool	readDimacs (const char *filename)
	read a formula from a DIMACS file

bool	readDimacs (const string &filename)
	read a formula from a DIMACS file

bool	readDimacs (std::istream &in)
	read a formula in DIMACS format

void	removeClause (int i)
	removes a complete clause

void	reset ()
	delete all clauses and variables

bool	solve (Model &ReturnModel)
	tries to solve the formula

bool	solve (Model &ReturnModel, double &timeLimit)
	tries to solve the formula with a time limit in milliseconds

bool	writeDimacs (const char *filename)
	write a formula to a DIMACS file

bool	writeDimacs (const string &filename)
	write a formula to a DIMACS file

bool	writeDimacs (std::ostream &f)
	write a formula in DIMACS format

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< Lit >	conflict

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< lbool >	model

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< Lit >	add_tmp

vec< Lit >	analyze_stack

vec< Lit >	analyze_toclear

vec< lbool >	assigns

vec< Lit >	assumptions

bool	asynch_interrupt

ClauseAllocator	ca

double	cla_inc

vec< CRef >	clauses

int64_t	conflict_budget

vec< char >	decision

vec< CRef >	learnts

int	learntsize_adjust_cnt

double	learntsize_adjust_confl

double	max_learnts

bool	ok

Heap< VarOrderLt >	order_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< Lit >	trail

vec< int >	trail_lim

double	var_inc

vec< VarData >	vardata

OccLists< Lit, vec< Watcher >, WatcherDeleted >	watches

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 220 of file Minisat.h.

Constructor & Destructor Documentation

◆ Formula()

Minisat::Formula::Formula ( )

inline

Definition at line 228 of file Minisat.h.

◆ ~Formula()

virtual Minisat::Formula::~Formula ( )

inlinevirtual

Definition at line 230 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 257 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 306 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

cl	is 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

cl	is 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 282 of file Minisat.h.

◆ getProblemClauseCount()

int Minisat::Formula::getProblemClauseCount ( )

inline

count of problem clauses

Definition at line 279 of file Minisat.h.

◆ getVarFromLit()

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

inline

Definition at line 302 of file Minisat.h.

◆ getVariableCount()

int Minisat::Formula::getVariableCount ( )

inline

returns varable count currently in solver

Definition at line 285 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 233 of file Minisat.h.

◆ newVars()

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

inline

add multiple new variables to the formula

Definition at line 236 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

ReturnModel is 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

ReturnModel	is the model output
timeLimit	is 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 223 of file Minisat.h.

◆ m_messages

std::stringstream Minisat::Formula::m_messages

private

Definition at line 222 of file Minisat.h.

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

include/ogdf/external/Minisat.h

OpenGraph DrawingFramework

Public Member Functions

Private Member Functions

Private Attributes

Additional Inherited Members

Detailed Description

Constructor & Destructor Documentation

◆ Formula()

◆ ~Formula()

Member Function Documentation

◆ addClause()

◆ clauseAddLiteral()

◆ finalizeClause()

◆ finalizeNotExtensibleClause()

◆ free()

◆ getClause()

◆ getClauseCount()

◆ getProblemClauseCount()

◆ getVarFromLit()

◆ getVariableCount()

◆ newClause()

◆ newVar()

◆ newVars()

◆ readDimacs() [1/3]

◆ readDimacs() [2/3]

◆ readDimacs() [3/3]

◆ removeClause()

◆ reset()

◆ solve() [1/2]

◆ solve() [2/2]

◆ writeDimacs() [1/3]

◆ writeDimacs() [2/3]

◆ writeDimacs() [3/3]

Member Data Documentation

◆ m_Clauses

◆ m_messages

Open
Graph Drawing
Framework