operations_research::sat::ProtoTrail Class Reference

#include <work_assignment.h>

Public Member Functions
	ProtoTrail ()
void	PushLevel (const ProtoLiteral &decision, IntegerValue objective_lb, int node_id)
	Adds a new assigned level to the trail.
void	SetLevelImplied (int level)
	Asserts that the decision at level is implied by earlier decisions.
void	Clear ()
	Clear the trail, removing all levels.
void	SetObjectiveLb (int level, IntegerValue objective_lb)
	Set a lower bound on the objective at level.
int	MaxLevel () const
	Returns the maximum decision level stored in the trail.
ProtoLiteral	Decision (int level) const
	Returns the decision assigned at level.
absl::Span< const int >	NodeIds (int level) const
	Returns the node ids for decisions and implications at level.
absl::Span< const ProtoLiteral >	Implications (int level) const
void	AddImplication (int level, ProtoLiteral implication)
IntegerValue	ObjectiveLb (int level) const
absl::Span< const ProtoLiteral >	Literals () const
const std::vector< ProtoLiteral > &	TargetPhase () const
void	ClearTargetPhase ()
bool	AddPhase (const ProtoLiteral &lit)
	Appends a literal to the target phase, returns false if the phase is full.
void	SetTargetPhase (absl::Span< const ProtoLiteral > phase)

Detailed Description

ProtoTrail acts as an intermediate datastructure that can be synced with the shared tree and the local Trail as appropriate. It's intended that you sync a ProtoTrail with the tree on restart or when a subtree is closed, and with the local trail after propagation. Specifically it stores objective lower bounds, and literals that have been branched on and later proven to be implied by the prior decisions (i.e. they can be enqueued at this level).

Todo

(user): It'd be good to store an earlier level at which implications may be propagated.

Definition at line 104 of file work_assignment.h.

Constructor & Destructor Documentation

ProtoTrail()

operations_research::sat::ProtoTrail::ProtoTrail

(

)

Definition at line 147 of file work_assignment.cc.

Member Function Documentation

AddImplication()

void operations_research::sat::ProtoTrail::AddImplication ( int level, ProtoLiteral implication )

inline

Definition at line 137 of file work_assignment.h.

AddPhase()

bool operations_research::sat::ProtoTrail::AddPhase ( const ProtoLiteral & lit )

inline

Appends a literal to the target phase, returns false if the phase is full.

Definition at line 154 of file work_assignment.h.

Clear()

void operations_research::sat::ProtoTrail::Clear

(

)

Clear the trail, removing all levels.

Definition at line 187 of file work_assignment.cc.

ClearTargetPhase()

void operations_research::sat::ProtoTrail::ClearTargetPhase ( )

inline

Definition at line 152 of file work_assignment.h.

Decision()

ProtoLiteral operations_research::sat::ProtoTrail::Decision ( int level ) const

inline

Returns the decision assigned at level.

Definition at line 125 of file work_assignment.h.

Implications()

absl::Span< const ProtoLiteral > operations_research::sat::ProtoTrail::Implications

(

int

level

)

const

Returns literals which may be propagated at level, this does not include the decision.

Definition at line 211 of file work_assignment.cc.

Literals()

absl::Span< const ProtoLiteral > operations_research::sat::ProtoTrail::Literals ( ) const

inline

Definition at line 149 of file work_assignment.h.

MaxLevel()

int operations_research::sat::ProtoTrail::MaxLevel ( ) const

inline

Returns the maximum decision level stored in the trail.

Definition at line 122 of file work_assignment.h.

NodeIds()

absl::Span< const int > operations_research::sat::ProtoTrail::NodeIds

(

int

level

)

const

Returns the node ids for decisions and implications at level.

Definition at line 203 of file work_assignment.cc.

ObjectiveLb()

IntegerValue operations_research::sat::ProtoTrail::ObjectiveLb ( int level ) const

inline

Definition at line 144 of file work_assignment.h.

PushLevel()

void operations_research::sat::ProtoTrail::PushLevel	(	const ProtoLiteral &	decision,
		IntegerValue	objective_lb,
		int	node_id )

Adds a new assigned level to the trail.

Definition at line 149 of file work_assignment.cc.

SetLevelImplied()

void operations_research::sat::ProtoTrail::SetLevelImplied

(

int

level

)

Asserts that the decision at level is implied by earlier decisions.

We don't store implications for level 0, so only move implications up to the parent if we are removing level 2 or greater.

implications_[level-1] stores the implications for level, which are now stored in the parent's implications, so we can delete them.

Definition at line 162 of file work_assignment.cc.

SetObjectiveLb()

void operations_research::sat::ProtoTrail::SetObjectiveLb	(	int	level,
		IntegerValue	objective_lb )

Set a lower bound on the objective at level.

Definition at line 197 of file work_assignment.cc.

SetTargetPhase()

void operations_research::sat::ProtoTrail::SetTargetPhase ( absl::Span< const ProtoLiteral > phase )

inline

Definition at line 161 of file work_assignment.h.

TargetPhase()

const std::vector< ProtoLiteral > & operations_research::sat::ProtoTrail::TargetPhase ( ) const

inline

Definition at line 151 of file work_assignment.h.

---

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

• ortools/sat/work_assignment.h
• ortools/sat/work_assignment.cc