Detailed Description

Stores all the precedences relation of the form "a*x + b*y <= ub" that we could extract from the linear constraint of the model. These are stored in a directed graph.

Todo

(user): Support conditional relation.

(user): Support non-DAG like graph.

(user): Support variable offset that can be updated as search progress.

Definition at line 57 of file precedences.h.

#include <precedences.h>

Inheritance diagram for operations_research::sat::PrecedenceRelations:

Classes
struct	PrecedenceData

Public Member Functions
	PrecedenceRelations (Model *model)
void	Resize (int num_variables)
bool	AddBounds (LinearExpression2 expr, IntegerValue lb, IntegerValue ub)
bool	AddUpperBound (LinearExpression2 expr, IntegerValue ub)
	Same as above, but only for the upper bound.
void	PushConditionalRelation (absl::Span< const Literal > enforcements, LinearExpression2 expr, IntegerValue rhs)
void	SetLevel (int level) final
	Called each time we change decision level.
void	ComputeFullPrecedences (absl::Span< const IntegerVariable > vars, std::vector< FullIntegerPrecedence > *output)
void	CollectPrecedences (absl::Span< const IntegerVariable > vars, std::vector< PrecedenceData > *output)
IntegerValue	LevelZeroUpperBound (LinearExpression2 expr) const
IntegerValue	UpperBound (LinearExpression2 expr) const
void	AddReasonForUpperBoundLowerThan (LinearExpression2 expr, IntegerValue ub, std::vector< Literal > literal_reason, std::vector< IntegerLiteral > integer_reason) const
void	Build ()
Public Member Functions inherited from operations_research::ReversibleInterface
	ReversibleInterface ()
virtual	~ReversibleInterface ()

Constructor & Destructor Documentation

◆ PrecedenceRelations()

operations_research::sat::PrecedenceRelations::PrecedenceRelations ( Model * model )

inlineexplicit

Definition at line 59 of file precedences.h.

Member Function Documentation

◆ AddBounds()

bool operations_research::sat::PrecedenceRelations::AddBounds	(	LinearExpression2	expr,
		IntegerValue	lb,
		IntegerValue	ub )

Add a relation lb <= expr <= ub. If expr is not a proper linear2 expression (e.g. 0*x + y, y + y, y - y) it will be ignored. Returns true if it was added and is considered "new".

This class handles only binary relationships, let something else handle the case where there is actually a single variable.

Add to root_relations_.

Todo: (user): AddInternal() only returns true if this is the first relation between head and tail. But we can still avoid an extra lookup.

If we are not built, make sure there is enough room in the graph.

Todo: (user): Alternatively, force caller to do a Resize().

Definition at line 56 of file precedences.cc.

◆ AddReasonForUpperBoundLowerThan()

void operations_research::sat::PrecedenceRelations::AddReasonForUpperBoundLowerThan	(	LinearExpression2	expr,
		IntegerValue	ub,
		std::vector< Literal > *	literal_reason,
		std::vector< IntegerLiteral > *	integer_reason ) const

Definition at line 211 of file precedences.cc.

◆ AddUpperBound()

bool operations_research::sat::PrecedenceRelations::AddUpperBound	(	LinearExpression2	expr,
		IntegerValue	ub )

Same as above, but only for the upper bound.

Definition at line 97 of file precedences.cc.

◆ Build()

void operations_research::sat::PrecedenceRelations::Build ( )

The current code requires the internal data to be processed once all relations are loaded.

Todo: (user): Be more dynamic as we start to add relations during search.

We will construct a graph with the current relation from all_relations_. And use this to compute the "closure".

Todo: (user): Support negative offset?

Note: if we only have >= 0 ones, if we do have a cycle, we could make sure all variales are the same, and otherwise, we have a DAG or a conflict.

Todo: (user): Support non-1 coefficients.

We have two arcs.

Is it a DAG? Get a topological order of the DAG formed by all the arcs that are present.

Todo: (user): This can fail if we don't have a DAG. We could just skip Bad edges instead, and have a sub-DAG as an heuristic. Or analyze the arc weight and make sure cycle are not an issue. We can also start with arcs with strictly positive weight.

Todo: (user): Only explore the sub-graph reachable from "vars".

Lets build full precedences if we don't have too many of them.

Todo: (user): Also do that if we don't have a DAG?

Definition at line 246 of file precedences.cc.

◆ CollectPrecedences()

void operations_research::sat::PrecedenceRelations::CollectPrecedences	(	absl::Span< const IntegerVariable >	vars,
		std::vector< PrecedenceData > *	output )

+1 for the negation.

We first compute the degree/size in order to perform the transposition.

Note: we also remove duplicates.

We do not want duplicates.

Permute tmp_precedences_ into the output to put it in the correct order. For that we transform var_to_degree to point to the first position of each lbvar in the output vector.

Optimization: we remove degree one relations.

Note: it is okay to increase the -1 pos since they appear only once.

Cleanup var_to_degree, note that we don't need to clean var_to_last_index_.

Definition at line 454 of file precedences.cc.

◆ ComputeFullPrecedences()

void operations_research::sat::PrecedenceRelations::ComputeFullPrecedences	(	absl::Span< const IntegerVariable >	vars,
		std::vector< FullIntegerPrecedence > *	output )

Returns a set of relations var >= max_i(vars[index[i]] + offsets[i]).

This currently only works if the precedence relation form a DAG. If not we will just abort.

Todo: (user): generalize.

For more efficiency, this method ignores all linear2 expressions with any coefficient different from 1.

Todo: (user): Put some work limit in place, as this can be slow. Complexity is in O(vars.size()) * num_arcs.

Todo: (user): Since we don't need ALL precedences, we could just work on a sub-DAG of the full precedence graph instead of aborting. Or we can just support the general non-DAG cases.

Todo: (user): Many relations can be redundant. Filter them.

Compute all precedences. We loop over the node in topological order, and we maintain for all variable we encounter, the list of "to_consider" variables that are before.

Todo: (user): use vector of fixed size.

We copy the data for tail_var here, because the pointer is not stable.

Todo: (user): optimize when needed.

No need to create an empty entry in this case.

Small filtering heuristic: if we have (before) < tail, and tail < head, we really do not need to list (before, tail) < head. We only need that if the list of variable before head contains some variable that are not already before tail.

Extract the output for tail_var. Because of the topological ordering, the data for tail_var is already final now.

Todo: (user): Release the memory right away.

Definition at line 360 of file precedences.cc.

◆ LevelZeroUpperBound()

IntegerValue operations_research::sat::PrecedenceRelations::LevelZeroUpperBound ( LinearExpression2 expr ) const

If we don't have too many variable, we compute the full transitive closure and can query in O(1) if there is a relation between two variables. This can be used to optimize some scheduling propagation and reasons.

Warning: If there are too many, this will NOT contain all relations.

Returns kMaxIntegerValue if there are none, otherwise return an upper bound such that expr <= ub.

Definition at line 200 of file precedences.cc.

◆ PushConditionalRelation()

void operations_research::sat::PrecedenceRelations::PushConditionalRelation	(	absl::Span< const Literal >	enforcements,
		LinearExpression2	expr,
		IntegerValue	rhs )

Adds add relation (enf => expr <= rhs) that is assumed to be true at the current level.

It will be automatically reverted via the SetLevel() functions that is called before any integer propagations trigger.

This is assumed to be called when a relation becomes true (enforcement are assigned) and when it becomes false in reverse order (CHECKed).

If expr is not a proper linear2 expression (e.g. 0*x + y, y + y, y - y) it will be ignored.

This must be currently true.

Ignore if no better than best_relations, otherwise increase it.

We should only decrease because we ignored entry worse than the one in best_relations_.

Update.

Definition at line 102 of file precedences.cc.

◆ Resize()

void operations_research::sat::PrecedenceRelations::Resize ( int num_variables )

inline

Definition at line 66 of file precedences.h.

◆ SetLevel()

void operations_research::sat::PrecedenceRelations::SetLevel ( int level )

finalvirtual

Called each time we change decision level.

We only pop what is needed.

Implements operations_research::ReversibleInterface.

Definition at line 171 of file precedences.cc.

◆ UpperBound()

IntegerValue operations_research::sat::PrecedenceRelations::UpperBound ( LinearExpression2 expr ) const

Returns the maximum value for expr, and the reason for it (all true). Note that we always check LevelZeroUpperBound() so if it is better, the returned literal reason will be empty.

We separate the two because usually the reason is only needed when we push, which happen less often, so we don't mind doing two hash lookups, and we really want to optimize the UpperBound() instead.

Important: This doesn't contains the transitive closure. Important: The span is only valid in a narrow scope.

Definition at line 234 of file precedences.cc.

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

ortools/sat/precedences.h
ortools/sat/precedences.cc