Implements the different interfaces to interact with the Cadical CDCL solver. More...

#include <Cadical.hpp>

Inheritance diagram for Cadical:

Collaboration diagram for Cadical:

Public Member Functions
	Cadical (int id, const std::shared_ptr< ClauseDatabase > &clauseDB)
	Constructor.

virtual	~Cadical ()
	Destructor.

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

void	setSolverInterrupt () override
	Interrupt resolution, solving cannot continue until interrupt is unset.

void	unsetSolverInterrupt () override
	Remove the SAT solving interrupt request.

void	initCadicalOptions ()
	Initializes the map CadicalOptions with the default configuration.

void	diversify (const SeedGenerator &getSeed) override
	Native diversification.

void	loadFormula (const char *filename) override
	Load formula from a given dimacs file, return false if failed.

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

void	addClause (ClauseExchangePtr clause) override
	Add a permanent clause to the formula.

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

bool	importClause (const ClauseExchangePtr &clause) override
	Add a learned clause to the formula.

void	importClauses (const std::vector< ClauseExchangePtr > &clauses) override
	Add a list of learned clauses to the formula.

unsigned int	getVariablesCount () override
	Get the number of variables of the current resolution.

int	getDivisionVariable () override
	Get a variable suitable for search splitting.

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

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

void	printStatistics () override
	Get solver statistics.

void	printWinningLog () override
	Print the winning log.

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

std::vector< int >	getSatAssumptions () override
	Get current assumptions.

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

bool	learning (int size, int glue) override
	Tells if CaDiCaL should export a clause.

void	learn (int lit) override
	Used by the base solver to export a clause.

bool	hasClauseToImport () override
	Tells if CaDiCaL has a clause to import.

void	getClauseToImport (std::vector< int > &clause, int &glue) override
	Loads the clause to import data in the parameters.

Public Member Functions inherited from SolverCdclInterface
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 void	printParameters ()
	Print the parameters set for a solver.

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.

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
std::unordered_map< std::string, int >	cadicalOptions
	A map mapping a Cadical option name to its value.

Public Attributes inherited from SolverCdclInterface
SolverCdclType	m_cdclType
	Type of this CDCL solver.

Protected Attributes
std::unique_ptr< CaDiCaL::Solver >	solver
	Pointer to a Cadical solver.

ClauseBuffer	clausesToAdd
	Buffer used to add permanent clauses.

std::atomic< bool >	stopSolver
	Used to stop or continue the resolution.

Protected Attributes inherited from SolverCdclInterface
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

Implements the different interfaces to interact with the Cadical CDCL solver.

Member Function Documentation

◆ addClause()

void Cadical::addClause ( ClauseExchangePtr clause )

overridevirtual

Add a permanent clause to the formula.

Implements SolverInterface.

◆ addClauses()

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

overridevirtual

Add a list of permanent clauses to the formula.

Implements SolverInterface.

◆ addInitialClauses()

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

overridevirtual

Add a list of initial clauses to the formula.

Implements SolverInterface.

◆ bumpVariableActivity()

void Cadical::bumpVariableActivity	(	const int	var,
		const int	times )

overridevirtual

Bump activity of a given variable.

Implements SolverCdclInterface.

◆ diversify()

void Cadical::diversify ( const SeedGenerator & getSeed )

overridevirtual

Native diversification.

Implements SolverInterface.

◆ getClauseToImport()

void Cadical::getClauseToImport	(	std::vector< int > &	clause,
		int &	glue )

override

Loads the clause to import data in the parameters.

Parameters

clause	holds the clause literals
glue	holds the lbd value of the clause

◆ getDivisionVariable()

int Cadical::getDivisionVariable ( )

overridevirtual

Get a variable suitable for search splitting.

Implements SolverInterface.

◆ getFinalAnalysis()

std::vector< int > Cadical::getFinalAnalysis ( )

overridevirtual

Get the final analysis in case of UNSAT result.

Returns: Vector of integers representing the final analysis

Implements SolverCdclInterface.

◆ getModel()

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

overridevirtual

Return the model in case of SAT result.

Implements SolverInterface.

◆ getSatAssumptions()

std::vector< int > Cadical::getSatAssumptions ( )

overridevirtual

Get current assumptions.

Returns: Vector of integers representing the current assumptions

Implements SolverCdclInterface.

◆ getVariablesCount()

unsigned int Cadical::getVariablesCount ( )

overridevirtual

Get the number of variables of the current resolution.

Implements SolverInterface.

◆ hasClauseToImport()

bool Cadical::hasClauseToImport ( )

override

Tells if CaDiCaL has a clause to import.

Returns: true if there is one, false otherwise

◆ importClause()

bool Cadical::importClause ( const ClauseExchangePtr & clause )

overridevirtual

Add a learned clause to the formula.

Implements SharingEntity.

◆ importClauses()

void Cadical::importClauses ( const std::vector< ClauseExchangePtr > & clauses )

overridevirtual

Add a list of learned clauses to the formula.

Implements SharingEntity.

◆ learn()

void Cadical::learn ( int lit )

override

Used by the base solver to export a clause.

Parameters

lit	a literal of the clause to export (non zero integer), 0 if it is the end

◆ learning()

bool Cadical::learning	(	int	size,
		int	glue )

override

Tells if CaDiCaL should export a clause.

It is important to note that the methods are not multi-thread safe

Parameters

size	size of the clause to export
glue	lbd value of the clause to export

Returns: true if the clause is to be exported, false otherwise

◆ loadFormula()

void Cadical::loadFormula ( const char * filename )

overridevirtual

Load formula from a given dimacs file, return false if failed.

Implements SolverInterface.

◆ printStatistics()

void Cadical::printStatistics ( )

overridevirtual

Get solver statistics.

Reimplemented from SolverInterface.

◆ printWinningLog()

void Cadical::printWinningLog ( )

overridevirtual

Print the winning log.

Reimplemented from SolverInterface.

◆ setPhase()

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

overridevirtual

Set initial phase for a given variable.

Implements SolverCdclInterface.

◆ setSolverInterrupt()

void Cadical::setSolverInterrupt ( )

overridevirtual

Interrupt resolution, solving cannot continue until interrupt is unset.

Implements SolverInterface.

◆ solve()

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

overridevirtual

Solve the formula with a given cube.

Implements SolverInterface.

◆ unsetSolverInterrupt()

void Cadical::unsetSolverInterrupt ( )

overridevirtual

Remove the SAT solving interrupt request.

Implements SolverInterface.

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

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

Public Member Functions

Public Attributes

Protected Attributes

Additional Inherited Members

Detailed Description

Member Function Documentation

◆ addClause()

◆ addClauses()

◆ addInitialClauses()

◆ bumpVariableActivity()

◆ diversify()

◆ getClauseToImport()

◆ getDivisionVariable()

◆ getFinalAnalysis()

◆ getModel()

◆ getSatAssumptions()

◆ getVariablesCount()

◆ hasClauseToImport()

◆ importClause()

◆ importClauses()

◆ learn()

◆ learning()

◆ loadFormula()

◆ printStatistics()

◆ printWinningLog()

◆ setPhase()

◆ setSolverInterrupt()

◆ solve()

◆ unsetSolverInterrupt()