#include <implied_bounds.h>

Public Member Functions
	ImpliedBounds (Model *model)

	~ImpliedBounds ()
	Just display some global statistics on destruction.

bool	Add (Literal literal, IntegerLiteral integer_literal)

void	AddLiteralImpliesVarEqValue (Literal literal, IntegerVariable var, IntegerValue value)
	Adds literal => var == value.

bool	ProcessIntegerTrail (Literal first_decision)

const std::vector< ImpliedBoundEntry > &	GetImpliedBounds (IntegerVariable var)

const std::vector< IntegerVariable > &	VariablesWithImpliedBounds () const

const absl::flat_hash_map< IntegerVariable, IntegerValue > &	GetImpliedValues (Literal literal) const
	Returns all the implied values stored for a given literal.

bool	EnqueueNewDeductions ()

Detailed Description

Maintains all the implications of the form Literal => IntegerLiteral. We collect these implication at model loading, during probing and during search.

Todo: (user): This can quickly use up too much memory. Add some limit in place. In particular, each time we have literal => integer_literal we should avoid storing the same integer_literal for all other_literal for which other_literal => literal. For this we need to interact with the BinaryImplicationGraph.

Todo: (user): This is a bit of a duplicate with the Literal <=> IntegerLiteral stored in the IntegerEncoder class. However we only need one side here.

Todo: (user): Do like in the DomainDeductions class and allow to process clauses (or store them) to perform more level zero deductions. Note that this is again a slight duplicate with what we do there (except that we work at the Domain level in that presolve class).

Todo: (user): Add an implied bound cut generator to add these simple constraints to the LP when needed.

Definition at line 89 of file implied_bounds.h.

Constructor & Destructor Documentation

◆ ImpliedBounds()

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

inlineexplicit

Definition at line 91 of file implied_bounds.h.

◆ ~ImpliedBounds()

operations_research::sat::ImpliedBounds::~ImpliedBounds ( )

Just display some global statistics on destruction.

Definition at line 52 of file implied_bounds.cc.

Member Function Documentation

◆ Add()

bool operations_research::sat::ImpliedBounds::Add	(	Literal	literal,
		IntegerLiteral	integer_literal )

Adds literal => integer_literal to the repository.

Not that it checks right aways if there is another bound on the same variable involving literal.Negated(), in which case we can improve the level zero lower bound of the variable.

Ignore any Add() with a bound worse than the level zero one.

Todo: (user): Check that this never happen? it shouldn't.

We skip any IntegerLiteral referring to a variable with only two consecutive possible values. This is because, once shifted this will already be a variable in [0, 1] so we shouldn't gain much by substituing it.

Add or update the current bound.

No new info.

Checks if the variable is now fixed.

Check if we have any deduction. Since at least one of (literal, literal.Negated()) must be true, we can take the min bound as valid at level zero.

Todo: (user): Like in probing, we can also create hole in the domain if there is some implied bounds for (literal.NegatedIndex, NegagtionOf(var)) that crosses integer_literal.bound.

The other bounds is worse than the new level-zero bound which can happen because of lazy update, so here we just remove it.

The entries that are equal to the min no longer need to be stored once the level zero bound is enqueued.

No need to update var_to_bounds_ in this case.

The information below is currently only used for cuts. So no need to store it if we aren't going to use it.

If we have a new implied bound and the literal has a view, add it to var_to_bounds_. Note that we might add more than one entry with the same literal_view, and we will later need to lazily clean the vector up.

Definition at line 63 of file implied_bounds.cc.

◆ AddLiteralImpliesVarEqValue()

void operations_research::sat::ImpliedBounds::AddLiteralImpliesVarEqValue	(	Literal	literal,
		IntegerVariable	var,
		IntegerValue	value )

Adds literal => var == value.

Definition at line 196 of file implied_bounds.cc.

◆ EnqueueNewDeductions()

bool operations_research::sat::ImpliedBounds::EnqueueNewDeductions ( )

Adds to the integer trail all the new level-zero deduction made here. This can only be called at decision level zero. Returns false iff the model is infeasible.

◆ GetImpliedBounds()

const std::vector< ImpliedBoundEntry > & operations_research::sat::ImpliedBounds::GetImpliedBounds ( IntegerVariable var )

Returns all the implied bounds stored for the given variable.

Note: only literal with an IntegerView are considered here.

Lazily remove obsolete entries from the vector.

Todo: (user): Check no duplicate and remove old entry if the enforcement is tighter.

Definition at line 176 of file implied_bounds.cc.

◆ GetImpliedValues()

const absl::flat_hash_map< IntegerVariable, IntegerValue > & operations_research::sat::ImpliedBounds::GetImpliedValues ( Literal literal ) const

inline

Returns all the implied values stored for a given literal.

Definition at line 129 of file implied_bounds.h.

◆ ProcessIntegerTrail()

bool operations_research::sat::ImpliedBounds::ProcessIntegerTrail ( Literal first_decision )

This must be called after first_decision has been enqueued and propagated. It will inspect the trail and add all new implied bounds.

Preconditions: The decision level must be one (CHECKed). And the decision must be equal to first decision (we currently do not CHECK that).

Definition at line 206 of file implied_bounds.cc.

◆ VariablesWithImpliedBounds()

const std::vector< IntegerVariable > & operations_research::sat::ImpliedBounds::VariablesWithImpliedBounds ( ) const