HordeSatSharing Class Reference

This strategy is a HordeSat-like sharing strategy. More...

#include <HordeSatSharing.hpp>

Inheritance diagram for HordeSatSharing:

Collaboration diagram for HordeSatSharing:

Public Member Functions
	HordeSatSharing (const std::shared_ptr< ClauseDatabase > &clauseDB, unsigned long literalsPerProducerPerRound, unsigned int initialLbdLimit, unsigned int roundsBeforeLbdIncrease, const std::vector< std::shared_ptr< SharingEntity > > &producers={}, const std::vector< std::shared_ptr< SharingEntity > > &consumers={})
	Constructor for HordeSatSharing.
	~HordeSatSharing ()
	Destructor for HordeSatSharing.
bool	importClause (const ClauseExchangePtr &clause) override
	Imports a single clause if the lbd limit is respected. And updates the amount of literals exprted by the producer for the coming round.
void	importClauses (const std::vector< ClauseExchangePtr > &v_clauses) override
	Imports multiple clauses.
bool	doSharing () override
	Performs the sharing operation. It checks the literal production to decide if the lbd limit should be increased, decreased or unchanged. The selection of clauses from the database is exported to all consumers.
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.
virtual std::chrono::microseconds	getSleepingTime ()
	Determines the sleeping time for the sharer.
virtual void	printStats ()
	Prints the statistics of the strategy.
void	connectConstructorProducers ()
	Add this to the producers' clients list.
virtual void	connectProducer (std::shared_ptr< SharingEntity > producer)
	Connect a producer to this strategy. Add (this) to clients of (producer)
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
void	addProducer (std::shared_ptr< SharingEntity > producer) override
	Adds a producer to the sharing strategy. It initializes the lbd limit and the per round literal production for the producer.
void	removeProducer (std::shared_ptr< SharingEntity > producer) override
	Removes a producer from the sharing strategy.
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 long	literalPerRound
	Number of shared literals per round.
unsigned int	initialLbdLimit
	Initial lbd value for per producer filter.
unsigned int	roundBeforeIncrease
	Number of rounds before forcing an increase in production.
int	round
	Round Number.
std::vector< ClauseExchangePtr >	selection
	Used to manipulate clauses (as a member to reduce number of allocations).
std::unordered_map< unsigned int, std::atomic< unsigned int > >	lbdLimitPerProducer
	SharingEntity id to lbdLimit.
std::unordered_map< unsigned int, std::atomic< unsigned long > >	literalsPerProducer
	Metadata for clause database.
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.

Static Protected Attributes
static constexpr int	UNDER_UTILIZATION_THRESHOLD = 75
static constexpr int	OVER_UTILIZATION_THRESHOLD = 98

Detailed Description

This strategy is a HordeSat-like sharing strategy.

Todo

Strengthening strategy + keep units for future ones in derived classes?

Constructor & Destructor Documentation

HordeSatSharing()

HordeSatSharing::HordeSatSharing	(	const std::shared_ptr< ClauseDatabase > &	clauseDB,
		unsigned long	literalsPerProducerPerRound,
		unsigned int	initialLbdLimit,
		unsigned int	roundsBeforeLbdIncrease,
		const std::vector< std::shared_ptr< SharingEntity > > &	producers = {},
		const std::vector< std::shared_ptr< SharingEntity > > &	consumers = {} )

Constructor for HordeSatSharing.

Parameters

clauseDB	Shared pointer to the clause database.
producers	Vector of shared pointers to producer entities.
consumers	Vector of shared pointers to consumer entities.
literalsPerProducerPerRound	Number of literals a producer should export to this strategy per round
initialLbdLimit	The initial value of the maximum allowed lbd value for a given producer
roundsBeforeLbdIncrease	The number of rounds to wait before updating the lbd limit of the producers

Member Function Documentation

addProducer()

void HordeSatSharing::addProducer ( std::shared_ptr< SharingEntity > producer )

inlineoverrideprotectedvirtual

Adds a producer to the sharing strategy. It initializes the lbd limit and the per round literal production for the producer.

Parameters

producer

Shared pointer to the producer entity to be added.

Reimplemented from SharingStrategy.

doSharing()

bool HordeSatSharing::doSharing ( )

overridevirtual

Performs the sharing operation. It checks the literal production to decide if the lbd limit should be increased, decreased or unchanged. The selection of clauses from the database is exported to all consumers.

Returns

True if sharing is complete or should be terminated, false otherwise.

Implements SharingStrategy.

importClause()

bool HordeSatSharing::importClause ( const ClauseExchangePtr & clause )

overridevirtual

Imports a single clause if the lbd limit is respected. And updates the amount of literals exprted by the producer for the coming round.

Parameters

clause

Pointer to the clause to be imported.

Returns

True if the clause was successfully imported, false otherwise.

Implements SharingEntity.

importClauses()

void HordeSatSharing::importClauses ( const std::vector< ClauseExchangePtr > & v_clauses )

inlineoverridevirtual

Imports multiple clauses.

Parameters

v_clauses

Vector of clause pointers to be imported.

Implements SharingEntity.

removeProducer()

void HordeSatSharing::removeProducer ( std::shared_ptr< SharingEntity > producer )

inlineoverrideprotectedvirtual

Removes a producer from the sharing strategy.

Parameters

producer

Shared pointer to the producer entity to be removed.

Reimplemented from SharingStrategy.

---

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

• /github/workspace/src/sharing/LocalStrategies/HordeSatSharing.hpp