Interface for Local Search solvers. More...

#include <LocalSearchInterface.hpp>

Inheritance diagram for LocalSearchInterface:

Collaboration diagram for LocalSearchInterface:

Public Member Functions
	LocalSearchInterface (int solverId, LocalSearchType _lsType)
	Constructor for LocalSearchInterface.

virtual	~LocalSearchInterface ()=default
	Virtual destructor.

virtual void	setPhase (const unsigned int var, const bool phase)=0
	Set initial phase for a given variable.

void	printWinningLog ()
	Print winning log information.

unsigned int	getNbUnsat ()
	Get the number of unsatisfied clauses.

Public Member Functions inherited from SolverInterface
virtual unsigned int	getVariablesCount ()=0
	Get the current number of variables.

virtual int	getDivisionVariable ()=0
	Get a variable suitable for search splitting.

virtual void	setSolverInterrupt ()=0
	Interrupt resolution, solving cannot continue until interrupt is unset.

virtual void	unsetSolverInterrupt ()=0
	Remove the SAT solving interrupt request.

virtual SatResult	solve (const std::vector< int > &cube)=0
	Solve the formula with a given cube.

virtual void	addClause (ClauseExchangePtr clause)=0
	Add a permanent clause to the formula.

virtual void	addClauses (const std::vector< ClauseExchangePtr > &clauses)=0
	Add a list of permanent clauses to the formula.

virtual void	addInitialClauses (const std::vector< simpleClause > &clauses, unsigned int nbVars)=0
	Add a list of initial clauses to the formula.

virtual void	loadFormula (const char *filename)=0
	Load formula from a given dimacs file.

virtual void	printStatistics ()
	Print solver statistics.

virtual std::vector< int >	getModel ()=0
	Return the model in case of SAT result.

virtual void	printParameters ()
	Print the parameters set for a solver.

virtual void	diversify (const SeedGenerator &getSeed=[](SolverInterface *s) { return s->getSolverId();})=0
	Perform native diversification. The Default lambda returns the solver ID.

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.

Protected Attributes
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

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.

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

Interface for Local Search solvers.

This class specializes SolverInterface to provide a common interface for all Local Search solvers.

Constructor & Destructor Documentation

◆ LocalSearchInterface()

LocalSearchInterface::LocalSearchInterface	(	int	solverId,
		LocalSearchType	_lsType )

inline

Constructor for LocalSearchInterface.

Parameters

solverId	Unique identifier for the solver
_lsType	Type of local search algorithm

Member Function Documentation

◆ getNbUnsat()

unsigned int LocalSearchInterface::getNbUnsat ( )

inline

Get the number of unsatisfied clauses.

Returns: Number of unsatisfied clauses

◆ printWinningLog()

void LocalSearchInterface::printWinningLog ( )

inlinevirtual

Print winning log information.

This method extends the base class implementation by adding solver-specific information.

Reimplemented from SolverInterface.

◆ setPhase()

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

pure virtual

Set initial phase for a given variable.

Parameters

var	Variable identifier
phase	Boolean phase to set

Implemented in YalSat.

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

/github/workspace/src/solvers/LocalSearch/LocalSearchInterface.hpp

Public Member Functions

Protected Attributes