ClauseDatabaseMallob Class Reference

A clause database implementation attempting to naively mimic the Simplified Adaptive Database from Mallob (ref:https://doi.org/10.1613/jair.1.15827). More...

#include <ClauseDatabaseMallob.hpp>

Inheritance diagram for ClauseDatabaseMallob:

Collaboration diagram for ClauseDatabaseMallob:

Public Member Functions
	ClauseDatabaseMallob (int maxClauseSize, int maxPartitioningLbd, size_t maxCapacity, int maxFreeSize)
	Constructs a new ClauseDatabaseMallob object.
	~ClauseDatabaseMallob () override
	Virtual destructor.
bool	addClause (ClauseExchangePtr clause) override
	Adds a clause to the database.
size_t	giveSelection (std::vector< ClauseExchangePtr > &selectedCls, unsigned int literalCountLimit) override
	Fills a buffer with selected clauses up to a given size limit.
void	getClauses (std::vector< ClauseExchangePtr > &v_cls) override
	Fills a buffer with all clauses in the database.
bool	getOneClause (ClauseExchangePtr &cls) override
	Retrieves a single clause from the best (smallest index) buffer possible.
size_t	getSize () const override
	Gets the total number of clauses in the database.
size_t	shrinkDatabase () override
	Shrinks the database by removing clauses to maintain the size within capacity.
void	clearDatabase () override
	Clears all clauses from the database and resets internal counters.
Public Member Functions inherited from ClauseDatabase
	ClauseDatabase ()
	Default Constructor.
virtual	~ClauseDatabase ()
	Virtual destructor to ensure proper cleanup of derived classes.

Protected Member Functions
unsigned	getIndex (int size, int lbd) const
	Calculates the index for a clause based on its size and LBD.
int	getSizeFromIndex (unsigned index) const
	Calculates the size of a clause from its index.
int	getLbdPartitionFromIndex (unsigned index) const
	Calculates the LBD partition from an index.

Protected Attributes
const size_t	m_totalLiteralCapacity
	Maximum total literal capacity of the database.
const int	m_maxPartitioningLbd
	Maximum LBD value for separate partitioning.
const int	m_maxClauseSize
	Maximum size of clauses to be stored.
const int	m_freeMaxSize
	Maximum size for which giveSelection does not count in while filling exportBuffer.
std::vector< std::unique_ptr< ClauseBuffer > >	m_clauses
	Vector of clause buffers, indexed by size and LBD.
std::atomic< long >	m_currentLiteralSize
	Current number of literals in the database (excluding unit clauses).
std::atomic< int >	m_currentWorstIndex
	Index of the current worst clause in the database.
std::shared_mutex	m_shrinkMutex
	Mutex used to coordinate shrinking and clause addition.
ClauseBuffer	m_missedAdditionsBfr

Detailed Description

A clause database implementation attempting to naively mimic the Simplified Adaptive Database from Mallob (ref:https://doi.org/10.1613/jair.1.15827).

This class implements a clause database that organizes clauses based on their size and LBD (Literal Block Distance). It uses a vector of ClauseBuffers to store clauses, with each buffer corresponding to a specific size and LBD range. The implementation aims to provide efficient clause storage, retrieval, and management while maintaining a balance between clause quality and database size.

Key features:

• Clauses are partitioned based on size and LBD.
• Supports concurrent additions with lock-free mechanisms for unit clauses.

• Implements a shrinking mechanism to maintain the database size within capacity.

  Todo

  fix the lbd partitioning to not have empty vectors, worth it ?

Constructor & Destructor Documentation

ClauseDatabaseMallob()

ClauseDatabaseMallob::ClauseDatabaseMallob ( int maxClauseSize, int maxPartitioningLbd, size_t maxCapacity, int maxFreeSize )

explicit

Constructs a new ClauseDatabaseMallob object.

Parameters

maxClauseSize	Maximum size of clauses to be stored.
maxPartitioningLbd	Maximum LBD value for separate partitioning.
maxCapacity	Maximum total literal capacity of the database.
maxFreeSize	Maximum size for which giveSelection does not decrement the literal count while filling the export buffer.

Exceptions

std::invalid_argument

if any parameter is invalid.

Member Function Documentation

addClause()

bool ClauseDatabaseMallob::addClause ( ClauseExchangePtr clause )

overridevirtual

Adds a clause to the database.

This method attempts to add a clause to the appropriate buffer based on its size and LBD. It uses shared locks for synchronizing the m_currentLiteralCounts and the other class atributes with shrinkDatabase. Units are always added, capacity is ignored for them.

Parameters

clause

pointer to the clause to be added.

Returns

true if the clause was successfully added, false otherwise.

Implements ClauseDatabase.

clearDatabase()

void ClauseDatabaseMallob::clearDatabase ( )

overridevirtual

Clears all clauses from the database and resets internal counters.

Implements ClauseDatabase.

getClauses()

void ClauseDatabaseMallob::getClauses ( std::vector< ClauseExchangePtr > & v_cls )

overridevirtual

Fills a buffer with all clauses in the database.

Parameters

v_cls

Vector to be filled with all clauses.

Implements ClauseDatabase.

getIndex()

unsigned ClauseDatabaseMallob::getIndex ( int size, int lbd ) const

inlineprotected

Calculates the index for a clause based on its size and LBD.

This function computes an index in the clauses vector based on the clause's size and LBD. It uses m_maxPartitioningLbd to determine the partitioning of LBD values.

Parameters

size	Size of the clause (must be >= UNIT_SIZE).
lbd	LBD (Literal Block Distance) of the clause (must be >= MIN_LBD).

Returns

Index in the clauses vector.

Exceptions

std::invalid_argument

if size is less than UNIT_SIZE or lbd is less than MIN_LBD.

Index calculation:

• For each size, there are m_maxPartitioningLbd possible indices.
• LBD values >= (MIN_LBD + m_maxPartitioningLbd) are grouped together in the last partition.

Example (assuming m_maxPartitioningLbd == 2):

• idx 0: size = 1, lbd = 2
• idx 1: size = 1, lbd >= 3 (never used)
• idx 2: size = 2, lbd = 2
• idx 3: size = 2, lbd >= 3 (never used)
• idx 4: size = 3, lbd = 2
• idx 5: size = 3, lbd >= 3 ...

getLbdPartitionFromIndex()

int ClauseDatabaseMallob::getLbdPartitionFromIndex ( unsigned index ) const

inlineprotected

Calculates the LBD partition from an index.

Parameters

index

Index in the clauses vector.

Returns

LBD partition.

getOneClause()

bool ClauseDatabaseMallob::getOneClause ( ClauseExchangePtr & cls )

overridevirtual

Retrieves a single clause from the best (smallest index) buffer possible.

This method attempts to retrieve a clause from any non-empty buffer in the database.

Parameters

cls	Reference to store the retrieved clause.

Returns

true if a clause was found, false if the database is empty.

Implements ClauseDatabase.

getSize()

size_t ClauseDatabaseMallob::getSize ( ) const

overridevirtual

Gets the total number of clauses in the database.

Returns

Number of clauses in the database.

Implements ClauseDatabase.

getSizeFromIndex()

int ClauseDatabaseMallob::getSizeFromIndex ( unsigned index ) const

inlineprotected

Calculates the size of a clause from its index.

Parameters

index

Index in the clauses vector.

Returns

Size of the clause.

giveSelection()

size_t ClauseDatabaseMallob::giveSelection ( std::vector< ClauseExchangePtr > & selectedCls, unsigned int literalCountLimit )

overridevirtual

Fills a buffer with selected clauses up to a given size limit.

This method selects clauses from the database, prioritizing unit clauses and then iterating through the clause buffers to fill the selection up to the specified limit.

Parameters

selectedCls	Vector to be filled with selected clauses.
literalCountLimit	Maximum number of literals to select.

Returns

Number of literals in the selected clauses.

Implements ClauseDatabase.

shrinkDatabase()

size_t ClauseDatabaseMallob::shrinkDatabase ( )

overridevirtual

Shrinks the database by removing clauses to maintain the size within capacity.

This method removes clauses from the worst (highest index) buffers until the database size is within the specified capacity. However it starts by adding missed clauses addition due to the previous shrink unique_lock. Unit clauses are never removed

Returns

Number of clauses removed during shrinking.

Implements ClauseDatabase.

---

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

• /github/workspace/src/containers/ClauseDatabaseMallob.hpp