YalSat Class Reference

Implements LocalSearchInterface to interact with the YalSAT local search solver. More...

#include <YalSat.hpp>

Inheritance diagram for YalSat:

Collaboration diagram for YalSat:

Public Member Functions
	YalSat (int _id, unsigned long flipsLimit, unsigned long maxNoise)
unsigned int	getVariablesCount ()
	Get the current number of variables.
int	getDivisionVariable ()
	Get a variable suitable for search splitting.
void	setSolverInterrupt ()
	Interrupt resolution, solving cannot continue until interrupt is unset.
void	unsetSolverInterrupt ()
	Remove the SAT solving interrupt request.
void	setPhase (const unsigned int var, const bool phase)
	Set initial phase for a given variable.
SatResult	solve (const std::vector< int > &cube)
	Solve the formula with a given cube.
void	addClause (ClauseExchangePtr clause)
	Add a permanent clause to the formula.
void	addClauses (const std::vector< ClauseExchangePtr > &clauses)
	Add a list of permanent clauses to the formula.
void	addInitialClauses (const std::vector< simpleClause > &clauses, unsigned int nbVars)
	Add a list of initial clauses to the formula.
void	loadFormula (const char *filename)
	Load formula from a given dimacs file.
std::vector< int >	getModel ()
	Return the model in case of SAT result.
void	printStatistics ()
	Print solver statistics.
void	printParameters ()
	Print the parameters set for a solver.
void	diversify (const SeedGenerator &getSeed)
	Perform native diversification. The Default lambda returns the solver ID.
Public Member Functions inherited from LocalSearchInterface
	LocalSearchInterface (int solverId, LocalSearchType _lsType)
	Constructor for LocalSearchInterface.
virtual	~LocalSearchInterface ()=default
	Virtual destructor.
void	printWinningLog ()
	Print winning log information.
unsigned int	getNbUnsat ()
	Get the number of unsatisfied clauses.
Public Member Functions inherited from SolverInterface
bool	isInitialized ()
	Check if the solver is initialized.
void	setInitialized (bool value)
	Set the initialization status of the solver.
SolverAlgorithmType	getAlgoType ()
	Get the algorithm type of the solver.
unsigned int	getSolverTypeId ()
	Get the solver type ID.
void	setSolverTypeId (unsigned int typeId)
	Set the solver type ID.
unsigned int	getSolverId ()
	Get the solver ID.
void	setSolverId (unsigned int id)
	Set the solver ID.
unsigned int	getSolverTypeCount () const
	Get the current count of instances of this object's most-derived type.
	SolverInterface (SolverAlgorithmType algoType, int solverId)
	Constructor for SolverInterface.
virtual	~SolverInterface ()
	Virtual destructor for SolverInterface.

Friends
int	yalsat_terminate (void *p_YalSat)

Additional Inherited Members
Protected Member Functions inherited from SolverInterface
template<typename Derived >
void	initializeTypeId ()
	Initialize the type ID for a derived class.
Static Protected Member Functions inherited from SolverInterface
template<typename Derived >
static unsigned int	getAndIncrementTypeCount ()
	Get and increment the instance count for a specific derived type.
Protected Attributes inherited from LocalSearchInterface
LocalSearchType	lsType
	Type of the local search.
LocalSearchStats	lsStats
	Statistics on the local search.
std::vector< int >	finalTrail
	Vector holding the model or the final trail.
Protected Attributes inherited from SolverInterface
SolverAlgorithmType	m_algoType
std::atomic< bool >	m_initialized
unsigned int	m_solverTypeId
int	m_solverId
Static Protected Attributes inherited from SolverInterface
static std::unordered_map< std::type_index, std::atomic< unsigned int > >	s_instanceCounts
	Number of existing instances of derived classes.

Detailed Description

Implements LocalSearchInterface to interact with the YalSAT local search solver.

Member Function Documentation

addClause()

void YalSat::addClause ( ClauseExchangePtr clause )

virtual

Add a permanent clause to the formula.

Parameters

clause

The clause to add.

Implements SolverInterface.

addClauses()

void YalSat::addClauses ( const std::vector< ClauseExchangePtr > & clauses )

virtual

Add a list of permanent clauses to the formula.

Parameters

clauses

The list of clauses to add.

Implements SolverInterface.

addInitialClauses()

void YalSat::addInitialClauses ( const std::vector< simpleClause > & clauses, unsigned int nbVars )

virtual

Add a list of initial clauses to the formula.

Parameters

clauses	The list of initial clauses.
nbVars	The number of variables.

Implements SolverInterface.

diversify()

void YalSat::diversify ( const SeedGenerator & getSeed )

virtual

Perform native diversification. The Default lambda returns the solver ID.

Implements SolverInterface.

getDivisionVariable()

int YalSat::getDivisionVariable ( )

virtual

Get a variable suitable for search splitting.

Returns

The division variable.

Implements SolverInterface.

getModel()

std::vector< int > YalSat::getModel ( )

virtual

Return the model in case of SAT result.

Returns

The model as a vector of integers.

Implements SolverInterface.

getVariablesCount()

unsigned int YalSat::getVariablesCount ( )

virtual

Get the current number of variables.

Returns

The number of variables.

Implements SolverInterface.

loadFormula()

void YalSat::loadFormula ( const char * filename )

virtual

Load formula from a given dimacs file.

Parameters

filename

The name of the file to load from.

Implements SolverInterface.

printParameters()

void YalSat::printParameters ( )

virtual

Print the parameters set for a solver.

Reimplemented from SolverInterface.

printStatistics()

void YalSat::printStatistics ( )

virtual

Print solver statistics.

Reimplemented from SolverInterface.

setPhase()

void YalSat::setPhase ( const unsigned int var, const bool phase )

virtual

Set initial phase for a given variable.

Parameters

var	Variable identifier
phase	Boolean phase to set

Implements LocalSearchInterface.

setSolverInterrupt()

void YalSat::setSolverInterrupt ( )

virtual

Interrupt resolution, solving cannot continue until interrupt is unset.

Implements SolverInterface.

solve()

SatResult YalSat::solve ( const std::vector< int > & cube )

virtual

Solve the formula with a given cube.

Parameters

cube	The cube to solve with.

Returns

The result of the solving process.

Implements SolverInterface.

unsetSolverInterrupt()

void YalSat::unsetSolverInterrupt ( )

virtual

Remove the SAT solving interrupt request.

Implements SolverInterface.

---

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

• /github/workspace/src/solvers/LocalSearch/YalSat.hpp