Interface for a SAT solver with standard features. More...

#include <SolverInterface.hpp>

Inheritance diagram for SolverInterface:

Collaboration diagram for SolverInterface:

Public Member Functions
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 void	printWinningLog ()
	Print the winning log.

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 Member Functions
template<typename Derived >
void	initializeTypeId ()
	Initialize the type ID for a derived class.

Static Protected Member Functions
template<typename Derived >
static unsigned int	getAndIncrementTypeCount ()
	Get and increment the instance count for a specific derived type.

Protected Attributes
SolverAlgorithmType	m_algoType

std::atomic< bool >	m_initialized

unsigned int	m_solverTypeId

int	m_solverId

Static Protected Attributes
static std::unordered_map< std::type_index, std::atomic< unsigned int > >	s_instanceCounts
	Number of existing instances of derived classes.

Detailed Description

Interface for a SAT solver with standard features.

Constructor & Destructor Documentation

◆ SolverInterface()

SolverInterface::SolverInterface	(	SolverAlgorithmType	algoType,
		int	solverId )

Constructor for SolverInterface.

Parameters

algoType	The algorithm type.
solverId	The solver ID.

Member Function Documentation

◆ addClause()

virtual void SolverInterface::addClause ( ClauseExchangePtr clause )

pure virtual

Add a permanent clause to the formula.

Parameters

clause The clause to add.

Implemented in Cadical, GlucoseSyrup, Kissat, KissatINCSolver, KissatMABSolver, Lingeling, MapleCOMSPSSolver, MiniSat, preprocess, StructuredBVA, and YalSat.

◆ addClauses()

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

pure virtual

Add a list of permanent clauses to the formula.

Parameters

clauses The list of clauses to add.

Implemented in Cadical, GlucoseSyrup, Kissat, KissatINCSolver, KissatMABSolver, Lingeling, MapleCOMSPSSolver, MiniSat, preprocess, StructuredBVA, and YalSat.

◆ addInitialClauses()

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

pure virtual

Add a list of initial clauses to the formula.

Parameters

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

Implemented in Cadical, GlucoseSyrup, Kissat, KissatINCSolver, KissatMABSolver, Lingeling, MapleCOMSPSSolver, MiniSat, preprocess, StructuredBVA, and YalSat.

◆ diversify()

virtual void SolverInterface::diversify ( const SeedGenerator & getSeed = [](SolverInterface *s) { return s->getSolverId();} )

pure virtual

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

Implemented in Cadical, GlucoseSyrup, Kissat, KissatINCSolver, KissatMABSolver, Lingeling, MapleCOMSPSSolver, MiniSat, preprocess, StructuredBVA, and YalSat.

◆ getAlgoType()

SolverAlgorithmType SolverInterface::getAlgoType ( )

inline

Get the algorithm type of the solver.

Returns: The algorithm type.

◆ getAndIncrementTypeCount()

template<typename Derived >

static unsigned int SolverInterface::getAndIncrementTypeCount ( )

inlinestaticprotected

Get and increment the instance count for a specific derived type.

Template Parameters

Derived The type of the derived class.

Returns: unsigned int The count of instances (including this one) of the specified type.

◆ getDivisionVariable()

virtual int SolverInterface::getDivisionVariable ( )

pure virtual

Get a variable suitable for search splitting.

Returns: The division variable.

Implemented in Cadical, GlucoseSyrup, Kissat, KissatINCSolver, KissatMABSolver, Lingeling, MapleCOMSPSSolver, MiniSat, preprocess, StructuredBVA, and YalSat.

◆ getModel()

virtual std::vector< int > SolverInterface::getModel ( )

pure virtual

Return the model in case of SAT result.

Returns: The model as a vector of integers.

Implemented in Cadical, GlucoseSyrup, Kissat, KissatINCSolver, KissatMABSolver, Lingeling, MapleCOMSPSSolver, MiniSat, preprocess, StructuredBVA, and YalSat.

◆ getSolverId()

unsigned int SolverInterface::getSolverId ( )

inline

Get the solver ID.

Returns: The solver ID.

◆ getSolverTypeCount()

unsigned int SolverInterface::getSolverTypeCount ( ) const

inline

Get the current count of instances of this object's most-derived type.

Returns: unsigned int The current count of instances of this object's most-derived type.

◆ getSolverTypeId()

unsigned int SolverInterface::getSolverTypeId ( )

inline

Get the solver type ID.

Returns: The solver type ID.

◆ getVariablesCount()

virtual unsigned int SolverInterface::getVariablesCount ( )

pure virtual

Get the current number of variables.

Returns: The number of variables.

Implemented in Cadical, GlucoseSyrup, Kissat, KissatINCSolver, KissatMABSolver, Lingeling, MapleCOMSPSSolver, MiniSat, preprocess, StructuredBVA, and YalSat.

◆ initializeTypeId()

template<typename Derived >

void SolverInterface::initializeTypeId ( )

inlineprotected

Initialize the type ID for a derived class.

This method should be called in the constructor of each derived class to properly initialize the type-specific instance count.

Template Parameters

Derived The type of the derived class.

◆ isInitialized()

bool SolverInterface::isInitialized ( )

inline

Check if the solver is initialized.

Returns: True if initialized, false otherwise.

◆ loadFormula()

virtual void SolverInterface::loadFormula ( const char * filename )

pure virtual

Load formula from a given dimacs file.

Parameters

filename The name of the file to load from.

Implemented in Cadical, GlucoseSyrup, Kissat, KissatINCSolver, KissatMABSolver, Lingeling, MapleCOMSPSSolver, MiniSat, preprocess, StructuredBVA, and YalSat.

◆ printParameters()

virtual void SolverInterface::printParameters ( )

virtual

Print the parameters set for a solver.

Reimplemented in YalSat.

◆ printStatistics()

virtual void SolverInterface::printStatistics ( )

virtual

Print solver statistics.

Reimplemented in Cadical, GlucoseSyrup, Kissat, KissatINCSolver, KissatMABSolver, Lingeling, MapleCOMSPSSolver, MiniSat, preprocess, StructuredBVA, and YalSat.

◆ printWinningLog()

virtual void SolverInterface::printWinningLog ( )

virtual

Print the winning log.

Reimplemented in Cadical, GlucoseSyrup, Kissat, KissatINCSolver, KissatMABSolver, Lingeling, LocalSearchInterface, MapleCOMSPSSolver, MiniSat, and SolverCdclInterface.

◆ setInitialized()

void SolverInterface::setInitialized ( bool value )

inline

Set the initialization status of the solver.

Parameters

value The initialization status to set.

◆ setSolverId()

void SolverInterface::setSolverId ( unsigned int id )

inline

Set the solver ID.

Parameters

id	The solver ID to set.

◆ setSolverInterrupt()

virtual void SolverInterface::setSolverInterrupt ( )

pure virtual

Interrupt resolution, solving cannot continue until interrupt is unset.

Implemented in Cadical, GlucoseSyrup, Kissat, KissatINCSolver, KissatMABSolver, Lingeling, MapleCOMSPSSolver, MiniSat, preprocess, StructuredBVA, and YalSat.

◆ setSolverTypeId()

void SolverInterface::setSolverTypeId ( unsigned int typeId )

inline

Set the solver type ID.

Parameters

typeId The solver type ID to set.

◆ solve()

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

pure virtual

Solve the formula with a given cube.

Parameters

cube	The cube to solve with.

Returns: The result of the solving process.

Implemented in Cadical, GlucoseSyrup, Kissat, KissatINCSolver, KissatMABSolver, Lingeling, MapleCOMSPSSolver, MiniSat, preprocess, StructuredBVA, and YalSat.

◆ unsetSolverInterrupt()

virtual void SolverInterface::unsetSolverInterrupt ( )

pure virtual

Remove the SAT solving interrupt request.

Implemented in Cadical, GlucoseSyrup, Kissat, KissatINCSolver, KissatMABSolver, Lingeling, MapleCOMSPSSolver, MiniSat, preprocess, StructuredBVA, and YalSat.

Member Data Documentation

◆ m_algoType

SolverAlgorithmType SolverInterface::m_algoType

protected

Algorithm family of this solver.

◆ m_initialized

std::atomic<bool> SolverInterface::m_initialized

protected

Initialization status.

◆ m_solverId

int SolverInterface::m_solverId

protected

Main ID of the solver.

◆ m_solverTypeId

unsigned int SolverInterface::m_solverTypeId

protected

ID local to the solver type.

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

/github/workspace/src/solvers/SolverInterface.hpp

Public Member Functions

Protected Member Functions

Static Protected Member Functions

Protected Attributes

Static Protected Attributes

Detailed Description

Constructor & Destructor Documentation

◆ SolverInterface()

Member Function Documentation

◆ addClause()

◆ addClauses()

◆ addInitialClauses()

◆ diversify()

◆ getAlgoType()

◆ getAndIncrementTypeCount()

◆ getDivisionVariable()

◆ getModel()

◆ getSolverId()

◆ getSolverTypeCount()

◆ getSolverTypeId()

◆ getVariablesCount()

◆ initializeTypeId()

◆ isInitialized()

◆ loadFormula()

◆ printParameters()

◆ printStatistics()

◆ printWinningLog()

◆ setInitialized()

◆ setSolverId()

◆ setSolverInterrupt()

◆ setSolverTypeId()

◆ solve()

◆ unsetSolverInterrupt()

Member Data Documentation

◆ m_algoType

◆ m_initialized

◆ m_solverId

◆ m_solverTypeId