Class List

Here are the classes, structs, unions and interfaces with brief descriptions:

[detail level 123]

▼NClauseUtils	Helping Functions for Clause Management (Hash and Equality)
CClauseExchangeEqual	Equality functor for ClauseExchange objects
CClauseExchangeHash	Hash functor for ClauseExchange objects
CClauseExchangePtrEqual	Equality functor for ClauseExchangePtr objects
CClauseExchangePtrHash	Hash functor for ClauseExchangePtr objects
CClauseHash	Hash functor for simple clauses
▼NGlucose
Cvec
▼NMapleCOMSPS
Cvec
▼NMinisat
Cvec
▼Npainless
▼Cskipzero_span	A span-like container that skips zero elements when iterating
CIterator
Cvector2D	A 2D vector implementation optimized for sparse data
▼NParsers	A set of helper functions for CNF file parsing
CClauseProcessor	Abstract base class for clause processors
CRedundancyFilter	Filter for removing redundant clauses
CSBVAInit	A filter for Structured BVA (Binary Variable Addition)
CTautologyFilter	Filter for removing tautological clauses. A tautological clause or simple a tautology is a clause that contains a literal and its complement, thus always satisfied
CAllGatherSharing	Implements a global sharing strategy using MPI_Allgather for clause exchange
CBitset	A class representing a bitset with dynamic size
CBloomFilter
CCadical	Implements the different interfaces to interact with the Cadical CDCL solver
CClauseBuffer	Wrapper for boost::lockfree::queue to manage ClauseExchange objects
CClauseDatabase	Abstract base class defining the interface for clause storage and management
CClauseDatabaseBufferPerEntity	A clause database that maintain separate buffers for each entity, mimicing old painless default behavior
CClauseDatabaseMallob	A clause database implementation attempting to naively mimic the Simplified Adaptive Database from Mallob (ref:https://doi.org/10.1613/jair.1.15827)
CClauseDatabasePerSize	A clause database that organizes clauses based on their size
CClauseDatabaseSingleBuffer	This is just a ClauseDatabase wrapper around a ClauseBuufer
CClauseExchange	Represents an exchangeable clause with flexible array member
CClauseMeta
CDataType
Cfnv	Struct for Fowler-Noll-Vo parameters
Cfnv< T, typename std::enable_if< sizeof(T)==4 >::type >	Fowler-Noll-Vo hash parameters for 32 bits
Cfnv< T, typename std::enable_if< sizeof(T)==8 >::type >	Fowler-Noll-Vo hash parameters for 64 bits
CFormula	Represents a SAT formula with unit and non-unit clauses
CGenericGlobalSharing	Implements a generic global sharing strategy for clause exchange
CGlobalSharingStatistics	Statistics of a global sharing strategy
CGlobalSharingStrategy	Base class for global clause sharing strategies across MPI processes
CGlucoseSyrup	Instance of a Glucose solver
CHashMap
CHashNode
CHordeSatSharing	This strategy is a HordeSat-like sharing strategy
CKissat	Instance of a Kissat solver
CKissatINCSolver	Instance of a KissatINCSolver solver
CKissatMABSolver	Instance of a KissatMABSolver solver
CLingeling	Instance of a Lingeling solver
CLocalSearchInterface	Interface for Local Search solvers
CLocalSearchStats	Local search statistics
CMallobSharing	Implements a global sharing strategy based on the Mallob algorithm
CMapleCOMSPSSolver	Instance of a MapleCOMSPS solver
CMiniSat	Instance of a Minisat solver
CMutex	Mutex class
CPairCompare	Functor for the priority queue used in solve()
Cparameter
CParameters
CPortfolioPRS	An Implementation of WorkingStrategy that mimics the strategy used in the PRS-Distributed solver from ISC24
CPortfolioSimple	A Simple Implementation of WorkingStrategy for the portfolio parallel strategy This strategy uses the different factories SolverFactory and SharingStrategyFactory in order to instantiate the different needed components specified by the parameters
Cpreprocess	The different simplification techniques implemented in PRS framework
CPreprocessorInterface	Interface for preprocessor algorithms in SAT solving
CPreprocessorStats	Preperocessing technique statistics
CProofClause
CqueuePair	QueuePair struct used for the priorityQueue in solve
CSequentialWorker	Basic Implementation of WorkingStrategy for a sequential execution
CSharer	A sharer is a thread responsible for executing a list of SharingStrategies
CSharingEntity	A base class representing entities that can exchange clauses between themselves
CSharingStatistics	Local Sharing statistics.Sharing statistics
CSharingStrategy	SharingStrategy class, inheriting from SharingEntity
CSharingStrategyFactory	Factory class for creating and managing sharing strategies
CSimpleSharing	This strategy is a simple sharing strategy
CSolverCdclInterface	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
CSolverFactory	Factory class for creating and managing SAT solvers
CSolverInterface	Interface for a SAT solver with standard features
CSolvingCdclStatistics	Structure for solver statistics
CStructuredBVA	Structured Binary Variable Addition (SBVA) preprocessing algorithm
CThread	Thread class
Ctype_gate
CWorkingStrategy	Base Interface for Working Strategies
Cxorgate
CYalSat	Implements LocalSearchInterface to interact with the YalSAT local search solver