Interface for CDCL (Conflict-Driven Clause Learning) solvers This class provides a common interface for all CDCL solvers. It inherits from SolverInterface for solving primitives and SharingEntity for sharing primitives. More...

#include <SolverCdclInterface.hpp>

Inheritance diagram for SolverCdclInterface:

Collaboration diagram for SolverCdclInterface:

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

virtual void	bumpVariableActivity (const int var, const int times)=0
	Bump activity of a given variable.

virtual std::vector< int >	getFinalAnalysis ()=0
	Get the final analysis in case of UNSAT result.

virtual std::vector< int >	getSatAssumptions ()=0
	Get current assumptions.

void	printWinningLog ()
	Print winning log information.

SolverCdclType	getSolverType ()
	Returns solver type for static cast.

	SolverCdclInterface (int solverId, const std::shared_ptr< ClauseDatabase > &clauseDB, SolverCdclType solverCdclType)
	Constructor for SolverCdclInterface.

virtual	~SolverCdclInterface ()
	Virtual destructor.

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.

Public Member Functions inherited from SharingEntity
	SharingEntity ()
	Construct a new SharingEntity object.

	SharingEntity (const std::vector< std::shared_ptr< SharingEntity > > &clients)
	Construct a new SharingEntity object.

virtual	~SharingEntity ()
	Destroy the SharingEntity object.

virtual bool	importClause (const ClauseExchangePtr &clause)=0
	Import a single clause to this sharing entity.

virtual void	importClauses (const std::vector< ClauseExchangePtr > &v_clauses)=0
	Import multiple clauses to this sharing entity.

int	getSharingId () const
	Get the sharing ID of this entity.

void	setSharingId (int _id)
	Set the sharing ID of this entity.

virtual void	addClient (std::shared_ptr< SharingEntity > client)
	Add a client to this entity.

virtual void	removeClient (std::shared_ptr< SharingEntity > client)
	Remove a specific client from this entity.

size_t	getClientCount () const
	Get the current number of clients.

void	clearClients ()
	Remove all clients.

Public Attributes
SolverCdclType	m_cdclType
	Type of this CDCL solver.

Protected Attributes
std::shared_ptr< ClauseDatabase >	m_clausesToImport
	Database used to import clauses. Can be common with other solvers.

Protected Attributes inherited from SolverInterface
SolverAlgorithmType	m_algoType

std::atomic< bool >	m_initialized

unsigned int	m_solverTypeId

int	m_solverId

Protected Attributes inherited from SharingEntity
std::vector< std::weak_ptr< SharingEntity > >	m_clients
	List of weak pointers to client SharingEntities.

std::shared_mutex	m_clientsMutex
	Mutex to protect access to m_clients.

Additional Inherited Members
Protected Member Functions inherited from SolverInterface
template<typename Derived >
void	initializeTypeId ()
	Initialize the type ID for a derived class.

Protected Member Functions inherited from SharingEntity
virtual bool	exportClauseToClient (const ClauseExchangePtr &clause, std::shared_ptr< SharingEntity > client)
	Export a clause to a specific client.

bool	exportClause (const ClauseExchangePtr &clause)
	Export a clause to all registered clients.

void	exportClauses (const std::vector< ClauseExchangePtr > &clauses)
	Export multiple clauses to all registered clients.

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 CDCL (Conflict-Driven Clause Learning) solvers This class provides a common interface for all CDCL solvers. It inherits from SolverInterface for solving primitives and SharingEntity for sharing primitives.

Warning: Be sure to use the sharing_id for producer clauses, otherwise the default exportClauseToClient will behave wrongly

Constructor & Destructor Documentation

◆ SolverCdclInterface()

SolverCdclInterface::SolverCdclInterface	(	int	solverId,
		const std::shared_ptr< ClauseDatabase > &	clauseDB,
		SolverCdclType	solverCdclType )

inline

Constructor for SolverCdclInterface.

Parameters

solverId	Unique identifier for the solver
solverCdclType	Type of CDCL solver

Member Function Documentation

◆ bumpVariableActivity()

virtual void SolverCdclInterface::bumpVariableActivity	(	const int	var,
		const int	times )

pure virtual

Bump activity of a given variable.

Parameters

var	Variable identifier
times	Number of times to bump the activity

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

◆ getFinalAnalysis()

virtual std::vector< int > SolverCdclInterface::getFinalAnalysis ( )

pure virtual

Get the final analysis in case of UNSAT result.

Returns: Vector of integers representing the final analysis

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

◆ getSatAssumptions()

virtual std::vector< int > SolverCdclInterface::getSatAssumptions ( )

pure virtual

Get current assumptions.

Returns: Vector of integers representing the current assumptions

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

◆ printWinningLog()

void SolverCdclInterface::printWinningLog ( )

inlinevirtual

Print winning log information.

Reimplemented from SolverInterface.

◆ setPhase()

virtual void SolverCdclInterface::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 Cadical, GlucoseSyrup, Kissat, KissatINCSolver, KissatMABSolver, Lingeling, MapleCOMSPSSolver, and MiniSat.

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

/github/workspace/src/solvers/CDCL/SolverCdclInterface.hpp

Public Member Functions

Public Attributes

Protected Attributes

Additional Inherited Members

Detailed Description

Constructor & Destructor Documentation

◆ SolverCdclInterface()

Member Function Documentation

◆ bumpVariableActivity()

◆ getFinalAnalysis()

◆ getSatAssumptions()

◆ printWinningLog()

◆ setPhase()