Painless
A framework to ease parallelization of sequential CDCL SAT solvers
Loading...
Searching...
No Matches
AllGatherSharing.hpp
1#pragma once
2
3#include "GlobalSharingStrategy.hpp"
4
16{
17 public:
23 AllGatherSharing(const std::shared_ptr<ClauseDatabase>& clauseDB, unsigned long bufferSize);
24
29
38 bool doSharing() override;
39
44 bool initMpiVariables() override;
45
52 void joinProcess(int winnerRank, SatResult res, const std::vector<int>& model) override;
53
54 protected:
61 int serializeClauses(std::vector<int>& serialized_v_cls);
62
68 void deserializeClauses(const std::vector<int>& serialized_v_cls, int num_buffers);
69
71 int color;
72
73 std::vector<int> clausesToSendSerialized;
74 std::vector<int> receivedClauses;
75
77};
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