operations_research::sat::ActivityBoundHelper Class Reference

#include <presolve_util.h>

Public Member Functions
	ActivityBoundHelper ()=default
void	ClearAtMostOnes ()
void	AddAtMostOne (absl::Span< const int > amo)
void	AddAllAtMostOnes (const CpModelProto &proto)
int64_t	ComputeMaxActivity (absl::Span< const std::pair< int, int64_t > > terms, std::vector< std::array< int64_t, 2 > > *conditional=nullptr)
int64_t	ComputeMinActivity (absl::Span< const std::pair< int, int64_t > > terms, std::vector< std::array< int64_t, 2 > > *conditional=nullptr)
bool	PresolveEnforcement (absl::Span< const int > refs, ConstraintProto *ct, absl::flat_hash_set< int > *literals_at_true)
int	RemoveEnforcementThatMakesConstraintTrivial (absl::Span< const std::pair< int, int64_t > > boolean_terms, const Domain &other_terms, const Domain &rhs, ConstraintProto *ct)
std::vector< absl::Span< const int > >	PartitionLiteralsIntoAmo (absl::Span< const int > literals)
	Similar algo as above for this simpler case.
bool	IsAmo (absl::Span< const int > literals)
	Returns true iff the given literal are in at most one relationship.
int	NumAmoForVariable (int var) const
	Returns in how many amo var or Not(var) are part of.

Detailed Description

Try to get more precise min/max activity of a linear constraints using at most ones from the model. This is heuristic based but should be relatively fast.

Todo

(user): Use better algorithm. The problem is the same as finding upper bound to the classic problem: maximum-independent set in a graph. We also only use at most ones, but we could use the more general binary implication graph.

Definition at line 167 of file presolve_util.h.

Constructor & Destructor Documentation

ActivityBoundHelper()

operations_research::sat::ActivityBoundHelper::ActivityBoundHelper ( )

default

Member Function Documentation

AddAllAtMostOnes()

void operations_research::sat::ActivityBoundHelper::AddAllAtMostOnes

(

const CpModelProto &

proto

)

Todo

(user): Add long ones first, or at least the ones of size 2 after.

a => b same as amo(a, not(b)).

Definition at line 284 of file presolve_util.cc.

AddAtMostOne()

void operations_research::sat::ActivityBoundHelper::AddAtMostOne

(

absl::Span< const int >

amo

)

Add it.

Definition at line 263 of file presolve_util.cc.

ClearAtMostOnes()

void operations_research::sat::ActivityBoundHelper::ClearAtMostOnes

(

)

The at most one constraint must be added before linear constraint are processed. The functions below will still works, but do nothing more than compute trivial bounds.

Definition at line 258 of file presolve_util.cc.

ComputeMaxActivity()

int64_t operations_research::sat::ActivityBoundHelper::ComputeMaxActivity ( absl::Span< const std::pair< int, int64_t > > terms, std::vector< std::array< int64_t, 2 > > * conditional = nullptr )

inline

Computes the max/min activity of a linear expression involving only Booleans.

Accepts a list of (literal, coefficient). Note that all literal will be interpreted as referring to [0, 1] variables. We use the CpModelProto convention for negated literal index.

If conditional is not nullptr, then conditional[i][0/1] will give the max activity if the literal at position i is false/true. This can be used to fix variables or extract enforcement literal.

Important: We shouldn't have duplicates or a lit and NegatedRef(lit) appearing both.

Note

the result of this function is not exact (it uses an heuristic to detect AMOs), but it does not depend on the order of the input terms, so passing an input in non-deterministic order is fine.

Todo

(user): Indicate when the bounds are trivial (i.e. not intersection with any amo) so that we don't waste more time processing the result?

Definition at line 198 of file presolve_util.h.

ComputeMinActivity()

int64_t operations_research::sat::ActivityBoundHelper::ComputeMinActivity ( absl::Span< const std::pair< int, int64_t > > terms, std::vector< std::array< int64_t, 2 > > * conditional = nullptr )

inline

Definition at line 203 of file presolve_util.h.

IsAmo()

bool operations_research::sat::ActivityBoundHelper::IsAmo

(

absl::Span< const int >

literals

)

Returns true iff the given literal are in at most one relationship.

Definition at line 467 of file presolve_util.cc.

NumAmoForVariable()

int operations_research::sat::ActivityBoundHelper::NumAmoForVariable ( int var ) const

inline

Returns in how many amo var or Not(var) are part of.

Definition at line 238 of file presolve_util.h.

PartitionLiteralsIntoAmo()

std::vector< absl::Span< const int > > operations_research::sat::ActivityBoundHelper::PartitionLiteralsIntoAmo

(

absl::Span< const int >

literals

)

Similar algo as above for this simpler case.

Partition the list of literals into disjoint at most ones. The returned spans are only valid until another function from this class is used.

New element.

We have the partition, lets construct the spans now.

Definition at line 415 of file presolve_util.cc.

PresolveEnforcement()

bool operations_research::sat::ActivityBoundHelper::PresolveEnforcement	(	absl::Span< const int >	refs,
		ConstraintProto *	ct,
		absl::flat_hash_set< int > *	literals_at_true )

Computes relevant info to presolve a constraint with enforcement using at most one information.

This returns false iff the enforcement list cannot be satisfied. It filters the enforcement list if some are consequences of other. It fills the given set with the literal that must be true due to the enforcement. Note that only literals or negated literal appearing in ref are filled.

If a previous enforcement literal implies this one, we can skip it.

Tricky: We need to do that before appending the amo containing ref in case an amo contains both ref and not(ref).

Todo

(user): Ideally these amo should not be added to this class.

If some other literal is at one in this amo, literal must be false, and so the constraint cannot be enforced.

Keep this enforcement.

Skip already fixed.

If some other literal is at one in this amo, literal must be false.

Definition at line 539 of file presolve_util.cc.

RemoveEnforcementThatMakesConstraintTrivial()

int operations_research::sat::ActivityBoundHelper::RemoveEnforcementThatMakesConstraintTrivial	(	absl::Span< const std::pair< int, int64_t > >	boolean_terms,
		const Domain &	other_terms,
		const Domain &	rhs,
		ConstraintProto *	ct )

For each enforcement literal enf, if not(enf) implies that the constraint is trivial, then we can just remove not(enf) from the list.

Actually, we could even "lift" such enforcement so that if it is negative the constraint is still trivial but tighter.

Compute min_max activity when enf_lit is false.

This is not supposed to happen after PresolveEnforcement(), so we just abort in this case.

Similarly, this is not supposed to happen after PresolveEnforcement().

Definition at line 598 of file presolve_util.cc.

---

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

• ortools/sat/presolve_util.h
• ortools/sat/presolve_util.cc