MallobSharing Class Reference

Implements a global sharing strategy based on the Mallob algorithm. More...

#include <MallobSharing.hpp>

Inheritance diagram for MallobSharing:

Collaboration diagram for MallobSharing:

Public Member Functions
	MallobSharing (const std::shared_ptr< ClauseDatabase > &clauseDB, unsigned long baseBufferSize, unsigned long maxBufferSize, unsigned int lbdLimitAtImport, unsigned int sizeLimitAtImport, unsigned int roundsPerSecond, float maxCompensation, unsigned int resharePeriodMicroSec)
	Constructor for MallobSharing.
	~MallobSharing ()
	Destructor for MallobSharing.
bool	initMpiVariables () override
	Initializes MPI-related variables.
bool	doSharing () override
	Performs the clause sharing operation.
void	joinProcess (int winnerRank, SatResult res, const std::vector< int > &model) override
	Handles the process of joining when a solution is found.
bool	importClause (const ClauseExchangePtr &cls) override
	Imports a clause into the clause database.
std::chrono::microseconds	getSleepingTime () override
	Gets the sleeping time for the sharing strategy.
void	initializeFilter (unsigned int resharingPeriod, unsigned int sharingsPerSecond, unsigned int maxProducerId=63)
	Initializes the sharing filter with given parameters.
bool	doesClauseExist (const ClauseExchangePtr &cls) const
	Checks if a clause exists in the sharing map.
void	updateClause (const ClauseExchangePtr &cls)
	Updates the metadata for an existing clause.
bool	insertClause (const ClauseExchangePtr &cls)
	Inserts a new clause or updates an existing one in the sharing map.
bool	isClauseShared (const ClauseExchangePtr &cls) const
	Checks if a clause has been shared recently.
bool	canConsumerImportClause (const ClauseExchangePtr &cls, unsigned consumerId)
	Determines if a consumer can import a given clause.
void	incrementEpoch ()
	Increments the current epoch.
void	markClauseAsShared (ClauseExchangePtr &cls)
	Marks a clause as shared, updating its metadata.
size_t	shrinkFilter ()
	Shrinks the filter to remove entries of clauses that can be reshared. Once a clause was shared m_resharingPeriod rpochs back it can be reshared.
Public Member Functions inherited from GlobalSharingStrategy
	GlobalSharingStrategy (const std::shared_ptr< ClauseDatabase > &clauseDB, const std::vector< std::shared_ptr< SharingEntity > > &producers={}, const std::vector< std::shared_ptr< SharingEntity > > &consumers={})
	Constructor for GlobalSharingStrategy.
virtual	~GlobalSharingStrategy ()
	Destructor.
void	importClauses (const std::vector< ClauseExchangePtr > &v_cls) override
	Imports multiple clauses into the clause database.
void	printStats () override
	Prints the statistics of the sharing strategy.
Public Member Functions inherited from SharingStrategy
	SharingStrategy (const std::vector< std::shared_ptr< SharingEntity > > &producers, const std::vector< std::shared_ptr< SharingEntity > > &consumers, const std::shared_ptr< ClauseDatabase > &clauseDB)
	Constructor for SharingStrategy. Be sure to call connectConstructorProducers after construction, this is due to the base class shared_from_this.
virtual	~SharingStrategy ()
	Virtual destructor.
void	connectConstructorProducers ()
	Add this to the producers' clients list.
virtual void	addProducer (std::shared_ptr< SharingEntity > producer)
	Adds a producer to this strategy.
virtual void	connectProducer (std::shared_ptr< SharingEntity > producer)
	Connect a producer to this strategy. Add (this) to clients of (producer)
virtual void	removeProducer (std::shared_ptr< SharingEntity > producer)
	Removes a producer from this strategy.
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.

Protected Member Functions
bool	exportClauseToClient (const ClauseExchangePtr &clause, std::shared_ptr< SharingEntity > client) override
	Exports a clause to a specific client.
void	deserializeClauses (const std::vector< int > &serialized_v_cls)
	Deserializes received clauses.
int	mergeSerializedBuffersWithMine (std::vector< std::reference_wrapper< std::vector< int > > > &buffers, std::vector< int > &result, size_t &nonFreeLiteralsCount)
	Merges serialized buffers with local clauses from the m_clauseDB database.
void	computeBufferSize (unsigned int aggregationsCount)
	Computes the buffer size based on the number of aggregations.
bool	getOneClauseWrapper (ClauseExchangePtr &cls)
	Wrapper for getting one clause from the database. This remove the need to make the filter thread-safe.
void	computeCompensation ()
	Computes the compensation factor for volume balancing.
Protected Member Functions inherited from SharingStrategy
bool	exportClauseToClient (const ClauseExchangePtr &clause, std::shared_ptr< SharingEntity > client) override
	A SharingStrategy doesn't send a clause to the source client (->from must store the sharingId of its producer)
Protected Member Functions inherited from SharingEntity
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.

Protected Attributes
unsigned int	defaultBufferSize
	Default size of the sharing buffer.
const unsigned int	baseSize
	Base size for buffer calculations.
const unsigned int	maxSize
	Maximum size for buffer calculations.
std::vector< std::reference_wrapper< std::vector< int > > >	buffers
	Buffers for clause sharing.
std::vector< int >	clausesToSendSerialized
	Buffer for serialized clauses to send.
std::vector< int >	receivedClausesLeft
	Buffer for clauses received from left child.
std::vector< int >	receivedClausesRight
	Buffer for clauses received from right child.
std::vector< int >	receivedClausesFather
	Buffer for clauses received from parent.
std::vector< ClauseExchangePtr >	deserializedClauses
	Buffer for deserialized clauses.
Bitset	myBitVector
	Bitset for tracking shared clauses.
int	father
	MPI rank of the parent node.
int	left_child
	MPI rank of the left child.
int	right_child
	MPI rank of the right child.
int	nb_children
	Number of children nodes.
size_t	sleepTime
	Sleep time between sharing operations.
bool	addChildClauses
	Flag to determine if child clauses should be added.
const int	lbdLimitAtImport
	LBD limit for clause import.
const int	sizeLimitAtImport
	Size limit for clause import.
unsigned	m_freeSize
	Clause size not counted in the buffer at serialization.
float	accumulatedAdmittedLiterals
	Accumulated number of literals shared to parent.
float	accumulatedDesiredLiterals
	Accumulated number of literals received from children.
size_t	lastEpochAdmittedLits
	Number of literals in last epoch final buffer.
size_t	lastEpochReceivedLits
	Number of literals received in last epoch.
float	compensationFactor
	Factor for volume compensation.
float	maxCompensationFactor
	Maximum Compensation factor.
float	estimatedIncomingLits
	Estimated number of incoming literals.
float	estimatedSharedLits
	Estimated number of shared literals.
Protected Attributes inherited from GlobalSharingStrategy
GlobalSharingStatistics	gstats
	Statistics for global sharing.
bool	requests_sent
	Flag indicating if requests to end were sent to the root.
std::vector< MPI_Request >	recv_end_requests
	MPI requests for non-blocking receive of end signals.
MPI_Request	send_end_request
	MPI request for non-root Isend for final synchronization with root.
std::vector< int >	receivedFinalResultRoot
	Buffer for storing results received from other mpi processes.
Protected Attributes inherited from SharingStrategy
std::shared_ptr< ClauseDatabase >	m_clauseDB
	Clause database where exported clauses are stored.
SharingStatistics	stats
	Sharing statistics.
std::vector< std::weak_ptr< SharingEntity > >	m_producers
	The set holding the references to the producers.
std::shared_mutex	m_producersMutex
	Shared mutex for producers list (to become RCU ?)
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.

Detailed Description

Implements a global sharing strategy based on the Mallob algorithm.

This class extends GlobalSharingStrategy to implement a specific sharing mechanism inspired by the Mallob algorithm for distributed SAT solving (ref:https://doi.org/10.1613/jair.1.15827).

Constructor & Destructor Documentation

MallobSharing()

MallobSharing::MallobSharing	(	const std::shared_ptr< ClauseDatabase > &	clauseDB,
		unsigned long	baseBufferSize,
		unsigned long	maxBufferSize,
		unsigned int	lbdLimitAtImport,
		unsigned int	sizeLimitAtImport,
		unsigned int	roundsPerSecond,
		float	maxCompensation,
		unsigned int	resharePeriodMicroSec )

Constructor for MallobSharing.

Parameters

clauseDB	Shared pointer to the clause database.
baseBufferSize	The base size of the buffer in computation
maxBufferSize	The maxmimum size of the buffer in computation
lbdLimitAtImport	The maximum lbd value of imported clauses
sizeLimitAtImport	The maximum size of imported clauses
roundsPerSecond	The number of sharings done in a second
maxCompensation	The maximum compensation factor
resharePeriodMicroSec	The resharing period for the exact filter

Member Function Documentation

canConsumerImportClause()

bool MallobSharing::canConsumerImportClause	(	const ClauseExchangePtr &	cls,
		unsigned	consumerId )

Determines if a consumer can import a given clause.

Parameters

cls	Pointer to the clause to check.
consumerId	ID of the consumer attempting to import the clause.

Returns

true if the consumer can import the clause, false otherwise.

Checks if the clause is in the filter (produced but not shared) and if the consumer was not one of its producers.

computeBufferSize()

void MallobSharing::computeBufferSize ( unsigned int aggregationsCount )

protected

Computes the buffer size based on the number of aggregations.

Parameters

aggregationsCount

The number of aggregations.

deserializeClauses()

void MallobSharing::deserializeClauses ( const std::vector< int > & serialized_v_cls )

protected

Deserializes received clauses.

Parameters

serialized_v_cls

Vector containing the serialized clauses.

doesClauseExist()

bool MallobSharing::doesClauseExist

(

const ClauseExchangePtr &

cls

)

const

Checks if a clause exists in the sharing map.

Parameters

cls	Pointer to the clause to check.

Returns

true if the clause is present in the map, false otherwise.

doSharing()

bool MallobSharing::doSharing ( )

overridevirtual

Performs the clause sharing operation.

Returns

true if sharing is complete and the process can terminate, false otherwise.

Reimplemented from GlobalSharingStrategy.

exportClauseToClient()

bool MallobSharing::exportClauseToClient ( const ClauseExchangePtr & clause, std::shared_ptr< SharingEntity > client )

overrideprotectedvirtual

Exports a clause to a specific client.

Parameters

clause	Pointer to the clause to be exported.
client	Shared pointer to the client receiving the clause.

Returns

true if the clause was successfully exported, false otherwise.

Reimplemented from GlobalSharingStrategy.

getOneClauseWrapper()

bool MallobSharing::getOneClauseWrapper ( ClauseExchangePtr & cls )

inlineprotected

Wrapper for getting one clause from the database. This remove the need to make the filter thread-safe.

Parameters

cls	Output parameter to store the retrieved clause.

Returns

true if a clause was successfully retrieved, false otherwise.

getSleepingTime()

std::chrono::microseconds MallobSharing::getSleepingTime ( )

overridevirtual

Gets the sleeping time for the sharing strategy.

Returns

The sleeping time in microseconds.

Reimplemented from GlobalSharingStrategy.

importClause()

bool MallobSharing::importClause ( const ClauseExchangePtr & cls )

overridevirtual

Imports a clause into the clause database.

Parameters

cls	Pointer to the clause to be imported.

Returns

true if the clause was successfully imported, false otherwise.

Reimplemented from GlobalSharingStrategy.

initializeFilter()

void MallobSharing::initializeFilter	(	unsigned int	resharingPeriod,
		unsigned int	sharingsPerSecond,
		unsigned int	maxProducerId = 63 )

Initializes the sharing filter with given parameters.

Parameters

resharingPeriod	Period in microseconds before a clause can be reshared.
sharingsPerSecond	Number of sharing operations per second.
maxProducerId	Maximum ID for producers (default 63, as we use a 64-bit integer for tracking).

Exceptions

std::invalid_argument

If maxProducerId > 63 or sharingsPerSecond == 0.

initMpiVariables()

bool MallobSharing::initMpiVariables ( )

overridevirtual

Initializes MPI-related variables.

Returns

true if initialization was successful, false otherwise.

Reimplemented from GlobalSharingStrategy.

insertClause()

bool MallobSharing::insertClause

(

const ClauseExchangePtr &

cls

)

Inserts a new clause or updates an existing one in the sharing map.

Parameters

cls	Pointer to the clause to insert or update.

Returns

true if the clause was newly inserted, false if it was updated.

If the clause doesn't exist:

• Sets sharingEpoch to -resharingPeriodInEpochs
• Initializes the sources bitset with the clause's origin
• Sets productionEpoch to the current epoch If the clause exists:
• Updates the existing clause information

isClauseShared()

bool MallobSharing::isClauseShared

(

const ClauseExchangePtr &

cls

)

const

Checks if a clause has been shared recently.

Parameters

cls	Pointer to the clause to check.

Returns

true if the clause is in the map and (currentEpoch - sharingEpoch <= resharingPeriod), false otherwise.

Note

The condition is always true for newly inserted clauses due to sharingEpoch initialization. This allows resharing of clauses not yet removed from the filter.

joinProcess()

void MallobSharing::joinProcess ( int winnerRank, SatResult res, const std::vector< int > & model )

overridevirtual

Handles the process of joining when a solution is found.

Parameters

winnerRank	The rank of the process that found the solution.
res	The result of the SAT solving process.
model	The satisfying assignment, if any.

Reimplemented from GlobalSharingStrategy.

markClauseAsShared()

void MallobSharing::markClauseAsShared

(

ClauseExchangePtr &

cls

)

Marks a clause as shared, updating its metadata.

Parameters

cls	Pointer to the clause to mark as shared.

Updates the shared epoch to the current epoch and resets the sources bitset to 0.

mergeSerializedBuffersWithMine()

int MallobSharing::mergeSerializedBuffersWithMine ( std::vector< std::reference_wrapper< std::vector< int > > > & buffers, std::vector< int > & result, size_t & nonFreeLiteralsCount )

protected

Merges serialized buffers with local clauses from the m_clauseDB database.

Serialization Pattern ([size][lbd][literals])*

Parameters

buffers	Vector of references to buffers containing serialized clauses.
result	Vector to store the merged result.
nonFreeLiteralsCount	Output parameter to store the count of non-free literals.

Returns

The number of clauses merged.

shrinkFilter()

size_t MallobSharing::shrinkFilter

(

)

Shrinks the filter to remove entries of clauses that can be reshared. Once a clause was shared m_resharingPeriod rpochs back it can be reshared.

Returns

The number of entries removed from the filter.

updateClause()

void MallobSharing::updateClause

(

const ClauseExchangePtr &

cls

)

Updates the metadata for an existing clause.

Parameters

cls	Pointer to the clause to update.

Note

Updates the sources bitset and sets the production epoch to the current epoch.

---

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

• /github/workspace/src/sharing/GlobalStrategies/MallobSharing.hpp