SolverFactory Class Reference

Factory class for creating and managing SAT solvers. More...

#include <SolverFactory.hpp>

Collaboration diagram for SolverFactory:

Static Public Member Functions
static SolverAlgorithmType	createSolver (char type, char importDbType, std::shared_ptr< SolverInterface > &createdSolver)
	Creates a solver of the specified type.
static SolverAlgorithmType	createSolver (char type, char importDBType, std::vector< std::shared_ptr< SolverCdclInterface > > &cdclSolvers, std::vector< std::shared_ptr< LocalSearchInterface > > &localSolvers)
	Creates a solver of the specified type and adds it to the appropriate vector.
static void	createSolvers (int count, char importDBType, std::string portfolio, std::vector< std::shared_ptr< SolverCdclInterface > > &cdclSolvers, std::vector< std::shared_ptr< LocalSearchInterface > > &localSolvers)
	Creates multiple solvers based on a portfolio.
static void	printStats (const std::vector< std::shared_ptr< SolverCdclInterface > > &cdclSolvers, const std::vector< std::shared_ptr< LocalSearchInterface > > &localSolvers)
	Prints statistics for a group of solvers.
static void	diversification (const std::vector< std::shared_ptr< SolverCdclInterface > > &cdclSolvers, const std::vector< std::shared_ptr< LocalSearchInterface > > &localSolvers, const IDScaler &generalIdScaler=[](const std::shared_ptr< SolverInterface > &solver) { return solver->getSolverId();}, const IDScaler &typeIdScaler=[](const std::shared_ptr< SolverInterface > &solver) { return solver->getSolverTypeId();})
	Applies diversification to a group of solvers.

Static Public Attributes
static std::atomic< int >	currentIdSolver
	Atomic counter for assigning unique IDs to solvers.

Detailed Description

Factory class for creating and managing SAT solvers.

Member Function Documentation

createSolver() [1/2]

static SolverAlgorithmType SolverFactory::createSolver ( char type, char importDbType, std::shared_ptr< SolverInterface > & createdSolver )

static

Creates a solver of the specified type.

Parameters

type	Character representing the solver type (e.g., 'g' for Glucose, 'l' for Lingeling).
importDBType	Character representing the import database type ('s' for single buffer, 'm' for Mallob, 'd' for per size).
createdSolver	Shared pointer to store the created solver.

Returns

The algorithm type of the created solver.

createSolver() [2/2]

static SolverAlgorithmType SolverFactory::createSolver ( char type, char importDBType, std::vector< std::shared_ptr< SolverCdclInterface > > & cdclSolvers, std::vector< std::shared_ptr< LocalSearchInterface > > & localSolvers )

static

Creates a solver of the specified type and adds it to the appropriate vector.

Parameters

type	Character representing the solver type.
importDbType	Character representing the import database type.
cdclSolvers	Vector to store created CDCL solvers.
localSolvers	Vector to store created local search solvers.

Returns

The algorithm type of the created solver (CDCL, LOCAL_SEARCH, or UNKNOWN).

createSolvers()

static void SolverFactory::createSolvers ( int count, char importDBType, std::string portfolio, std::vector< std::shared_ptr< SolverCdclInterface > > & cdclSolvers, std::vector< std::shared_ptr< LocalSearchInterface > > & localSolvers )

static

Creates multiple solvers based on a portfolio.

Parameters

count	Maximum number of solvers to create.
importDBType	Character representing the import database type.
portfolio	String representing the types of solvers to create.
cdclSolvers	Vector to store created CDCL solvers.
localSolvers	Vector to store created local search solvers.

diversification()

static void SolverFactory::diversification ( const std::vector< std::shared_ptr< SolverCdclInterface > > & cdclSolvers, const std::vector< std::shared_ptr< LocalSearchInterface > > & localSolvers, const IDScaler & generalIdScaler = [](const std::shared_ptr< SolverInterface > &solver) { return solver->getSolverId();}, const IDScaler & typeIdScaler = [](const std::shared_ptr< SolverInterface > &solver) { return solver->getSolverTypeId();} )

static

Applies diversification to a group of solvers.

Parameters

cdclSolvers	Vector of CDCL solvers.
localSolvers	Vector of local search solvers.
generalIdScaler	Function to scale the general solver ID (default uses solver's ID).
typeIdScaler	Function to scale the solver type ID (default uses solver's type ID).

printStats()

static void SolverFactory::printStats ( const std::vector< std::shared_ptr< SolverCdclInterface > > & cdclSolvers, const std::vector< std::shared_ptr< LocalSearchInterface > > & localSolvers )

static

Prints statistics for a group of solvers.

Parameters

cdclSolvers	Vector of CDCL solvers.
localSolvers	Vector of local search solvers.

---

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

• /github/workspace/src/solvers/SolverFactory.hpp