#include <integer.h>

Inheritance diagram for operations_research::sat::IntegerTrail:

Public Member Functions
	IntegerTrail (Model *model)

	IntegerTrail (const IntegerTrail &)=delete
	This type is neither copyable nor movable.

IntegerTrail &	operator= (const IntegerTrail &)=delete

	~IntegerTrail () final

bool	Propagate (Trail *trail) final

void	Untrail (const Trail &trail, int literal_trail_index) final

absl::Span< const Literal >	Reason (const Trail &trail, int trail_index, int64_t conflict_id) const final

IntegerVariable	NumIntegerVariables () const

void	ReserveSpaceForNumVariables (int num_vars)

IntegerVariable	AddIntegerVariable (IntegerValue lower_bound, IntegerValue upper_bound)

IntegerVariable	AddIntegerVariable (const Domain &domain)

const Domain &	InitialVariableDomain (IntegerVariable var) const

bool	UpdateInitialDomain (IntegerVariable var, Domain domain)

IntegerVariable	GetOrCreateConstantIntegerVariable (IntegerValue value)

int	NumConstantVariables () const

IntegerVariable	AddIntegerVariable ()

IntegerValue	LowerBound (IntegerVariable i) const
	Returns the current lower/upper bound of the given integer variable.

IntegerValue	UpperBound (IntegerVariable i) const

const IntegerValue *	LowerBoundsData () const

bool	IsFixed (IntegerVariable i) const
	Checks if the variable is fixed.

IntegerValue	FixedValue (IntegerVariable i) const
	Checks that the variable is fixed and returns its value.

IntegerValue	LowerBound (AffineExpression expr) const
	Same as above for an affine expression.

IntegerValue	UpperBound (AffineExpression expr) const

bool	IsFixed (AffineExpression expr) const

IntegerValue	FixedValue (AffineExpression expr) const

IntegerLiteral	LowerBoundAsLiteral (IntegerVariable i) const

IntegerLiteral	UpperBoundAsLiteral (IntegerVariable i) const

IntegerLiteral	LowerBoundAsLiteral (AffineExpression expr) const

IntegerLiteral	UpperBoundAsLiteral (AffineExpression expr) const

bool	IntegerLiteralIsTrue (IntegerLiteral l) const
	Returns the current value (if known) of an IntegerLiteral.

bool	IntegerLiteralIsFalse (IntegerLiteral l) const

IntegerValue	LevelZeroLowerBound (IntegerVariable var) const
	Returns globally valid lower/upper bound on the given integer variable.

IntegerValue	LevelZeroUpperBound (IntegerVariable var) const

IntegerValue	LevelZeroLowerBound (AffineExpression exp) const
	Returns globally valid lower/upper bound on the given affine expression.

IntegerValue	LevelZeroUpperBound (AffineExpression exp) const

bool	IsFixedAtLevelZero (IntegerVariable var) const
	Returns true if the variable is fixed at level 0.

bool	IsFixedAtLevelZero (AffineExpression expr) const
	Returns true if the affine expression is fixed at level 0.

IntegerValue	ConditionalLowerBound (Literal l, IntegerVariable i) const

IntegerValue	ConditionalLowerBound (Literal l, AffineExpression expr) const

IntegerValue	ConditionalUpperBound (Literal l, IntegerVariable i) const
	Returns the current upper bound assuming the literal is true.

IntegerValue	ConditionalUpperBound (Literal l, AffineExpression expr) const

void	RelaxLinearReason (IntegerValue slack, absl::Span< const IntegerValue > coeffs, std::vector< IntegerLiteral > *reason) const

void	AppendRelaxedLinearReason (IntegerValue slack, absl::Span< const IntegerValue > coeffs, absl::Span< const IntegerVariable > vars, std::vector< IntegerLiteral > *reason) const
	Same as above but take in IntegerVariables instead of IntegerLiterals.

void	RelaxLinearReason (IntegerValue slack, absl::Span< const IntegerValue > coeffs, std::vector< int > *trail_indices) const
	Same as above but relax the given trail indices.

void	RemoveLevelZeroBounds (std::vector< IntegerLiteral > *reason) const

ABSL_MUST_USE_RESULT bool	Enqueue (IntegerLiteral i_lit)

ABSL_MUST_USE_RESULT bool	Enqueue (IntegerLiteral i_lit, absl::Span< const Literal > literal_reason, absl::Span< const IntegerLiteral > integer_reason)

ABSL_MUST_USE_RESULT bool	SafeEnqueue (IntegerLiteral i_lit, absl::Span< const IntegerLiteral > integer_reason)

ABSL_MUST_USE_RESULT bool	ConditionalEnqueue (Literal lit, IntegerLiteral i_lit, std::vector< Literal > literal_reason, std::vector< IntegerLiteral > integer_reason)

ABSL_MUST_USE_RESULT bool	Enqueue (IntegerLiteral i_lit, absl::Span< const Literal > literal_reason, absl::Span< const IntegerLiteral > integer_reason, int trail_index_with_same_reason)

ABSL_MUST_USE_RESULT bool	EnqueueWithLazyReason (IntegerLiteral i_lit, int id, IntegerValue propagation_slack, LazyReasonInterface *explainer)
	Lazy reason API.

ABSL_MUST_USE_RESULT bool	RootLevelEnqueue (IntegerLiteral i_lit)

void	EnqueueLiteral (Literal literal, absl::Span< const Literal > literal_reason, absl::Span< const IntegerLiteral > integer_reason)

std::vector< Literal >	ReasonFor (IntegerLiteral literal) const

void	MergeReasonInto (absl::Span< const IntegerLiteral > literals, std::vector< Literal > *output) const

int64_t	num_enqueues () const

int64_t	timestamp () const

int64_t	num_level_zero_enqueues () const
	Same as num_enqueues but only count the level zero changes.

void	RegisterWatcher (SparseBitset< IntegerVariable > *p)

bool	ReportConflict (absl::Span< const Literal > literal_reason, absl::Span< const IntegerLiteral > integer_reason)

bool	ReportConflict (absl::Span< const IntegerLiteral > integer_reason)

bool	VariableLowerBoundIsFromLevelZero (IntegerVariable var) const
	Returns true if the variable lower bound is still the one from level zero.

void	RegisterReversibleClass (ReversibleInterface *rev)

int	Index () const

void	AppendNewBounds (std::vector< IntegerLiteral > *output) const

void	AppendNewBoundsFrom (int base_index, std::vector< IntegerLiteral > *output) const

int	FindTrailIndexOfVarBefore (IntegerVariable var, int threshold) const

bool	InPropagationLoop () const

void	NotifyThatPropagationWasAborted ()

IntegerVariable	NextVariableToBranchOnInPropagationLoop () const

bool	CurrentBranchHadAnIncompletePropagation ()

IntegerVariable	FirstUnassignedVariable () const

bool	HasPendingRootLevelDeduction () const
	Return true if we can fix new fact at level zero.

void	RegisterDebugChecker (std::function< bool(absl::Span< const Literal > clause, absl::Span< const IntegerLiteral > integers)> checker)

void	AddAllGreaterThanConstantReason (absl::Span< AffineExpression > exprs, IntegerValue target_min, std::vector< int > *indices) const

Public Member Functions inherited from operations_research::sat::SatPropagator
	SatPropagator (const std::string &name)

	SatPropagator (const SatPropagator &)=delete
	This type is neither copyable nor movable.

SatPropagator &	operator= (const SatPropagator &)=delete

virtual	~SatPropagator ()=default

void	SetPropagatorId (int id)
	Sets/Gets this propagator unique id.

int	PropagatorId () const

bool	PropagatePreconditionsAreSatisfied (const Trail &trail) const
	######################## Implementations below ########################

bool	PropagationIsDone (const Trail &trail) const
	Returns true iff all the trail was inspected by this propagator.

virtual bool	IsEmpty () const

Additional Inherited Members
Protected Attributes inherited from operations_research::sat::SatPropagator
const std::string	name_

int	propagator_id_

int	propagation_trail_index_

Detailed Description

This class maintains a set of integer variables with their current bounds. Bounds can be propagated from an external "source" and this class helps to maintain the reason for each propagation.

Definition at line 774 of file integer.h.

Constructor & Destructor Documentation

◆ IntegerTrail() [1/2]

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

inlineexplicit

Definition at line 776 of file integer.h.

◆ IntegerTrail() [2/2]

operations_research::sat::IntegerTrail::IntegerTrail ( const IntegerTrail & )

delete

This type is neither copyable nor movable.

◆ ~IntegerTrail()

operations_research::sat::IntegerTrail::~IntegerTrail ( )

final

Definition at line 698 of file integer.cc.

Member Function Documentation

◆ AddAllGreaterThanConstantReason()

void operations_research::sat::IntegerTrail::AddAllGreaterThanConstantReason	(	absl::Span< AffineExpression >	exprs,
		IntegerValue	target_min,
		std::vector< int > *	indices ) const

inline

This is used by the GreaterThanAtLeastOneOf() lazy reason.

Todo: (user): This might better lives together with the propagation code, but it does need access to data about the reason/conflict being currently computed. Also for speed we do need all the code here in on block. Given than we have just a few "lazy integer reason", we might not really want a generic code in any case.

Skip if we already have an explanation for expr >= target_min. Note that we already do that while processing the returned indices, so this mainly save a FindLowestTrailIndexThatExplainBound() call per skipped indices, which can still be costly.

We need to find the index that explain the bound.

Note: this will skip if the condition is true at level zero.

Definition at line 1158 of file integer.h.

◆ AddIntegerVariable() [1/3]

IntegerVariable operations_research::sat::IntegerTrail::AddIntegerVariable ( )

inline

Same as AddIntegerVariable() but uses the maximum possible range. Note that since we take negation of bounds in various places, we make sure that we don't have overflow when we take the negation of the lower bound or of the upper bound.

Definition at line 854 of file integer.h.

◆ AddIntegerVariable() [2/3]

IntegerVariable operations_research::sat::IntegerTrail::AddIntegerVariable ( const Domain & domain )

Same as above but for a more complex domain specified as a sorted list of disjoint intervals. See the Domain class.

Definition at line 868 of file integer.cc.

◆ AddIntegerVariable() [3/3]

IntegerVariable operations_research::sat::IntegerTrail::AddIntegerVariable	(	IntegerValue	lower_bound,
		IntegerValue	upper_bound )

Adds a new integer variable. Adding integer variable can only be done when the decision level is zero (checked). The given bounds are INCLUSIVE and must not cross.

Note on integer overflow: 'upper_bound - lower_bound' must fit on an int64_t, this is DCHECKed. More generally, depending on the constraints that are added, the bounds magnitude must be small enough to satisfy each constraint overflow precondition.

Definition at line 837 of file integer.cc.

◆ AppendNewBounds()

void operations_research::sat::IntegerTrail::AppendNewBounds ( std::vector< IntegerLiteral > * output ) const

Inspects the trail and output all the non-level zero bounds (one per variables) to the output. The algo is sparse if there is only a few propagations on the trail.

Definition at line 2065 of file integer.cc.

◆ AppendNewBoundsFrom()

void operations_research::sat::IntegerTrail::AppendNewBoundsFrom	(	int	base_index,
		std::vector< IntegerLiteral > *	output ) const

Inspects the trail and output all the non-level zero bounds from the base index (one per variables) to the output. The algo is sparse if there is only a few propagations on the trail.

Todo: (user): Implement a dense version if there is more trail entries than variables!

In order to push the best bound for each variable, we loop backward.

Definition at line 2071 of file integer.cc.

◆ AppendRelaxedLinearReason()

void operations_research::sat::IntegerTrail::AppendRelaxedLinearReason	(	IntegerValue	slack,
		absl::Span< const IntegerValue >	coeffs,
		absl::Span< const IntegerVariable >	vars,
		std::vector< IntegerLiteral > *	reason ) const

Same as above but take in IntegerVariables instead of IntegerLiterals.

Definition at line 1047 of file integer.cc.

◆ ConditionalEnqueue()

bool operations_research::sat::IntegerTrail::ConditionalEnqueue	(	Literal	lit,
		IntegerLiteral	i_lit,
		std::vector< Literal > *	literal_reason,
		std::vector< IntegerLiteral > *	integer_reason )

Pushes the given integer literal assuming that the Boolean literal is true. This can do a few things:

If lit it true, add it to the reason and push the integer bound.
If the bound is infeasible, push lit to false.
If the underlying variable is optional and also controlled by lit, push the bound even if lit is not assigned.

We can't push anything in this case.

We record it for this propagation phase (until the next untrail) as this is relatively fast and heuristics can exploit this.

Note: currently we only use ConditionalEnqueue() in scheduling propagator, and these propagator are quite slow so this is not visible.

Todo: (user): We could even keep the reason and maybe do some reasoning using at_least_one constraint on a set of the Boolean used here.

Definition at line 1269 of file integer.cc.

◆ ConditionalLowerBound() [1/2]

IntegerValue operations_research::sat::IntegerTrail::ConditionalLowerBound	(	Literal	l,
		AffineExpression	expr ) const

inline

Definition at line 1743 of file integer.h.

◆ ConditionalLowerBound() [2/2]

IntegerValue operations_research::sat::IntegerTrail::ConditionalLowerBound	(	Literal	l,
		IntegerVariable	i ) const

inline

Advanced usage. Returns the current lower bound assuming the literal is true.

Definition at line 1734 of file integer.h.

◆ ConditionalUpperBound() [1/2]

IntegerValue operations_research::sat::IntegerTrail::ConditionalUpperBound	(	Literal	l,
		AffineExpression	expr ) const

inline

Definition at line 1754 of file integer.h.

◆ ConditionalUpperBound() [2/2]

IntegerValue operations_research::sat::IntegerTrail::ConditionalUpperBound	(	Literal	l,
		IntegerVariable	i ) const

inline

Returns the current upper bound assuming the literal is true.

Definition at line 1749 of file integer.h.

◆ CurrentBranchHadAnIncompletePropagation()

bool operations_research::sat::IntegerTrail::CurrentBranchHadAnIncompletePropagation ( )

If we had an incomplete propagation, it is important to fix all the variables and not really on the propagation to do so. This is related to the InPropagationLoop() code above.

Definition at line 1481 of file integer.cc.

◆ Enqueue() [1/3]

ABSL_MUST_USE_RESULT bool operations_research::sat::IntegerTrail::Enqueue ( IntegerLiteral i_lit )

inline

Enqueue new information about a variable bound. Calling this with a less restrictive bound than the current one will have no effect.

The reason for this "assignment" must be provided as:

A set of Literal currently being all false.
A set of IntegerLiteral currently being all true.

IMPORTANT: Notice the inversed sign in the literal reason. This is a bit confusing but internally SAT use this direction for efficiency.

Note(user): Duplicates Literal/IntegerLiteral are supported because we call STLSortAndRemoveDuplicates() in MergeReasonInto(), but maybe they shouldn't for efficiency reason.

Todo: (user): If the given bound is equal to the current bound, maybe the new reason is better? how to decide and what to do in this case? to think about it. Currently we simply don't do anything.

Definition at line 972 of file integer.h.

◆ Enqueue() [2/3]

ABSL_MUST_USE_RESULT bool operations_research::sat::IntegerTrail::Enqueue	(	IntegerLiteral	i_lit,
		absl::Span< const Literal >	literal_reason,
		absl::Span< const IntegerLiteral >	integer_reason )

inline

Definition at line 975 of file integer.h.

◆ Enqueue() [3/3]

ABSL_MUST_USE_RESULT bool operations_research::sat::IntegerTrail::Enqueue	(	IntegerLiteral	i_lit,
		absl::Span< const Literal >	literal_reason,
		absl::Span< const IntegerLiteral >	integer_reason,
		int	trail_index_with_same_reason )

inline

Same as Enqueue(), but takes an extra argument which if smaller than integer_trail_.size() is interpreted as the trail index of an old Enqueue() that had the same reason as this one. Note that the given Span must still be valid as they are used in case of conflict.

Todo: (user): This currently cannot refer to a trail_index with a lazy reason. Fix or at least check that this is the case.

Definition at line 1011 of file integer.h.

◆ EnqueueLiteral()

void operations_research::sat::IntegerTrail::EnqueueLiteral	(	Literal	literal,
		absl::Span< const Literal >	literal_reason,
		absl::Span< const IntegerLiteral >	integer_reason )

Enqueues the given literal on the trail. See the comment of Enqueue() for the reason format.

Definition at line 1392 of file integer.cc.

◆ EnqueueWithLazyReason()

ABSL_MUST_USE_RESULT bool operations_research::sat::IntegerTrail::EnqueueWithLazyReason	(	IntegerLiteral	i_lit,
		int	id,
		IntegerValue	propagation_slack,
		LazyReasonInterface *	explainer )

inline

Lazy reason API.

Definition at line 1020 of file integer.h.

◆ FindTrailIndexOfVarBefore()

int operations_research::sat::IntegerTrail::FindTrailIndexOfVarBefore	(	IntegerVariable	var,
		int	threshold ) const

Returns the trail index < threshold of a TrailEntry about var. Returns -1 if there is no such entry (at a positive decision level). This is basically the trail index of the lower bound of var at the time.

Important: We do some optimization internally, so this should only be used from within a LazyReasonFunction().

Optimization. We assume this is only called when computing a reason, so we can ignore this trail_index if we already need a more restrictive reason for this var.

Hacky: We know this is only called with threshold == trail_index of the trail entry we are trying to explain. So this test can only trigger when a variable was shown to be already implied by the current conflict.

Disable the other optim if we might expand this literal during 1-UIP resolution.

Check the validity of the cached index and use it if possible.

Definition at line 946 of file integer.cc.

◆ FirstUnassignedVariable()

IntegerVariable operations_research::sat::IntegerTrail::FirstUnassignedVariable ( ) const

Definition at line 1485 of file integer.cc.

◆ FixedValue() [1/2]

IntegerValue operations_research::sat::IntegerTrail::FixedValue ( AffineExpression expr ) const

inline

Definition at line 1785 of file integer.h.

◆ FixedValue() [2/2]

IntegerValue operations_research::sat::IntegerTrail::FixedValue ( IntegerVariable i ) const

inline

Checks that the variable is fixed and returns its value.

Definition at line 1729 of file integer.h.

◆ GetOrCreateConstantIntegerVariable()

IntegerVariable operations_research::sat::IntegerTrail::GetOrCreateConstantIntegerVariable ( IntegerValue value )

Same as AddIntegerVariable(value, value), but this is a bit more efficient because it reuses another constant with the same value if its exist.

Note(user): Creating constant integer variable is a bit wasteful, but not that much, and it allows to simplify a lot of constraints that do not need to handle this case any differently than the general one. Maybe there is a better solution, but this is not really high priority as of December 2016.

Note: this might invalidate insert.first->second.

Definition at line 925 of file integer.cc.

◆ HasPendingRootLevelDeduction()

bool operations_research::sat::IntegerTrail::HasPendingRootLevelDeduction ( ) const

inline

Return true if we can fix new fact at level zero.

Definition at line 1137 of file integer.h.

◆ Index()

int operations_research::sat::IntegerTrail::Index ( ) const

inline

Definition at line 1103 of file integer.h.

◆ InitialVariableDomain()

const Domain & operations_research::sat::IntegerTrail::InitialVariableDomain ( IntegerVariable var ) const

Returns the initial domain of the given variable. Note that the min/max are updated with level zero propagation, but not holes.

Definition at line 876 of file integer.cc.

◆ InPropagationLoop()

bool operations_research::sat::IntegerTrail::InPropagationLoop ( ) const

Basic heuristic to detect when we are in a propagation loop, and suggest a good variable to branch on (taking the middle value) to get out of it.

We count the number of propagation at the current level, and returns true if it seems really large. Note that we disable this if we are in fixed search.

Definition at line 1434 of file integer.cc.

◆ IntegerLiteralIsFalse()

bool operations_research::sat::IntegerTrail::IntegerLiteralIsFalse ( IntegerLiteral l ) const

inline

Definition at line 1806 of file integer.h.

◆ IntegerLiteralIsTrue()

bool operations_research::sat::IntegerTrail::IntegerLiteralIsTrue ( IntegerLiteral l ) const

inline

Returns the current value (if known) of an IntegerLiteral.

Definition at line 1802 of file integer.h.

◆ IsFixed() [1/2]

bool operations_research::sat::IntegerTrail::IsFixed ( AffineExpression expr ) const

inline

Definition at line 1780 of file integer.h.

◆ IsFixed() [2/2]

bool operations_research::sat::IntegerTrail::IsFixed ( IntegerVariable i ) const

inline

Checks if the variable is fixed.

Definition at line 1725 of file integer.h.

◆ IsFixedAtLevelZero() [1/2]

bool operations_research::sat::IntegerTrail::IsFixedAtLevelZero ( AffineExpression expr ) const

inline

Returns true if the affine expression is fixed at level 0.

Definition at line 1839 of file integer.h.

◆ IsFixedAtLevelZero() [2/2]

bool operations_research::sat::IntegerTrail::IsFixedAtLevelZero ( IntegerVariable var ) const

inline

Returns true if the variable is fixed at level 0.

Definition at line 1822 of file integer.h.

◆ LevelZeroLowerBound() [1/2]

IntegerValue operations_research::sat::IntegerTrail::LevelZeroLowerBound ( AffineExpression exp ) const

inline

Returns globally valid lower/upper bound on the given affine expression.

Definition at line 1827 of file integer.h.

◆ LevelZeroLowerBound() [2/2]

IntegerValue operations_research::sat::IntegerTrail::LevelZeroLowerBound ( IntegerVariable var ) const

inline

Returns globally valid lower/upper bound on the given integer variable.

The level zero bounds are stored at the beginning of the trail and they also serves as sentinels. Their index match the variables index.

Definition at line 1812 of file integer.h.

◆ LevelZeroUpperBound() [1/2]

IntegerValue operations_research::sat::IntegerTrail::LevelZeroUpperBound ( AffineExpression exp ) const

inline

Definition at line 1833 of file integer.h.

◆ LevelZeroUpperBound() [2/2]

IntegerValue operations_research::sat::IntegerTrail::LevelZeroUpperBound ( IntegerVariable var ) const

inline

Definition at line 1817 of file integer.h.

◆ LowerBound() [1/2]

IntegerValue operations_research::sat::IntegerTrail::LowerBound ( AffineExpression expr ) const

inline

Same as above for an affine expression.

Definition at line 1770 of file integer.h.

◆ LowerBound() [2/2]

IntegerValue operations_research::sat::IntegerTrail::LowerBound ( IntegerVariable i ) const

inline

Returns the current lower/upper bound of the given integer variable.

Definition at line 1717 of file integer.h.

◆ LowerBoundAsLiteral() [1/2]

IntegerLiteral operations_research::sat::IntegerTrail::LowerBoundAsLiteral ( AffineExpression expr ) const

inline

Returns the integer literal that represent the current lower/upper bound of the given affine expression. In case the expression is constant, it returns IntegerLiteral::TrueLiteral().

Definition at line 1790 of file integer.h.

◆ LowerBoundAsLiteral() [2/2]

IntegerLiteral operations_research::sat::IntegerTrail::LowerBoundAsLiteral ( IntegerVariable i ) const

inline

Returns the integer literal that represent the current lower/upper bound of the given integer variable.

Definition at line 1760 of file integer.h.

◆ LowerBoundsData()

const IntegerValue * operations_research::sat::IntegerTrail::LowerBoundsData ( ) const

inline

If one needs to do a lot of LowerBound()/UpperBound() it will be faster to cache the current pointer to the underlying vector.

Definition at line 864 of file integer.h.

◆ MergeReasonInto()

void operations_research::sat::IntegerTrail::MergeReasonInto	(	absl::Span< const IntegerLiteral >	literals,
		std::vector< Literal > *	output ) const

Appends the reason for the given integer literals to the output and call STLSortAndRemoveDuplicates() on it. This function accept "constant" literal.

Any indices lower than that means that there is no reason needed.

Note: it is important for size to be signed because of -1 indices.

Definition at line 1825 of file integer.cc.

◆ NextVariableToBranchOnInPropagationLoop()

IntegerVariable operations_research::sat::IntegerTrail::NextVariableToBranchOnInPropagationLoop ( ) const

We try to select a variable with a large domain that was propagated a lot already.

Definition at line 1452 of file integer.cc.

◆ NotifyThatPropagationWasAborted()

void operations_research::sat::IntegerTrail::NotifyThatPropagationWasAborted ( )

Definition at line 1444 of file integer.cc.

◆ num_enqueues()

int64_t operations_research::sat::IntegerTrail::num_enqueues ( ) const

inline

Returns the number of enqueues that changed a variable bounds. We don't count enqueues called with a less restrictive bound than the current one.

Note(user): this can be used to see if any of the bounds changed. Just looking at the integer trail index is not enough because at level zero it doesn't change since we directly update the "fixed" bounds.

Definition at line 1060 of file integer.h.

◆ num_level_zero_enqueues()

int64_t operations_research::sat::IntegerTrail::num_level_zero_enqueues ( ) const

inline

Same as num_enqueues but only count the level zero changes.

Definition at line 1064 of file integer.h.

◆ NumConstantVariables()

int operations_research::sat::IntegerTrail::NumConstantVariables ( ) const

The +1 if for the special key zero (the only case when we have an odd number of entries).

Definition at line 940 of file integer.cc.

◆ NumIntegerVariables()

IntegerVariable operations_research::sat::IntegerTrail::NumIntegerVariables ( ) const

inline

Returns the number of created integer variables.

Note: this is twice the number of call to AddIntegerVariable() since we automatically create the NegationOf() variable too.

Definition at line 806 of file integer.h.

◆ operator=()

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

delete

◆ Propagate()

bool operations_research::sat::IntegerTrail::Propagate ( Trail * trail )

finalvirtual

SatPropagator interface. These functions make sure the current bounds information is in sync with the current solver literal trail. Any class/propagator using this class must make sure it is synced to the correct state before calling any of its functions.

Make sure that our internal "integer_search_levels_" size matches the sat decision levels. At the level zero, integer_search_levels_ should be empty.

This is required because when loading a model it is possible that we add (literal <-> integer literal) associations for literals that have already been propagated here. This often happens when the presolve is off and many variables are fixed.

Todo: (user): refactor the interaction IntegerTrail <-> IntegerEncoder so that we can just push right away such literal. Unfortunately, this is is a big chunk of work.

Note: we do not call Enqueue here but directly the update domain function so that we do not abort even if the level zero bounds were up to date.

Process all the "associated" literals and Enqueue() the corresponding bounds.

The reason is simply the associated literal.

Implements operations_research::sat::SatPropagator.

Definition at line 705 of file integer.cc.

◆ Reason()

absl::Span< const Literal > operations_research::sat::IntegerTrail::Reason	(	const Trail &	trail,
		int	trail_index,
		int64_t	conflict_id ) const

finalvirtual

Todo: (user): If this is called many time on the same variables, it could be made faster by using some caching mechanism.

Reimplemented from operations_research::sat::SatPropagator.

Definition at line 2047 of file integer.cc.

◆ ReasonFor()

std::vector< Literal > operations_research::sat::IntegerTrail::ReasonFor ( IntegerLiteral literal ) const

Returns the reason (as set of Literal currently false) for a given integer literal. Note that the bound must be less restrictive than the current bound (checked).

Definition at line 1819 of file integer.cc.

◆ RegisterDebugChecker()

void operations_research::sat::IntegerTrail::RegisterDebugChecker ( std::function< bool(absl::Span< const Literal > clause, absl::Span< const IntegerLiteral > integers)> checker )

inline

If this is set, and in debug mode, we will call this on all conflict to be checked for potential issue. Usually against a known optimal solution.

Definition at line 1144 of file integer.h.

◆ RegisterReversibleClass()

void operations_research::sat::IntegerTrail::RegisterReversibleClass ( ReversibleInterface * rev )

inline

Registers a reversible class. This class will always be synced with the correct decision level.

Definition at line 1099 of file integer.h.

◆ RegisterWatcher()

void operations_research::sat::IntegerTrail::RegisterWatcher ( SparseBitset< IntegerVariable > * p )

inline

All the registered bitsets will be set to one each time a LbVar is modified. It is up to the client to clear it if it wants to be notified with the newly modified variables.

Definition at line 1069 of file integer.h.

◆ RelaxLinearReason() [1/2]

void operations_research::sat::IntegerTrail::RelaxLinearReason	(	IntegerValue	slack,
		absl::Span< const IntegerValue >	coeffs,
		std::vector< int > *	trail_indices ) const

Same as above but relax the given trail indices.

We start by filtering *trail_indices:

remove all level zero entries.
keep the one that cannot be relaxed.
move the other one to the relax_heap_ (and creating the heap).

We ignore level zero entries.

If the coeff is too large, we cannot relax this entry.

This is a bit hacky, but when it is used from MergeReasonIntoInternal(), we never relax a reason that will not be expanded because it is already part of the current conflict.

Note: both terms of the product are positive.

The slack might have changed since the entry was added.

Relax, and decide what to do with the new value of index.

Same code as in the first block.

If we aborted early because of the slack, we need to push all remaining indices back into the reason.

Definition at line 1062 of file integer.cc.

◆ RelaxLinearReason() [2/2]

void operations_research::sat::IntegerTrail::RelaxLinearReason	(	IntegerValue	slack,
		absl::Span< const IntegerValue >	coeffs,
		std::vector< IntegerLiteral > *	reason ) const

Advanced usage. Given the reason for (Sum_i coeffs[i] * reason[i].var >= current_lb) initially in reason, this function relaxes the reason given that we only need the explanation of (Sum_i coeffs[i] * reason[i].var >= current_lb - slack).

Preconditions:

coeffs must be of same size as reason, and all entry must be positive.
*reason must initially contains the trivial initial reason, that is the current lower-bound of each variables.

Todo
(user): Requiring all initial literal to be at their current bound is not really clean. Maybe we can change the API to only take IntegerVariable and produce the reason directly.

Todo
(user): change API so that this work is performed during the conflict analysis where we can be smarter in how we relax the reason. Note however that this function is mainly used when we have a conflict, so this is not really high priority.

Todo
(user): Test that the code work in the presence of integer overflow.

Todo
(user): Get rid of this function and only keep the trail index one?

Definition at line 1025 of file integer.cc.

◆ RemoveLevelZeroBounds()

void operations_research::sat::IntegerTrail::RemoveLevelZeroBounds ( std::vector< IntegerLiteral > * reason ) const

Removes from the reasons the literal that are always true. This is mainly useful for experiments/testing.

Definition at line 1159 of file integer.cc.

◆ ReportConflict() [1/2]

bool operations_research::sat::IntegerTrail::ReportConflict ( absl::Span< const IntegerLiteral > integer_reason )

inline

Definition at line 1084 of file integer.h.

◆ ReportConflict() [2/2]

bool operations_research::sat::IntegerTrail::ReportConflict	(	absl::Span< const Literal >	literal_reason,
		absl::Span< const IntegerLiteral >	integer_reason )

inline

Helper functions to report a conflict. Always return false so a client can simply do: return integer_trail_->ReportConflict(...);

Definition at line 1076 of file integer.h.

◆ ReserveSpaceForNumVariables()

void operations_research::sat::IntegerTrail::ReserveSpaceForNumVariables ( int num_vars )

Optimization: you can call this before calling AddIntegerVariable() num_vars time.

We only store the domain for the positive variable.

Because we always create both a variable and its negation.

Definition at line 821 of file integer.cc.

◆ RootLevelEnqueue()

bool operations_research::sat::IntegerTrail::RootLevelEnqueue ( IntegerLiteral i_lit )

Sometimes we infer some root level bounds but we are not at the root level. In this case, we will update the level-zero bounds right away, but will delay the current push until the next restart.

Note: if you want to also push the literal at the current level, then just calling Enqueue() is enough. Since there is no reason, the literal will still be recorded properly.

We update right away the level zero bounds, but delay the actual enqueue until we are back at level zero. This allow to properly push any associated literal.

Definition at line 1229 of file integer.cc.

◆ SafeEnqueue()

bool operations_research::sat::IntegerTrail::SafeEnqueue	(	IntegerLiteral	i_lit,
		absl::Span< const IntegerLiteral >	integer_reason )

Enqueue new information about a variable bound. It has the same behavior as the Enqueue() method, except that it accepts true and false integer literals, both for i_lit, and for the integer reason.

This method will do nothing if i_lit is a true literal. It will report a conflict if i_lit is a false literal, and enqueue i_lit normally otherwise. Furthemore, it will check that the integer reason does not contain any false literals, and will remove true literals before calling ReportConflict() or Enqueue().

Note: ReportConflict() deal correctly with constant literals.

Most of our propagation code do not use "constant" literal, so to not have to test for them in Enqueue(), we clear them beforehand.

Definition at line 1252 of file integer.cc.

◆ timestamp()

int64_t operations_research::sat::IntegerTrail::timestamp ( ) const

inline

Definition at line 1061 of file integer.h.

◆ Untrail()

void operations_research::sat::IntegerTrail::Untrail	(	const Trail &	,
		int	trail_index )

finalvirtual

Reverts the state so that all the literals with a trail index greater or equal to the given one are not processed for propagation. Note that the trail current decision level is already reverted before this is called.

Todo: (user): Currently this is called at each Backtrack(), but we could bundle the calls in case multiple conflict one after the other are detected even before the Propagate() call of a SatPropagator is called.

Todo: (user): It is not yet 100% the case, but this can be guaranteed to be called with a trail index that will always be the start of a new decision level.

Note: if a conflict was detected before Propagate() of this class was even called, it is possible that there is nothing to backtrack.

Resize lazy reason.

Clear reason.

We notify the new level once all variables have been restored to their old value.

Reimplemented from operations_research::sat::SatPropagator.

Definition at line 768 of file integer.cc.

◆ UpdateInitialDomain()

bool operations_research::sat::IntegerTrail::UpdateInitialDomain	(	IntegerVariable	var,
		Domain	domain )

Takes the intersection with the current initial variable domain.

Todo: (user): There is some memory inefficiency if this is called many time because of the underlying data structure we use. In practice, when used with a presolve, this is not often used, so that is fine though.

Note: we don't support optional variable here. Or at least if you set the domain of an optional variable to zero, the problem will be declared unsat.

Update directly the level zero bounds.

Do not forget to update the watchers.

Update the encoding.

Definition at line 886 of file integer.cc.

◆ UpperBound() [1/2]

IntegerValue operations_research::sat::IntegerTrail::UpperBound ( AffineExpression expr ) const

inline

Definition at line 1775 of file integer.h.

◆ UpperBound() [2/2]

IntegerValue operations_research::sat::IntegerTrail::UpperBound ( IntegerVariable i ) const

inline

Definition at line 1721 of file integer.h.

◆ UpperBoundAsLiteral() [1/2]

IntegerLiteral operations_research::sat::IntegerTrail::UpperBoundAsLiteral ( AffineExpression expr ) const

inline

Definition at line 1796 of file integer.h.

◆ UpperBoundAsLiteral() [2/2]

IntegerLiteral operations_research::sat::IntegerTrail::UpperBoundAsLiteral ( IntegerVariable i ) const

inline

Definition at line 1765 of file integer.h.

◆ VariableLowerBoundIsFromLevelZero()

bool operations_research::sat::IntegerTrail::VariableLowerBoundIsFromLevelZero ( IntegerVariable var ) const

inline

Returns true if the variable lower bound is still the one from level zero.

Definition at line 1093 of file integer.h.

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

ortools/sat/integer.h
ortools/sat/integer.cc

Public Member Functions

Additional Inherited Members

Detailed Description

Constructor & Destructor Documentation

◆ IntegerTrail() [1/2]

◆ IntegerTrail() [2/2]

◆ ~IntegerTrail()

Member Function Documentation

◆ AddAllGreaterThanConstantReason()

◆ AddIntegerVariable() [1/3]

◆ AddIntegerVariable() [2/3]

◆ AddIntegerVariable() [3/3]

◆ AppendNewBounds()

◆ AppendNewBoundsFrom()

◆ AppendRelaxedLinearReason()

◆ ConditionalEnqueue()

◆ ConditionalLowerBound() [1/2]

◆ ConditionalLowerBound() [2/2]

◆ ConditionalUpperBound() [1/2]

◆ ConditionalUpperBound() [2/2]

◆ CurrentBranchHadAnIncompletePropagation()

◆ Enqueue() [1/3]

◆ Enqueue() [2/3]

◆ Enqueue() [3/3]

◆ EnqueueLiteral()

◆ EnqueueWithLazyReason()

◆ FindTrailIndexOfVarBefore()

◆ FirstUnassignedVariable()

◆ FixedValue() [1/2]

◆ FixedValue() [2/2]

◆ GetOrCreateConstantIntegerVariable()

◆ HasPendingRootLevelDeduction()

◆ Index()

◆ InitialVariableDomain()

◆ InPropagationLoop()

◆ IntegerLiteralIsFalse()

◆ IntegerLiteralIsTrue()

◆ IsFixed() [1/2]

◆ IsFixed() [2/2]

◆ IsFixedAtLevelZero() [1/2]

◆ IsFixedAtLevelZero() [2/2]

◆ LevelZeroLowerBound() [1/2]

◆ LevelZeroLowerBound() [2/2]

◆ LevelZeroUpperBound() [1/2]

◆ LevelZeroUpperBound() [2/2]

◆ LowerBound() [1/2]

◆ LowerBound() [2/2]

◆ LowerBoundAsLiteral() [1/2]

◆ LowerBoundAsLiteral() [2/2]

◆ LowerBoundsData()

◆ MergeReasonInto()

◆ NextVariableToBranchOnInPropagationLoop()

◆ NotifyThatPropagationWasAborted()

◆ num_enqueues()

◆ num_level_zero_enqueues()

◆ NumConstantVariables()

◆ NumIntegerVariables()

◆ operator=()

◆ Propagate()

◆ Reason()

◆ ReasonFor()

◆ RegisterDebugChecker()

◆ RegisterReversibleClass()

◆ RegisterWatcher()

◆ RelaxLinearReason() [1/2]

◆ RelaxLinearReason() [2/2]

◆ RemoveLevelZeroBounds()

◆ ReportConflict() [1/2]

◆ ReportConflict() [2/2]

◆ ReserveSpaceForNumVariables()

◆ RootLevelEnqueue()

◆ SafeEnqueue()

◆ timestamp()

◆ Untrail()

◆ UpdateInitialDomain()

◆ UpperBound() [1/2]

◆ UpperBound() [2/2]

◆ UpperBoundAsLiteral() [1/2]

◆ UpperBoundAsLiteral() [2/2]

◆ VariableLowerBoundIsFromLevelZero()