operations_research::sat::ProtoTrail Class Reference

#include <work_assignment.h>

Public Member Functions
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	SetPhase (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 93 of file work_assignment.h.

Member Function Documentation

AddImplication()

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

inline

Definition at line 124 of file work_assignment.h.

Clear()

void operations_research::sat::ProtoTrail::Clear

(

)

Clear the trail, removing all levels.

Definition at line 179 of file work_assignment.cc.

Decision()

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

inline

Returns the decision assigned at level.

Definition at line 112 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 203 of file work_assignment.cc.

Literals()

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

inline

Definition at line 136 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 109 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 195 of file work_assignment.cc.

ObjectiveLb()

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

inline

Definition at line 131 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 141 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 154 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 189 of file work_assignment.cc.

SetPhase()

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

inline

Definition at line 139 of file work_assignment.h.

TargetPhase()

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

inline

Definition at line 138 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