operations_research::sat::CpModelPresolver Class Reference

#include <cp_model_presolve.h>

Public Member Functions
	CpModelPresolver (PresolveContext *context, std::vector< int > *postsolve_mapping)
CpSolverStatus	Presolve ()
bool	PresolveOneConstraint (int c)
	Executes presolve method for the given constraint. Public for testing only.
void	RemoveEmptyConstraints ()
	Visible for testing.
void	DetectDuplicateColumns ()
void	DetectDifferentVariables ()
	Detects variable that must take different values.

Detailed Description

Presolves the initial content of presolved_model.

This also creates a mapping model that encode the correspondence between the two problems. This works as follow:

• The first variables of mapping_model are in one to one correspondence with the variables of the initial model.
• The presolved_model variables are in one to one correspondence with the variable at the indices given by postsolve_mapping in the mapping model.
• Fixing one of the two sets of variables and solving the model will assign the other set to a feasible solution of the other problem. Moreover, the objective value of these solutions will be the same. Note that solving such problems will take little time in practice because the propagation will basically do all the work.

Note(user): an optimization model can be transformed into a decision problem, if for instance the objective is fixed, or independent from the rest of the problem.

Todo

(user): Identify disconnected components and returns a vector of presolved model? If we go this route, it may be nicer to store the indices inside the model. We can add a IntegerVariableProto::initial_index;

Definition at line 76 of file cp_model_presolve.h.

Constructor & Destructor Documentation

CpModelPresolver()

operations_research::sat::CpModelPresolver::CpModelPresolver	(	PresolveContext *	context,
		std::vector< int > *	postsolve_mapping )

Definition at line 13063 of file cp_model_presolve.cc.

Member Function Documentation

DetectDifferentVariables()

void operations_research::sat::CpModelPresolver::DetectDifferentVariables

(

)

Detects variable that must take different values.

List the variable that are pairwise different, also store in offset[x, y] the offsets such that x >= y + offset.second OR y >= x + offset.first.

Process the fact "v1 - v2 \in Domain".

We have x - y not in exclusion, so x - y > exclusion.Max() --> x > y + exclusion.Max(); OR x - y < exclusion.Min() --> y > x - exclusion.Min();

Try to find identical linear constraint with incompatible domains. This works really well on neos16.mps.gz where we have a <=> x <= y b <=> x >= y and a => not(b), Because of this presolve, we detect that not(a) => b and thus that a and not(b) are equivalent. We can thus simplify the problem to just a => x < y not(a) => x > y

Todo

(user): On that same problem, we could actually just have x != y and remove the enforcement literal that is just used for that. But then we will just re-create it, since we don't have a native way to handle x != y.

Todo

(user): Again on neos16.mps, we actually have cliques of x != y so we end up with a bunch of groups of 7 variables in [0, 6] that are all different. If we can detect that, then we close the problem quickly instead of not closing it.

Detect direct encoding of x != y. Note that we also see that from x > y and related.

We assume the constraint was already divided by its gcd.

Todo

(user): Handle this case?

Detect x != y via lit => x > y && not(lit) => x < y.

We have x - y in domain1 or in domain2, so it must be in the union.

We assume the constraint was already divided by its gcd.

Detect all_different cliques. We reuse the max-clique code from sat.

Todo

(user): To avoid doing that more than once, we only run it if there is no all-diff in the model already. This is not perfect.

Note(user): The all diff added here will not be expanded since we run this after expansion. This is fragile though. Not even sure this is what we want.

Todo

(user): Start with the existing all diff and expand them rather than not running this if there are all_diff present.

Todo

(user): Only add them at the end of the presolve! it hurt our presolve (like probing is slower) and only serve for linear relaxation.

All variables at false is always a valid solution of the local model, so this should never return UNSAT.

We have an all-diff, but inspect the offsets to see if we have a disjunctive ! Note that this is quadratic, but no more complex than the scan of the model we just did above, since we had one linear constraint per entry.

When this happens, it means this interval can never be before any other. We should probably handle this case better, but for now we abort.

We have one size greater than 1, lets add a no_overlap!

Todo

(user): try to remove all the quadratic boolean and their corresponding linear2 ? Any Boolean not used elsewhere could be removed.

Definition at line 10157 of file cp_model_presolve.cc.

DetectDuplicateColumns()

void operations_research::sat::CpModelPresolver::DetectDuplicateColumns

(

)

Note

our symmetry-detector will also identify full permutation group for these columns, but it is better to handle that even before. We can also detect variable with different domains but with indentical columns.

Our current implementation require almost a full copy. First construct a transpose var to columns (constraint_index, coeff).

We will only support columns that include:

• objective
• linear (non-enforced part)

• at_most_one/exactly_one/clauses (but with positive variable only).

  Todo

  (user): deal with enforcement_literal, especially bool_and. It is a bit annoying to have to deal with all kind of constraints. Maybe convert bool_and to at_most_one first? We already do that in other places. Note however that an at most one of size 2 means at most 2 columns can be identical. If we have a bool and with many term on the left, all column could be indentical, but we have to linearize the constraint first.

It is okay to ignore terms (the columns will not be full).

Use kObjectiveConstraint (-1) for the objective.

Todo

(user): deal with equivalent column with different objective value. It might not be easy to presolve, but we can at least have a single variable = sum of var appearing only in objective. And we can transfer the min cost.

Now construct the graph.

Find duplicate columns using an hash map. We only consider "full" columns. var -> var_representative using columns hash/comparison.

Todo

(user): If we have duplicate columns appearing in Boolean constraint we can only easily substitute if the sum of columns is a Boolean (i.e. if it appear in an at most one or exactly one). Otherwise we will need to transform such constraint to linear, do that?

Process duplicates.

Since columns are the same, we can introduce a new variable = sum all columns. Note that the linear expression will not overflow, but the overflow check also requires that max_sum < int_max/2, which might happen.

In the corner case where there is a lot of holes in the domain, and the sum domain is too complex, we skip. Hopefully this should be rare.

Deal with objective right away.

Lets rescan the model, and remove all variables, replacing them by the sum. We do that in one O(model size) pass.

Deal with bool case.

Todo

(user): maybe converting to linear + single code is better?

Todo

(user): clear amo/exo of size 1.

Deal with linear case.

We removed all occurrence of "var_to_remove" so we can remove them now.

Note

since we introduce a new variable per equivalence class, we remove one less for each equivalent class.

Definition at line 9532 of file cp_model_presolve.cc.

Presolve()

CpSolverStatus operations_research::sat::CpModelPresolver::Presolve

(

)

We returns the status of the problem after presolve:

• UNKNOWN if everything was ok.
• INFEASIBLE if the model was proven so during presolve
• MODEL_INVALID if the model caused some issues, like if we are not able to scale a floating point objective with enough precision.

The presolve works as follow:

First stage: We will process all active constraints until a fix point is reached. During this stage:

• Variable will never be deleted, but their domain will be reduced.
• Constraint will never be deleted (they will be marked as empty if needed).
• New variables and new constraints can be added after the existing ones.
• Constraints are added only when needed to the mapping_problem if they are needed during the postsolve.

Second stage:

• All the variables domain will be copied to the mapping_model.
• Everything will be remapped so that only the variables appearing in some constraints will be kept and their index will be in [0, num_new_variables).

If the objective is a floating point one, we scale it.

Todo

(user): We should probably try to delay this even more. For that we just need to isolate more the "dual" reduction that usually need to look at the objective.

At this point, we didn't create any new variables, so the integer objective is in term of the orinal problem variables. We save it so that we can expose to the user what exact objective we are actually optimizing.

If there is a large proprotion of fixed variable, lets remap the model before we start the actual presolve. This is useful for LNS in particular.

fixed_postsolve_mapping[i] will contains the original index of the variable that will be at position i after MaybeRemoveFixedVariables(). If the mapping is left empty, it will be set to the identity mapping later by InitializeMappingModelVariables().

Initialize the initial context.working_model domains. Initialize the objective and the constraint <-> variable graph.

Note

we did some basic presolving during the first copy of the model. This is important has initializing the constraint <-> variable graph can be costly, so better to remove trivially feasible constraint for instance.

If presolve is false, just run expansion.

We still write back the canonical objective has we don't deal well with uninitialized domain or duplicate variables.

We need to append all the variable equivalence that are still used!

Make sure we also have an initialized mapping model as we use this for filling the tightened variables. Even without presolve, we do some trivial presolving during the initial copy of the model, and expansion might do more.

We don't want to run postsolve when the presolve is disabled, but the expansion might have added some constraints to the mapping model. To restore correctness, we merge them with the working model.

Presolve all variable domain once. The PresolveToFixPoint() function will only reprocess domain that changed.

Try to canonicalize the domain, note that we should have detected all affine relations before, so we don't recreate "canononical" variables if they already exist in the model.

Main propagation loop.

Propagate the objective.

Todo

(user): The presolve transformations we do after this is called might result in even more presolve if we were to call this again! improve the code. See for instance plusexample_6_sat.fzn were represolving the presolved problem reduces it even more.

Call expansion.

We need to re-evaluate the degree because some presolve rule only run after expansion.

We run the symmetry before more complex presolve rules as many of them are heuristic based and might break the symmetry present in the original problems. This happens for example on the flatzinc wordpress problem.

Todo

(user): Decide where is the best place for this.

Todo

(user): try not to break symmetry in our clique extension or other more advanced presolve rule? Ideally we could even exploit them. But in this case, it is still good to compute them early.

Both kind of duplications might introduce a lot of symmetries and we want to do that before we even compute them.

If the presolve always keep symmetry, we compute it once and for all.

We distinguish an empty symmetry message meaning that symmetry were computed and there is none, and the absence of symmetry message meaning we don't know.

Todo

(user): Maybe this is a bit brittle. Also move this logic to DetectAndAddSymmetryToProto() ?

Runs SAT specific presolve on the pure-SAT part of the problem.

Note

because this can only remove/fix variable not used in the other part of the problem, there is no need to redo more presolve afterwards.

Extract redundant at most one constraint from the linear ones.

Todo

(user): more generally if we do some probing, the same relation will be detected (and more). Also add an option to turn this off?

Todo

(user): instead of extracting at most one, extract pairwise conflicts and add them to bool_and clauses? this is some sort of small scale probing, but good for sat presolve and clique later?

Deal with pair of constraints.

Todo

(user): revisit when different transformation appear.

Todo

Todo

(user): merge these code instead of doing many passes?

These operations might break symmetry. Or at the very least, the newly created variable must be incorporated in the generators.

Heuristic: vertical introduce smaller defining constraint and appear in many constraints, so might be more constrained. We might also still make horizontal rectangle with the variable introduced.

We do that after the duplicate, SAT and SetPPC constraints.

Merge clauses that differ in just one literal. Heuristic use at_most_one to try to tighten the initial LP Relaxation.

The TransformIntoMaxCliques() call above transform all bool and into at most one of size 2. This does the reverse and merge them.

Call the main presolve to remove the fixed variables and do more deductions.

Exit the loop if no operations were performed.

Todo

(user): try to be smarter and avoid looping again if little changed.

Regroup no-overlaps into max-cliques.

Tries to spread the objective amongst many variables. We re-do a canonicalization with the final linear expression.

If we have fixed variables or created new affine relations, there might be more things to presolve.

We re-do a canonicalization with the final linear expression.

Now that everything that could possibly be fixed was fixed, make sure we don't leave any linear constraint with fixed variables.

Take care of linear constraint with a complex rhs.

Adds all needed affine relation to context_->working_model.

If we have symmetry information, lets filter it.

The strategy variable indices will be remapped in ApplyVariableMapping() but first we use the representative of the affine relations for the variables that are not present anymore.

Note

we properly take into account the sign of the coefficient which will result in the same domain reduction strategy. Moreover, if the variable order is not CHOOSE_FIRST, then we also encode the associated affine transformation in order to preserve the order.

Canonicalize each expression to use affine representative.

Remove fixed expression and affine corresponding to same variables.

Sync the domains and initialize the mapping model variables.

Remove all the unused variables from the presolved model.

Heuristic: If a variable is removed and has a representative that is not, we "move" the representative to the spot of that variable in the original order. This is to preserve any info encoded in the variable order by the modeler.

Deal with unused variables.

If the variable is not fixed, we have multiple feasible solution for this variable, so we can't remove it if we want all of them.

Tricky. Variables that where not removed by a presolve rule should be fixed first during postsolve, so that more complex postsolve rules can use their values. One way to do that is to fix them here.

We prefer to fix them to zero if possible.

Merge identical constant. Note that the only place were constant are still left are in the circuit and route constraint for fixed arcs.

The mapping might merge variable, so we have to be careful here.

Compact all non-empty constraint at the beginning.

Hack to display the number of deductions stored.

Stats and checks.

This is not supposed to happen, and is more indicative of an error than an INVALID model. But for our no-overflow preconditions, we might run into bad situation that causes the final model to be invalid.

Definition at line 13195 of file cp_model_presolve.cc.

PresolveOneConstraint()

bool operations_research::sat::CpModelPresolver::PresolveOneConstraint

(

int

c

)

Executes presolve method for the given constraint. Public for testing only.

Generic presolve to exploit variable/literal equivalence.

Generic presolve for reified constraint.

Call the presolve function for this constraint if any.

We first propagate the domains before calling this presolve rule.

There is no need to re-do a propagation here, but the constraint size might have been reduced.

If we extracted some enforcement, we redo some presolve.

For 2D, we don't exploit index duplication between x/y so it is not important to do it beforehand. Moreover in some situation PresolveNoOverlap2D() remove a lot of interval, so better to do it afterwards.

Definition at line 8785 of file cp_model_presolve.cc.

RemoveEmptyConstraints()

void operations_research::sat::CpModelPresolver::RemoveEmptyConstraints

(

)

Visible for testing.

Remove all empty constraints and duplicated intervals. Note that we need to remap the interval references.

Now that they have served their purpose, we also remove dummy constraints, otherwise that causes issue because our model are invalid in tests.

Warning

interval_representative_ holds a pointer to the working model to compute hashes, so we need to be careful about not changing a constraint after its index is added to the map.

Definition at line 122 of file cp_model_presolve.cc.

---

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

• ortools/sat/cp_model_presolve.h
• ortools/sat/cp_model_presolve.cc