C++ Reference: class UpperBoundedLinearConstraint

This documentation is automatically generated.

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.
Method
activity

Return type: double

AddToConflict

Return type: void

Arguments: 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.

already_propagated_end

Return type: int

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

ComputeCancelation

Return type: Coefficient

Arguments: 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.

FillReason

Return type: void

Arguments: 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).

hash

Return type: int64

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

HasIdenticalTerms

Return type: bool

Arguments: const std::vector<LiteralWithCoeff>& cst

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

InitializeRhs

Return type: bool

Arguments: 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.

is_learned

Return type: bool

is_marked_for_deletion

Return type: bool

is_used_as_a_reason

Return type: bool

MarkForDeletion

Return type: void

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

Propagate

Return type: bool

Arguments: 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.

ResolvePBConflict

Return type: void

Arguments: 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.

Rhs

Return type: Coefficient

set_activity

Return type: void

Arguments: double activity

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

set_is_learned

Return type: void

Arguments: bool is_learned

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

Untrail

Return type: void

Arguments: 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.

UpperBoundedLinearConstraint

Return type: explicit

Arguments: const std::vector<LiteralWithCoeff>& cst

Takes a pseudo-Boolean formula in canonical form.