operations_research::sat::LinearConstraintPropagator< use_int128 > Class Template Reference

#include <integer_expr.h>

Inheritance diagram for operations_research::sat::LinearConstraintPropagator< use_int128 >:

Public Member Functions
	LinearConstraintPropagator (absl::Span< const Literal > enforcement_literals, absl::Span< const IntegerVariable > vars, absl::Span< const IntegerValue > coeffs, IntegerValue upper_bound, Model *model)
	LinearConstraintPropagator (LinearConstraint ct, Model *model)
bool	Propagate () final
void	RegisterWith (GenericLiteralWatcher *watcher)
bool	PropagateAtLevelZero ()
std::pair< IntegerValue, IntegerValue >	ConditionalLb (IntegerLiteral integer_literal, IntegerVariable target_var) const
	NOTE(user): This is only used with int128, so we code only a single version.
void	Explain (int id, IntegerValue propagation_slack, IntegerVariable var_to_explain, int trail_index, std::vector< Literal > *literals_reason, std::vector< int > *trail_indices_reason) final
	For LazyReasonInterface.
Public Member Functions inherited from operations_research::sat::PropagatorInterface
	PropagatorInterface ()=default
virtual	~PropagatorInterface ()=default
virtual bool	IncrementalPropagate (const std::vector< int > &)

Detailed Description

template<bool use_int128 = false>
class operations_research::sat::LinearConstraintPropagator< use_int128 >

A really basic implementation of an upper-bounded sum of integer variables. The complexity is in O(num_variables) at each propagation.

Note

we assume that there can be NO integer overflow. This must be checked at model validation time before this is even created. If use_int128 is true, then we actually do the computations that could overflow in 128 bits, so that we can deal with constraints that might overflow (like the one scaled from the LP relaxation). Note that we still use some preconditions, such that for each variable the difference between their bounds fit on an int64_t.

Todo

(user): Technically we could still have an int128 overflow since we sum n terms that cannot overflow but can still be pretty close to the limit. Make sure this never happens! For most problem though, because the variable bounds will be smaller than 10^9, we are pretty safe.

Todo

(user): If one has many such constraint, it will be more efficient to propagate all of them at once rather than doing it one at the time.

Todo

(user): Explore tree structure to get a log(n) complexity.

Todo

(user): When the variables are Boolean, use directly the pseudo-Boolean constraint implementation. But we do need support for enforcement literals there.

Definition at line 67 of file integer_expr.h.

Constructor & Destructor Documentation

LinearConstraintPropagator() [1/2]

template<bool use_int128>

operations_research::sat::LinearConstraintPropagator< use_int128 >::LinearConstraintPropagator	(	absl::Span< const Literal >	enforcement_literals,
		absl::Span< const IntegerVariable >	vars,
		absl::Span< const IntegerValue >	coeffs,
		IntegerValue	upper_bound,
		Model *	model )

If refied_literal is kNoLiteralIndex then this is a normal constraint, otherwise we enforce the implication refied_literal => constraint is true.

Note

we don't do the reverse implication here, it is usually done by another LinearConstraintPropagator constraint on the negated variables.

Todo

(user): deal with this corner case.

Copy data.

Handle negative coefficients.

Literal reason will only be used with the negation of enforcement_literals. It will stay constant. We also do not store enforcement_literals, but retrieve them from there.

Initialize the reversible numbers.

Definition at line 46 of file integer_expr.cc.

LinearConstraintPropagator() [2/2]

template<bool use_int128>

operations_research::sat::LinearConstraintPropagator< use_int128 >::LinearConstraintPropagator	(	LinearConstraint	ct,
		Model *	model )

This version allow to std::move the memory from the LinearConstraint directly. It Only uses the upper bound. Id does not support enforcement_literals.

Todo

(user): Avoid duplication with other constructor.

Todo

(user): deal with this corner case.

Handle negative coefficients.

Initialize the reversible numbers.

Definition at line 87 of file integer_expr.cc.

Member Function Documentation

ConditionalLb()

template<bool use_int128>

std::pair< IntegerValue, IntegerValue > operations_research::sat::LinearConstraintPropagator< use_int128 >::ConditionalLb	(	IntegerLiteral	integer_literal,
		IntegerVariable	target_var ) const

NOTE(user): This is only used with int128, so we code only a single version.

This is a pretty usage specific function. Returns the implied lower bound on target_var if the given integer literal is false (resp. true). If the variables do not appear both in the linear inequality, this returns two kMinIntegerValue.

The code below is wrong if integer_literal and target_var are the same. In this case we return the trivial bounds.

Recall that all our coefficient are positive.

Warning

It is important to do the computation like the propagation is doing it to be sure we don't have overflow, since this is what we check when creating constraints.

The upper bound on NegationOf(target_var) are lb(-target) + slack / coeff. So the lower bound on target_var is ub - slack / coeff.

Todo

(user): If there is a conflict (negative slack) we can be more precise.

A literal means var >= bound.

We have var_coeff * var in the expression, the literal is var >= bound. When it is false, it is not relevant as implied_lb used var >= lb. When it is true, the diff is bound - lb.

We have var_coeff * -var in the expression, the literal is var >= bound. When it is true, it is not relevant as implied_lb used -var >= -ub. And when it is false it means var < bound, so -var >= -bound + 1

Definition at line 139 of file integer_expr.cc.

Explain()

template<bool use_int128>

void operations_research::sat::LinearConstraintPropagator< use_int128 >::Explain ( int id, IntegerValue propagation_slack, IntegerVariable var_to_explain, int trail_index, std::vector< Literal > * literals_reason, std::vector< int > * trail_indices_reason )

finalvirtual

For LazyReasonInterface.

Implements operations_research::sat::LazyReasonInterface.

Definition at line 231 of file integer_expr.cc.

Propagate()

template<bool use_int128>

bool operations_research::sat::LinearConstraintPropagator< use_int128 >::Propagate ( )

finalvirtual

We propagate:

• If the sum of the individual lower-bound is > upper_bound, we fail.
• For all i, upper-bound of i <= upper_bound - Sum {individual lower-bound excluding i).

Reified case: If any of the enforcement_literals are false, we ignore the constraint.

Unfortunately, we can't propagate anything if we have more than one unassigned enforcement literal.

Compute the new lower bound and update the reversible structures.

Update the set of fixed variables.

Save the current sum of fixed variables.

If use_int128 is true, the slack or propagation slack can be larger than this. To detect overflow with capped arithmetic, it is important the slack used in our algo never exceed this value.

Conflict?

It is fine if we don't relax as much as possible.

Note

RelaxLinearReason() is overflow safe.

Propagate the only non-true literal to false.

We can only propagate more if all the enforcement literals are true.

The lower bound of all the variables except one can be used to update the upper bound of the last one.

Todo

(user): If the new ub fall into an hole of the variable, we can actually relax the reason more by computing a better slack.

Todo

(user): this is never supposed to happen since if we didn't have a conflict above, we should be able to reduce the upper bound. It might indicate an issue with our Boolean <-> integer encoding.

Implements operations_research::sat::PropagatorInterface.

Definition at line 259 of file integer_expr.cc.

PropagateAtLevelZero()

template<bool use_int128>

bool operations_research::sat::LinearConstraintPropagator< use_int128 >::PropagateAtLevelZero

(

)

Same as Propagate() but only consider current root level bounds. This is mainly useful for the LP propagator since it can find relevant optimal really late in the search tree.

Todo

(user): Deal with enforcements. It is just a bit of code to read the value of the literals at level zero.

Compute the new lower bound and update the reversible structures.

Conflict?

The lower bound of all the variables except one can be used to update the upper bound of the last one.

Definition at line 398 of file integer_expr.cc.

RegisterWith()

template<bool use_int128>

void operations_research::sat::LinearConstraintPropagator< use_int128 >::RegisterWith

(

GenericLiteralWatcher *

watcher

)

We only watch the true direction.

Todo

(user): if there is more than one, maybe we should watch more to propagate a "conflict" as soon as only one is unassigned?

Definition at line 467 of file integer_expr.cc.

---

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

• ortools/sat/integer_expr.h
• ortools/sat/integer_expr.cc