#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) ABSL_LOCKS_EXCLUDED(mutex_)

bool	Delete (absl::Span< const int > clause) ABSL_LOCKS_EXCLUDED(mutex_)

CompactVectorVector< int >	NextBatch () ABSL_LOCKS_EXCLUDED(mutex_)

int	FillUpstreamBuffer (UniqueClauseStream &upstream, int clause_size, int max_clauses_to_export) ABSL_LOCKS_EXCLUDED(mutex_)

int	NumBufferedLiteralsOfSize (int size) const ABSL_LOCKS_EXCLUDED(mutex_)

int	NumBufferedLiterals () const ABSL_LOCKS_EXCLUDED(mutex_)

bool	CanAccept (int size, int lbd) const

void	RemoveWorstClauses ()

int	lbd_threshold () const ABSL_LOCKS_EXCLUDED(mutex_)

void	set_lbd_threshold (int lbd) ABSL_LOCKS_EXCLUDED(mutex_)

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	kMaxLiteralsPerBatch = 4096 / sizeof(int)
	Export 4KiB of clauses per batch.

static constexpr int	kMaxBufferedLiterals = kMaxLiteralsPerBatch

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 class is thread-safe, the idea is to have one per worker plus a global one to deduplicate between workers to minimize contention.

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 we never overfill the "global" stream, and if we drop a clause on a worker, one of the following will most likely happen:

Some other worker learns the clause and shares it later.
All other workers also learn and drop the clause.
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.

Definition at line 638 of file synchronization.h.

Constructor & Destructor Documentation

◆ UniqueClauseStream() [1/3]

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

Definition at line 1130 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 )

Adds the clause to a future batch and returns true if the clause was added. Otherwise returns false. This may return false if the buffer is full. It will not block the clause if it is dropped to avoid unbounded growth of the hash table.

This is just a safety check, the caller should have called CanAccept().

Definition at line 1136 of file synchronization.cc.

◆ CanAccept()

bool operations_research::sat::UniqueClauseStream::CanAccept	(	int	size,
		int	lbd ) const

Returns true if the stream can accept a clause of the specified size and LBD without dropping it.

Definition at line 1209 of file synchronization.cc.

◆ Delete()

bool operations_research::sat::UniqueClauseStream::Delete ( absl::Span< const int > clause )

Lazily deletes a clause with the same hash, returns true if it was present. The deleted clause will not be exported (either via NextBatch or FillUpstreamBuffer). A clause with the same hash may be re-added after calling Delete. If another clause with the same hash is added before the deleted clause is emitted then both clauses may be emitted.

Note a clause with this hash may be buffered, but not yet exported.

Definition at line 1157 of file synchronization.cc.

◆ FillUpstreamBuffer()

int operations_research::sat::UniqueClauseStream::FillUpstreamBuffer	(	UniqueClauseStream &	upstream,
		int	clause_size,
		int	max_clauses_to_export )

Adds up to max_clauses_to_export clauses of a given size to upstream and removes them from the internal buffer.

Don't emit deleted clauses.

Definition at line 1183 of file synchronization.cc.

◆ 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 1245 of file synchronization.cc.

◆ lbd_threshold()

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

inline

Definition at line 695 of file synchronization.h.

◆ NextBatch()

CompactVectorVector< int > operations_research::sat::UniqueClauseStream::NextBatch ( )

Returns a set of clauses totalling up to kMaxLiteralsPerBatch and removes exported clauses from the internal buffer.

Definition at line 1164 of file synchronization.cc.

◆ NumBufferedLiterals()

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

Definition at line 1200 of file synchronization.cc.

◆ NumBufferedLiteralsOfSize()

int operations_research::sat::UniqueClauseStream::NumBufferedLiteralsOfSize ( int size ) const

inline

Returns the number of literals in the buffer in clauses with size <= max_size.

Definition at line 679 of file synchronization.h.

◆ RemoveWorstClauses()

void operations_research::sat::UniqueClauseStream::RemoveWorstClauses ( )

Delete longest clauses while keeping at least kMaxBufferedLiterals. This guarantees that CanAccept will return the same result as before, and at least the next batch will contain the same clauses, but we will emit fewer old, long clauses in the future.

Stop if removing one more clause of the current size would leave the buffer under full. Otherwise we might remove a shorter clause later!

Definition at line 1220 of file synchronization.cc.

◆ set_lbd_threshold()

void operations_research::sat::UniqueClauseStream::set_lbd_threshold ( int lbd )

Definition at line 1240 of file synchronization.cc.

Member Data Documentation

◆ kMaxBufferedLiterals

int operations_research::sat::UniqueClauseStream::kMaxBufferedLiterals = kMaxLiteralsPerBatch

staticconstexpr

Bound the total literals we buffer, approximately enforced so shorter clauses can replace longer ones. This can be larger than kMaxLiteralsPerBatch (hence the separate constant), but experiments suggest that this doesn't help.

Definition at line 648 of file synchronization.h.

◆ kMaxClauseSize

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

staticconstexpr

Definition at line 641 of file synchronization.h.

◆ kMaxLiteralsPerBatch

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

staticconstexpr

Export 4KiB of clauses per batch.

Definition at line 643 of file synchronization.h.

◆ kMinClauseSize

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

staticconstexpr

Definition at line 640 of file synchronization.h.

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

ortools/sat/synchronization.h
ortools/sat/synchronization.cc

Public Member Functions

Static Public Member Functions

Static Public Attributes

Detailed Description

Constructor & Destructor Documentation

◆ UniqueClauseStream() [1/3]

◆ UniqueClauseStream() [2/3]

◆ UniqueClauseStream() [3/3]

Member Function Documentation

◆ Add()

◆ CanAccept()

◆ Delete()

◆ FillUpstreamBuffer()

◆ HashClause()

◆ lbd_threshold()

◆ NextBatch()

◆ NumBufferedLiterals()

◆ NumBufferedLiteralsOfSize()

◆ RemoveWorstClauses()

◆ set_lbd_threshold()

Member Data Documentation

◆ kMaxBufferedLiterals

◆ kMaxClauseSize

◆ kMaxLiteralsPerBatch

◆ kMinClauseSize