3#include "GlobalSharingStrategy.hpp"
23 AllGatherSharing(
const std::shared_ptr<ClauseDatabase>& clauseDB,
unsigned long bufferSize);
Implements a global sharing strategy using MPI_Allgather for clause exchange.
Definition AllGatherSharing.hpp:16
bool initMpiVariables() override
Initializes MPI-related variables.
void joinProcess(int winnerRank, SatResult res, const std::vector< int > &model) override
Handles the process of joining when a solution is found.
int color
Color used for MPI communicator splitting.
Definition AllGatherSharing.hpp:71
~AllGatherSharing()
Destructor for AllGatherSharing.
void deserializeClauses(const std::vector< int > &serialized_v_cls, int num_buffers)
Deserializes received clauses.
AllGatherSharing(const std::shared_ptr< ClauseDatabase > &clauseDB, unsigned long bufferSize)
Constructor for AllGatherSharing.
int serializeClauses(std::vector< int > &serialized_v_cls)
Serializes clauses for sharing.
std::vector< int > clausesToSendSerialized
Buffer for serialized clauses to send.
Definition AllGatherSharing.hpp:73
bool doSharing() override
Performs the clause sharing operation. A group is created for the process willing to shared only....
BloomFilter b_filter
Bloom filter for duplicate clause detection.
Definition AllGatherSharing.hpp:76
std::vector< int > receivedClauses
Buffer for received serialized clauses.
Definition AllGatherSharing.hpp:74
int totalSize
Total size of the buffer for clause sharing.
Definition AllGatherSharing.hpp:70
Definition BloomFilter.hpp:24
Base class for global clause sharing strategies across MPI processes.
Definition GlobalSharingStrategy.hpp:27
SatResult
Enumeration for SAT solver results.
Definition SolverInterface.hpp:39