![]() |
Google OR-Tools v9.14
a fast and portable software suite for combinatorial optimization
|
Emit a stream of clauses in batches without duplicates. Each batch has a fixed number of literals, containing the smallest clauses added. It has a finite size internal buffer that is a small multiple of the batch size.
This uses a finite buffer, so some clauses may be dropped if we generate too many more than we export, but that is rarely a problem because if we drop a clause on a worker, one of the following will most likely happen:
Definition at line 637 of file synchronization.h.
#include <synchronization.h>
Public Member Functions | |
UniqueClauseStream () | |
UniqueClauseStream (const UniqueClauseStream &)=delete | |
Move only - this is an expensive class to copy. | |
UniqueClauseStream (UniqueClauseStream &&)=default | |
bool | Add (absl::Span< const int > clause, int lbd=2) |
bool | BlockClause (absl::Span< const int > clause) |
CompactVectorVector< int > | NextBatch () |
void | ClearFingerprints () |
int | NumLiteralsOfSize (int size) const |
Returns the number of buffered literals in clauses of a given size. | |
int | NumBufferedLiterals () const |
int | lbd_threshold () const |
void | set_lbd_threshold (int lbd_threshold) |
Static Public Member Functions | |
static size_t | HashClause (absl::Span< const int > clause, size_t hash_seed=0) |
Computes a hash that is independent of the order of literals in the clause. |
Static Public Attributes | |
static constexpr int | kMinClauseSize = 3 |
static constexpr int | kMaxClauseSize = 32 |
static constexpr int | kMinLbd = 2 |
static constexpr int | kMaxLbd = 5 |
static constexpr int | kMaxLiteralsPerBatch = 4096 / sizeof(int) |
Export 4KiB of clauses per batch. |
operations_research::sat::UniqueClauseStream::UniqueClauseStream | ( | ) |
Definition at line 1131 of file synchronization.cc.
|
delete |
Move only - this is an expensive class to copy.
|
default |
bool operations_research::sat::UniqueClauseStream::Add | ( | absl::Span< const int > | clause, |
int | lbd = 2 ) |
Adds the clause to a future batch and returns true if the clause is new, otherwise returns false.
Maybe replace an old buffered clause of the same size if it has a smaller hash value. This means that the buffer will contain a deterministic sample of the clauses added independent of insertion order.
Definition at line 1138 of file synchronization.cc.
bool operations_research::sat::UniqueClauseStream::BlockClause | ( | absl::Span< const int > | clause | ) |
Stop a clause being added to future batches. Returns true if the clause is new. This is approximate and can have false positives and negatives, it is still guaranteed to prevent adding the same clause twice to the next batch.
Definition at line 1160 of file synchronization.cc.
|
inline |
Definition at line 667 of file synchronization.h.
|
static |
Computes a hash that is independent of the order of literals in the clause.
Definition at line 1213 of file synchronization.cc.
|
inline |
Definition at line 677 of file synchronization.h.
CompactVectorVector< int > operations_research::sat::UniqueClauseStream::NextBatch | ( | ) |
Returns a set of clauses totalling up to kMaxLiteralsPerBatch and clears the internal buffer. Increases the LBD threshold if the batch is underfull, and decreases it if too many clauses were dropped.
Definition at line 1168 of file synchronization.cc.
int operations_research::sat::UniqueClauseStream::NumBufferedLiterals | ( | ) | const |
Definition at line 1205 of file synchronization.cc.
int operations_research::sat::UniqueClauseStream::NumLiteralsOfSize | ( | int | size | ) | const |
Returns the number of buffered literals in clauses of a given size.
Definition at line 1236 of file synchronization.cc.
|
inline |
Definition at line 678 of file synchronization.h.
|
staticconstexpr |
Definition at line 640 of file synchronization.h.
|
staticconstexpr |
Definition at line 642 of file synchronization.h.
|
staticconstexpr |
Export 4KiB of clauses per batch.
Definition at line 644 of file synchronization.h.
|
staticconstexpr |
Definition at line 639 of file synchronization.h.
|
staticconstexpr |
Definition at line 641 of file synchronization.h.