#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

Detailed Description

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

Definition at line 300 of file clause.h.

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 302 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 307 of file clause.h.

◆ clause

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

Definition at line 320 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 318 of file clause.h.

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

ortools/sat/clause.h

Public Member Functions

Public Attributes