C++ Reference: class UpperBoundedLinearConstraint

Note: 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: uint64_t 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.