#include <pb_constraint.h>

Public Member Functions
	UpperBoundedLinearConstraint (const std::vector< LiteralWithCoeff > &cst)
	Takes a pseudo-Boolean formula in canonical form.

bool	HasIdenticalTerms (absl::Span< const LiteralWithCoeff > cst)
	Returns true if the given terms are the same as the one in this constraint.

Coefficient	Rhs () const

bool	InitializeRhs (Coefficient rhs, int trail_index, Coefficient threshold, Trail trail, PbConstraintsEnqueueHelper *helper)

bool	Propagate (int trail_index, Coefficient threshold, Trail trail, PbConstraintsEnqueueHelper *helper)

void	Untrail (Coefficient *threshold, int trail_index)

void	FillReason (const Trail &trail, int source_trail_index, BooleanVariable propagated_variable, std::vector< Literal > *reason)

void	ResolvePBConflict (const Trail &trail, BooleanVariable var, MutableUpperBoundedLinearConstraint conflict, Coefficient conflict_slack)

void	AddToConflict (MutableUpperBoundedLinearConstraint *conflict)

Coefficient	ComputeCancelation (const Trail &trail, int trail_index, const MutableUpperBoundedLinearConstraint &conflict)

void	MarkForDeletion ()
	API to mark a constraint for deletion before actually deleting it.

bool	is_marked_for_deletion () const

void	set_is_learned (bool is_learned)

bool	is_learned () const

bool	is_used_as_a_reason () const

void	set_activity (double activity)

double	activity () const

uint64_t	hash () const

int	already_propagated_end () const

Detailed Description

This class contains half the propagation logic for a constraint of the form

sum ci * li <= rhs, ci positive coefficients, li literals.

The other half is implemented by the PbConstraints class below which takes care of updating the 'threshold' value of this constraint:

'slack' is rhs minus all the ci of the variables xi assigned to true. Note that it is not updated as soon as xi is assigned, but only later when this assignment is "processed" by the PbConstraints class.
'threshold' is the distance from 'slack' to the largest coefficient ci smaller or equal to slack. By definition, all the literals with even larger coefficients that are yet 'processed' must be false for the constraint to be satisfiable.

Definition at line 386 of file pb_constraint.h.

Constructor & Destructor Documentation

◆ UpperBoundedLinearConstraint()

operations_research::sat::UpperBoundedLinearConstraint::UpperBoundedLinearConstraint ( const std::vector< LiteralWithCoeff > & cst )

explicit

Takes a pseudo-Boolean formula in canonical form.

Reserve the space for coeffs_ and starts_ (it is slightly more efficient).

Sentinel.

Definition at line 404 of file pb_constraint.cc.

Member Function Documentation

◆ activity()

double operations_research::sat::UpperBoundedLinearConstraint::activity ( ) const

inline

Definition at line 481 of file pb_constraint.h.

◆ AddToConflict()

void operations_research::sat::UpperBoundedLinearConstraint::AddToConflict ( MutableUpperBoundedLinearConstraint * conflict )

Adds this pb constraint into the given mutable one.

Todo: (user): Provides instead an easy to use iterator over an UpperBoundedLinearConstraint and move this function to MutableUpperBoundedLinearConstraint.

Definition at line 444 of file pb_constraint.cc.

◆ already_propagated_end()

int operations_research::sat::UpperBoundedLinearConstraint::already_propagated_end ( ) const

inline

This is used to get statistics of the number of literals inspected by a Propagate() call.

Definition at line 489 of file pb_constraint.h.

◆ ComputeCancelation()

Coefficient operations_research::sat::UpperBoundedLinearConstraint::ComputeCancelation	(	const Trail &	trail,
		int	trail_index,
		const MutableUpperBoundedLinearConstraint &	conflict )

Compute the sum of the "cancelation" in AddTerm() if *this is added to the given conflict. The sum doesn't take into account literal assigned with a trail index smaller than the given one.

Note(user): Currently, this is only used in DCHECKs.

Definition at line 660 of file pb_constraint.cc.

◆ FillReason()

void operations_research::sat::UpperBoundedLinearConstraint::FillReason	(	const Trail &	trail,
		int	source_trail_index,
		BooleanVariable	propagated_variable,
		std::vector< Literal > *	reason )

Provided that the literal with given source_trail_index was the one that propagated the conflict or the literal we wants to explain, then this will compute the reason.

Some properties of the reason:

Literals of level 0 are removed.
It will always contain the literal with given source_trail_index (except if it is of level 0).
We make the reason more compact by greedily removing terms with small coefficients that would not have changed the propagation.

Todo
(user): Maybe it is possible to derive a better reason by using more information. For instance one could use the mask of literals that are better to use during conflict minimization (namely the one already in the 1-UIP conflict).

Optimization for an "at most one" constraint.

Note: the source_trail_index set by InitializeRhs() is ok in this case.

Optimization: This will be set to the index of the last literal in the reason.

Compute the initial reason which is formed by all the literals of the constraint that were assigned to true at the time of the propagation. We remove literals with a level of 0 since they are not needed. We also compute the slack at the time.

In both cases, we can't minimize the reason further.

Remove literals with small coefficients from the reason as long as the limit is still stricly positive.

Definition at line 589 of file pb_constraint.cc.

◆ hash()

uint64_t operations_research::sat::UpperBoundedLinearConstraint::hash ( ) const

inline

Returns a fingerprint of the constraint linear expression (without rhs). This is used for duplicate detection.

Definition at line 485 of file pb_constraint.h.

◆ HasIdenticalTerms()

bool operations_research::sat::UpperBoundedLinearConstraint::HasIdenticalTerms ( absl::Span< const LiteralWithCoeff > cst )

Returns true if the given terms are the same as the one in this constraint.

Definition at line 456 of file pb_constraint.cc.

◆ InitializeRhs()

bool operations_research::sat::UpperBoundedLinearConstraint::InitializeRhs	(	Coefficient	rhs,
		int	trail_index,
		Coefficient *	threshold,
		Trail *	trail,
		PbConstraintsEnqueueHelper *	helper )

Sets the rhs of this constraint. Compute the initial threshold value using only the literal with a trail index smaller than the given one. Enqueues on the trail any propagated literals.

Returns false if the preconditions described in PbConstraints::AddConstraint() are not meet.

Compute the slack from the assigned variables with a trail index smaller than the given trail_index. The variable at trail_index has not yet been propagated.

sum_at_previous_level[i] is the sum of assigned literals with a level < i. Since we want the sums up to sum_at_previous_level[last_level + 1], the size of the vector must be last_level + 2.

The constraint is infeasible provided the current propagated trail.

Cumulative sum.

Check the no-propagation at earlier level precondition.

Initial propagation.

Todo: (user): The source trail index for the propagation reason (i.e. max_relevant_trail_index) may be higher than necessary (for some of the propagated literals). Currently this works with FillReason(), but it was a source of a really nasty bug (see CL 68906167) because of the (rhs == 1) optim. Find a good way to test the logic.

Definition at line 472 of file pb_constraint.cc.

◆ is_learned()

bool operations_research::sat::UpperBoundedLinearConstraint::is_learned ( ) const

inline

Definition at line 475 of file pb_constraint.h.

◆ is_marked_for_deletion()

bool operations_research::sat::UpperBoundedLinearConstraint::is_marked_for_deletion ( ) const

inline

Definition at line 470 of file pb_constraint.h.

◆ is_used_as_a_reason()

bool operations_research::sat::UpperBoundedLinearConstraint::is_used_as_a_reason ( ) const

inline

Definition at line 476 of file pb_constraint.h.

◆ MarkForDeletion()

void operations_research::sat::UpperBoundedLinearConstraint::MarkForDeletion ( )

inline

API to mark a constraint for deletion before actually deleting it.

Definition at line 469 of file pb_constraint.h.

◆ Propagate()

bool operations_research::sat::UpperBoundedLinearConstraint::Propagate	(	int	trail_index,
		Coefficient *	threshold,
		Trail *	trail,
		PbConstraintsEnqueueHelper *	helper )

Tests for propagation and enqueues propagated literals on the trail. Returns false if a conflict was detected, in which case conflict is filled.

Preconditions:

For each "processed" literal, the given threshold value must have been decreased by its associated coefficient in the constraint. It must now be stricly negative.
The given trail_index is the index of a true literal in the trail which just caused threshold to become stricly negative. All literals with smaller index must have been "processed". All assigned literals with greater trail index are not yet "processed".

The threshold is updated to its new value.

Check propagation.

Conflict.

Propagation.

Note: the reason for first_propagated_variable is always a valid reason for literals_[i].Variable() because we process the variable in increasing coefficient order.

Definition at line 546 of file pb_constraint.cc.

◆ ResolvePBConflict()

void operations_research::sat::UpperBoundedLinearConstraint::ResolvePBConflict	(	const Trail &	trail,
		BooleanVariable	var,
		MutableUpperBoundedLinearConstraint *	conflict,
		Coefficient *	conflict_slack )

Same operation as SatSolver::ResolvePBConflict(), the only difference is that here the reason for var is *this.

Compute the constraint activity at the time and the coefficient of the variable var.

The variable must be of the opposite sign in the current conflict.

Special case.

This constraint is already a conflict. Use this one instead to start the resolution.

Todo

(user): Investigate if this is a good idea. It doesn't happen often, but does happened. Maybe we can detect this before in Propagate()? The setup is:

At a given trail_index, var is propagated and added on the trail.
There is some constraint literals assigned to true with a trail index in (trail_index, var.trail_index).
Their sum is high enough to cause a conflict.
But individually, their coefficients are too small to be propagated, so the conflict is not yet detected. It will be when these variables are processed by PropagateNext().

This is the slack of *this for the trail prefix < limit_trail_index.

This is the slack of the conflict at the same level.

Todo: (user): If there is more "cancelation" than the min_coeffs below when we add the two constraints, the resulting slack may be even lower. Taking that into account is probably good.

When we add the two constraints together, the slack of the result for the trail < limit_trail_index - 1 must be negative. We know that its value is <= slack1 + slack2 - min(coeffs), so we have nothing to do if this bound is already negative.

We need to relax one or both of the constraints so the new slack is < 0. Using the relaxation described in ReduceSlackTo(), we can have this new slack bound:

(slack - diff) + (conflict_slack - conflict_diff)

For all diff in [0, slack) For all conflict_diff in [0, conflict_slack)

Is relaxing the constraint with the highest coeff enough?

Just reduce the slack of both constraints to zero.

Todo: (user): The best will be to relax as little as possible.

Relax the conflict.

We apply the same algorithm as the one in ReduceSlackTo() but on the non-mutable representation and add it on the fly into conflict.

Special case if there if no relaxation is needed.

Todo: (user): track the cancelation here so we can update *conflict_slack properly.

And the rhs.

Definition at line 677 of file pb_constraint.cc.

◆ Rhs()

Coefficient operations_research::sat::UpperBoundedLinearConstraint::Rhs ( ) const

inline

Definition at line 394 of file pb_constraint.h.

◆ set_activity()

void operations_research::sat::UpperBoundedLinearConstraint::set_activity ( double activity )

inline

Activity of the constraint. Only low activity constraint will be deleted during the constraint cleanup phase.

Definition at line 480 of file pb_constraint.h.

◆ set_is_learned()

void operations_research::sat::UpperBoundedLinearConstraint::set_is_learned ( bool is_learned )

inline

Only learned constraints are considered for deletion during the constraint cleanup phase. We also can't delete variables used as a reason.

Definition at line 474 of file pb_constraint.h.

◆ Untrail()

void operations_research::sat::UpperBoundedLinearConstraint::Untrail	(	Coefficient *	threshold,
		int	trail_index )

Updates the given threshold and the internal state. This is the opposite of Propagate(). Each time a literal in unassigned, the threshold value must have been increased by its coefficient. This update the threshold to its new value.

Definition at line 825 of file pb_constraint.cc.

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

ortools/sat/pb_constraint.h
ortools/sat/pb_constraint.cc

Public Member Functions

Detailed Description

Constructor & Destructor Documentation

◆ UpperBoundedLinearConstraint()

Member Function Documentation

◆ activity()

◆ AddToConflict()

◆ already_propagated_end()

◆ ComputeCancelation()

◆ FillReason()

◆ hash()

◆ HasIdenticalTerms()

◆ InitializeRhs()

◆ is_learned()

◆ is_marked_for_deletion()

◆ is_used_as_a_reason()

◆ MarkForDeletion()

◆ Propagate()

◆ ResolvePBConflict()

◆ Rhs()

◆ set_activity()

◆ set_is_learned()

◆ Untrail()