operations_research::sat::DualBoundStrengthening Class Reference

#include <var_domination.h>

Public Member Functions
void	Reset (int num_variables)
void	CannotDecrease (absl::Span< const int > refs, int ct_index=-1)
	All constraints should be mapped to one of more call to these functions.
void	CannotIncrease (absl::Span< const int > refs, int ct_index=-1)
void	CannotMove (absl::Span< const int > refs, int ct_index=-1)
template<typename LinearProto>
void	ProcessLinearConstraint (bool is_objective, const PresolveContext &context, const LinearProto &linear, int64_t min_activity, int64_t max_activity, int ct_index=-1)
	Most of the logic here deals with linear constraints.
bool	Strengthen (PresolveContext *context)
int64_t	CanFreelyDecreaseUntil (int ref) const
int	NumDeletedConstraints () const
	Reset on each Strengthen() call.

Detailed Description

This detects variables that can move freely in one direction, or that can move freely as long as their value do not cross a bound.

Todo

(user): This is actually an important step to do before scaling as it can usually reduce really large bounds!

Definition at line 223 of file var_domination.h.

Member Function Documentation

CanFreelyDecreaseUntil()

int64_t operations_research::sat::DualBoundStrengthening::CanFreelyDecreaseUntil ( int ref ) const

inline

The given ref can always freely decrease until the returned value.

Note

this does not take into account the domain of the variable.

Definition at line 256 of file var_domination.h.

CannotDecrease()

void operations_research::sat::DualBoundStrengthening::CannotDecrease	(	absl::Span< const int >	refs,
		int	ct_index = -1 )

All constraints should be mapped to one of more call to these functions.

Todo

(user): No need to set locking_ct_index_[var] if num_locks_[var] > 1

Optim: We cache pointers to avoid refetching them in the loop.

Definition at line 564 of file var_domination.cc.

CannotIncrease()

void operations_research::sat::DualBoundStrengthening::CannotIncrease	(	absl::Span< const int >	refs,
		int	ct_index = -1 )

Optim: We cache pointers to avoid refetching them in the loop.

Definition at line 578 of file var_domination.cc.

CannotMove()

void operations_research::sat::DualBoundStrengthening::CannotMove	(	absl::Span< const int >	refs,
		int	ct_index = -1 )

Optim: We cache pointers to avoid refetching them in the loop.

Definition at line 592 of file var_domination.cc.

NumDeletedConstraints()

int operations_research::sat::DualBoundStrengthening::NumDeletedConstraints ( ) const

inline

Reset on each Strengthen() call.

Definition at line 261 of file var_domination.h.

ProcessLinearConstraint()

template<typename LinearProto>

void operations_research::sat::DualBoundStrengthening::ProcessLinearConstraint	(	bool	is_objective,
		const PresolveContext &	context,
		const LinearProto &	linear,
		int64_t	min_activity,
		int64_t	max_activity,
		int	ct_index = -1 )

Most of the logic here deals with linear constraints.

lb side.

We never want to increase the objective value. Note that if the objective is lower bounded, we checked that on the lb side above.

ub side.

Definition at line 611 of file var_domination.cc.

Reset()

void operations_research::sat::DualBoundStrengthening::Reset ( int num_variables )

inline

Reset the class to a clean state. This must be called before processing the constraints.

Definition at line 227 of file var_domination.h.

Strengthen()

bool operations_research::sat::DualBoundStrengthening::Strengthen

(

PresolveContext *

context

)

Once ALL constraints have been processed, call this to fix variables or reduce their domain if possible.

Note

this also tighten some constraint that are the only one blocking in one direction. Currently we only do that for implication, so that if we have two Booleans such that a + b <= 1 we transform that to = 1 and we remove one variable since we have now an equivalence relation.

Fix to lb?

Fix to ub?

Here we can fix to any value in [ub_limit, lb_limit] that is compatible with the current domain. We prefer zero or the lowest possible magnitude.

Here we can reduce the domain, but we must be careful when the domain has holes.

For detecting near-duplicate constraint that can be made equivalent. hash -> (ct_index, modified ref).

If there is only one blocking constraint, we can simplify the problem in a few situation.

Todo

(user): Cover all the cases.

Todo

(user): Fix variable right away rather than waiting for next call.

If we have an enforcement literal then we can always add the implication "not enforced" => var at its lower bound. If we also have enforced => fixed var, then var is in affine relation with the enforced literal and we can remove one variable.

Todo

(user): We can also deal with more than one enforcement.

Corner case.

Note(user): If we have enforced => var fixed, we could actually just have removed var from the constraint it was implied by another constraint. If not, because of the new affine relation we could remove it right away.

The new affine relation added below can break the hint if hint(enf) is 0. In this case the only constraint blocking ref from decreasing [ct = enf => (var = implied)] does not apply. We can thus set the hint of positive_ref to bound to preserve the hint feasibility.

positive_ref = enf * implied + (1 - enf) * bound.

enf_var = PositiveRef(enf). positive_ref = (1 - enf_var) * implied + enf_var * bound.

If we have a literal, we always add the implication. This seems like a good thing to do.

The new implication can break the hint if hint(enf) is 0 and hint(ref) is 1. In this case the only locking constraint ct does not apply and thus does not prevent decreasing the hint of ref in order to preserve the hint feasibility.

We can add an implication not_enforced => var to its bound ?

We can make enf equivalent to the constraint instead of just =>. This seems useful since internally we always use fully reified encoding.

If it is different, we have an equivalence now, and we can remove the constraint.

Extending ct = "not(ref) => encoding_lit" to an equality can break the hint only if hint(ref) = hint(encoding_lit) = 1. But in this case ct is actually not blocking ref from decreasing. We can thus set its hint to 0 to preserve the hint feasibility.

Extending ct = "not(ref) => not(encoding_lit)" to an equality can break the hint only if hint(encoding_lit) = 0 and hint(ref) = 1. But in this case ct is actually not blocking ref from decreasing. We can thus set its hint to 0 to preserve the hint feasibility.

encoding_lit was maybe a new variable added during this loop, so make sure we cannot go out-of-bound.

The new_ct constraint ref => (var in complement) below can break the hint if hint(var) is not in complement. In this case, set the hint of ref to false. This should be safe since the only constraint blocking ref from decreasing is ct = not(ref) => (var in rhs) – which does not apply when ref is true.

If we have two Booleans, each with a single blocking constraint that is the same if we "swap" the Booleans reference, then we can make the Booleans equivalent. This is because they will be forced to their bad value only if it is needed by the other part of their respective blocking constraints. This is related to the FindAlmostIdenticalLinearConstraints() except that here we can deal with non-equality or enforced constraints.

Todo

(user): Generalize to non-Boolean. Also for Boolean, we might miss some possible reduction if replacing X by 1 - X make a constraint near-duplicate of another.

Todo

(user): We can generalize to non-linear constraint.

Optimization: Skip if this constraint was already used as a single blocking constraint of another variable. If this is the case, it cannot be equivalent to another constraint with "var" substituted, since otherwise var would have two blocking constraint. We can safely skip it. this make sure this is in O(num_entries) and not more.

Already present!

Corner case: We just discovered l => ct and not(l) => ct. So ct must just always be true. And since that was the only blocking constraint for l, we can just set l to an arbitrary value.

We have a true equality. The two ref can be made equivalent.

If the two hints are different, and since both refs have an equivalent blocking constraint, then the constraint is actually not blocking the ref at 1 from decreasing. Hence we can set its hint to false to preserve the hint feasibility despite the new Boolean equality constraint.

We can delete one of the constraint since they are duplicate now.

Other potential cases?

If (a => b) is the only constraint blocking a literal a in the up direction, then we can set a == b !

Recover a => b where a is having an unique up_lock (i.e this constraint).

Note

if many implications are encoded in the same bool_and, we have to be careful that a is appearing in just one of them.

Todo

(user): Make sure implication graph is transitively reduced to not miss such reduction. More generally, this might only use the graph rather than the encoding into bool_and / at_most_one ? Basically if a => all_direct_deduction, we can transform it into a <=> all_direct_deduction if that is interesting. This could always be done on a max-2sat problem in one of the two direction. Also think about max-2sat specific presolve.

Here, we can only add the equivalence if the literal is the only on the lhs, otherwise there is actually more lock.

If hint(a) is false we can always set it to hint(b) since this can only increase its value. If hint(a) is true then hint(b) must be true as well if the hint is feasible, due to the a => b constraint. Setting hint(a) to hint(b) is thus always safe. The opposite is true as well.

Definition at line 725 of file var_domination.cc.

---

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

• ortools/sat/var_domination.h
• ortools/sat/var_domination.cc