operations_research::sat::LinMinPropagator Class Reference

#include <integer_expr.h>

Inheritance diagram for operations_research::sat::LinMinPropagator:

Public Member Functions
	LinMinPropagator (std::vector< LinearExpression > exprs, IntegerVariable min_var, Model *model)
	LinMinPropagator (const LinMinPropagator &)=delete
LinMinPropagator &	operator= (const LinMinPropagator &)=delete
bool	Propagate () final
void	RegisterWith (GenericLiteralWatcher *watcher)
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

Same as MinPropagator except this works on min = MIN(exprs) where exprs are linear expressions. It uses IntegerSumLE to propagate bounds on the exprs. Assumes Canonical expressions (all positive coefficients).

Definition at line 244 of file integer_expr.h.

Constructor & Destructor Documentation

LinMinPropagator() [1/2]

operations_research::sat::LinMinPropagator::LinMinPropagator	(	std::vector< LinearExpression >	exprs,
		IntegerVariable	min_var,
		Model *	model )

Definition at line 646 of file integer_expr.cc.

LinMinPropagator() [2/2]

operations_research::sat::LinMinPropagator::LinMinPropagator ( const LinMinPropagator & )

delete

Member Function Documentation

Explain()

void operations_research::sat::LinMinPropagator::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.

Now add the old integer_reason that triggered this propagation.

Implements operations_research::sat::LazyReasonInterface.

Definition at line 653 of file integer_expr.cc.

operator=()

LinMinPropagator & operations_research::sat::LinMinPropagator::operator= ( const LinMinPropagator & )

delete

Propagate()

bool operations_research::sat::LinMinPropagator::Propagate ( )

finalvirtual

This will be called after one or more literals that are watched by this propagator changed. It will also always be called on the first propagation cycle after registration.

Count the number of interval that are possible candidate for the min. Only the intervals for which lb > current_min_ub cannot.

Propagation a) lb(min) >= lb(MIN(exprs)) = MIN(lb(exprs));

Conflict will be detected by the fact that the [lb, ub] of the min is empty. In case of conflict, we just need the reason for pushing UB + 1.

Propagation b) ub(min) >= ub(MIN(exprs)) and we can't propagate anything here unless there is just one possible expression 'e' that can be the min: for all u != e, lb(u) > ub(min); In this case, ub(min) >= ub(e).

For this propagation, we only need to fill the integer reason once at the lowest level. At higher levels this reason still remains valid.

The reason is that all the other interval start after current_min_ub. And that min_ub has its current value.

Implements operations_research::sat::PropagatorInterface.

Definition at line 750 of file integer_expr.cc.

RegisterWith()

void operations_research::sat::LinMinPropagator::RegisterWith

(

GenericLiteralWatcher *

watcher

)

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