operations_research::sat::ClauseManager::Watcher Struct Reference

Detailed Description

Contains, for each literal, the list of clauses that need to be inspected when the corresponding literal becomes false.

Definition at line 301 of file clause.h.

#include <clause.h>

Public Member Functions
	Watcher ()=default
	Watcher (SatClause *c, Literal b, int i=2)

Public Attributes
Literal	blocking_literal
int32_t	start_index
SatClause *	clause

Constructor & Destructor Documentation

Watcher() [1/2]

operations_research::sat::ClauseManager::Watcher::Watcher ( )

default

Watcher() [2/2]

operations_research::sat::ClauseManager::Watcher::Watcher ( SatClause * c, Literal b, int i = 2 )

inline

Definition at line 303 of file clause.h.

Member Data Documentation

blocking_literal

Literal operations_research::sat::ClauseManager::Watcher::blocking_literal

Optimization. A literal from the clause that sometimes allow to not even look at the clause memory when true.

Definition at line 308 of file clause.h.

clause

SatClause* operations_research::sat::ClauseManager::Watcher::clause

Definition at line 321 of file clause.h.

start_index

int32_t operations_research::sat::ClauseManager::Watcher::start_index

Optimization. An index in the clause. Instead of looking for another literal to watch from the start, we will start from here instead, and loop around if needed. This allows to avoid bad quadratic corner cases and lead to an "optimal" complexity. See "Optimal Implementation of Watched Literals and more General Techniques", Ian P. Gent.

Note

ideally, this should be part of a SatClause, so it can be shared across watchers. However, since we have 32 bits for "free" here because of the struct alignment, we store it here instead.

Definition at line 319 of file clause.h.

---

The documentation for this struct was generated from the following file:

• ortools/sat/clause.h