Google OR-Tools v9.14
a fast and portable software suite for combinatorial optimization
Loading...
Searching...
No Matches
operations_research::sat::UniqueClauseStream Class Reference

Detailed Description

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:

  1. Some other worker learns the clause and shares it later.
  2. All other workers also learn and drop the clause.
  3. No other worker learns the clause, so it was not that helpful anyway.
Note
this uses literals as encoded in a cp_model.proto. Thus, the literals can be negative numbers.
Todo
(user): This class might not want to live in this file now it no longer needs to be thread-safe.

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.

Constructor & Destructor Documentation

◆ UniqueClauseStream() [1/3]

operations_research::sat::UniqueClauseStream::UniqueClauseStream ( )

Definition at line 1131 of file synchronization.cc.

◆ UniqueClauseStream() [2/3]

operations_research::sat::UniqueClauseStream::UniqueClauseStream ( const UniqueClauseStream & )
delete

Move only - this is an expensive class to copy.

◆ UniqueClauseStream() [3/3]

operations_research::sat::UniqueClauseStream::UniqueClauseStream ( UniqueClauseStream && )
default

Member Function Documentation

◆ Add()

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.

◆ BlockClause()

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.

◆ ClearFingerprints()

void operations_research::sat::UniqueClauseStream::ClearFingerprints ( )
inline

Definition at line 667 of file synchronization.h.

◆ HashClause()

size_t operations_research::sat::UniqueClauseStream::HashClause ( absl::Span< const int > clause,
size_t hash_seed = 0 )
static

Computes a hash that is independent of the order of literals in the clause.

Definition at line 1213 of file synchronization.cc.

◆ lbd_threshold()

int operations_research::sat::UniqueClauseStream::lbd_threshold ( ) const
inline

Definition at line 677 of file synchronization.h.

◆ NextBatch()

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.

◆ NumBufferedLiterals()

int operations_research::sat::UniqueClauseStream::NumBufferedLiterals ( ) const

Definition at line 1205 of file synchronization.cc.

◆ NumLiteralsOfSize()

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.

◆ set_lbd_threshold()

void operations_research::sat::UniqueClauseStream::set_lbd_threshold ( int lbd_threshold)
inline

Definition at line 678 of file synchronization.h.

Member Data Documentation

◆ kMaxClauseSize

int operations_research::sat::UniqueClauseStream::kMaxClauseSize = 32
staticconstexpr

Definition at line 640 of file synchronization.h.

◆ kMaxLbd

int operations_research::sat::UniqueClauseStream::kMaxLbd = 5
staticconstexpr

Definition at line 642 of file synchronization.h.

◆ kMaxLiteralsPerBatch

int operations_research::sat::UniqueClauseStream::kMaxLiteralsPerBatch = 4096 / sizeof(int)
staticconstexpr

Export 4KiB of clauses per batch.

Definition at line 644 of file synchronization.h.

◆ kMinClauseSize

int operations_research::sat::UniqueClauseStream::kMinClauseSize = 3
staticconstexpr

Definition at line 639 of file synchronization.h.

◆ kMinLbd

int operations_research::sat::UniqueClauseStream::kMinLbd = 2
staticconstexpr

Definition at line 641 of file synchronization.h.

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