operations_research::sat::GreaterThanAtLeastOneOfPropagator Class Reference

#include <cp_constraints.h>

Inheritance diagram for operations_research::sat::GreaterThanAtLeastOneOfPropagator:

Public Member Functions
	GreaterThanAtLeastOneOfPropagator (IntegerVariable target_var, absl::Span< const AffineExpression > exprs, absl::Span< const Literal > selectors, absl::Span< const Literal > enforcements, Model *model)
	GreaterThanAtLeastOneOfPropagator (const GreaterThanAtLeastOneOfPropagator &)=delete
	This type is neither copyable nor movable.
GreaterThanAtLeastOneOfPropagator &	operator= (const GreaterThanAtLeastOneOfPropagator &)=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 > &)
Public Member Functions inherited from operations_research::sat::LazyReasonInterface
	LazyReasonInterface ()=default
virtual	~LazyReasonInterface ()=default

Detailed Description

If we have:

• selectors[i] => (target_var >= vars[i] + offset[i])
• and we known that at least one selectors[i] must be true then we can propagate the fact that if no selectors is chosen yet, the lower bound of target_var is greater than the min of the still possible alternatives.

This constraint take care of this case when no selectors[i] is chosen yet.

This constraint support duplicate selectors.

Definition at line 71 of file cp_constraints.h.

Constructor & Destructor Documentation

GreaterThanAtLeastOneOfPropagator() [1/2]

operations_research::sat::GreaterThanAtLeastOneOfPropagator::GreaterThanAtLeastOneOfPropagator	(	IntegerVariable	target_var,
		absl::Span< const AffineExpression >	exprs,
		absl::Span< const Literal >	selectors,
		absl::Span< const Literal >	enforcements,
		Model *	model )

Definition at line 82 of file cp_constraints.cc.

GreaterThanAtLeastOneOfPropagator() [2/2]

operations_research::sat::GreaterThanAtLeastOneOfPropagator::GreaterThanAtLeastOneOfPropagator ( const GreaterThanAtLeastOneOfPropagator & )

delete

This type is neither copyable nor movable.

Member Function Documentation

Explain()

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

If the level zero bounds is good enough, no reason needed.

Todo

(user): We could also skip this if we already have the reason for the expression being high enough in the current conflict.

Implements operations_research::sat::LazyReasonInterface.

Definition at line 93 of file cp_constraints.cc.

operator=()

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

delete

Propagate()

bool operations_research::sat::GreaterThanAtLeastOneOfPropagator::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.

Todo

(user): In case of a conflict, we could push one of them to false if it is the only one.

Compute the min of the lower-bound for the still possible variables.

Todo

(user): This could be optimized by keeping more info from the last Propagate() calls.

The permutation is needed to have proper lazy reason.

Abort if we can't get a better bound.

All false, conflit.

Note

we use id/propagation_slack for other purpose.

Implements operations_research::sat::PropagatorInterface.

Definition at line 122 of file cp_constraints.cc.

RegisterWith()

void operations_research::sat::GreaterThanAtLeastOneOfPropagator::RegisterWith

(

GenericLiteralWatcher *

watcher

)

Definition at line 174 of file cp_constraints.cc.

---

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

• ortools/sat/cp_constraints.h
• ortools/sat/cp_constraints.cc