#include <linear_constraint_manager.h>

Public Member Functions
	LinearConstraintSymmetrizer (Model *model)

	~LinearConstraintSymmetrizer ()

void	AddSymmetryOrbit (IntegerVariable sum_var, absl::Span< const IntegerVariable > orbit)

bool	HasSymmetry () const

int	NumOrbits () const
	Accessors by orbit index in [0, num_orbits).

IntegerVariable	OrbitSumVar (int i) const

absl::Span< const IntegerVariable >	Orbit (int i) const

int	OrbitIndex (IntegerVariable var) const

bool	IsOrbitSumVar (IntegerVariable var) const
	Returns true iff var is one of the sum_var passed to AddSymmetryOrbit().

bool	AppearInFoldedProblem (IntegerVariable var) const

bool	FoldLinearConstraint (LinearConstraint ct, bool folded=nullptr)

Detailed Description

Knowing the symmetry of the IP problem should allow us to solve the LP faster via "folding" techniques.

You can read this for the LP part: "Dimension Reduction via Colour Refinement", Martin Grohe, Kristian Kersting, Martin Mladenov, Erkal Selman, https://arxiv.org/abs/1307.5697

In the presence of symmetry, by considering all symmetric version of a constraint and summing them, we can derive a new constraint using the sum of the variable on each orbit instead of the individual variables.

For the integration in a MIP solver, I couldn't find many reference. The way I did it here is to introduce for each orbit a variable representing the sum of the orbit variable. This allows to represent the folded LP in terms of these variables (that are connected to the rest of the solver) and just reuse the full machinery.

There are related info in "Orbital Shrinking", Matteo Fischetti & Leo Liberti, https://link.springer.com/chapter/10.1007/978-3-642-32147-4_6

Definition at line 85 of file linear_constraint_manager.h.

Constructor & Destructor Documentation

◆ LinearConstraintSymmetrizer()

operations_research::sat::LinearConstraintSymmetrizer::LinearConstraintSymmetrizer ( Model * model )

inlineexplicit

Definition at line 87 of file linear_constraint_manager.h.

◆ ~LinearConstraintSymmetrizer()

operations_research::sat::LinearConstraintSymmetrizer::~LinearConstraintSymmetrizer ( )

Definition at line 53 of file linear_constraint_manager.cc.

Member Function Documentation

◆ AddSymmetryOrbit()

void operations_research::sat::LinearConstraintSymmetrizer::AddSymmetryOrbit	(	IntegerVariable	sum_var,
		absl::Span< const IntegerVariable >	orbit )

This must be called with all orbits before we call FoldLinearConstraint().

Note: sum_var MUST not be in any of the orbits. All orbits must also be disjoint.

Precondition: All IntegerVariable must be positive.

Store the orbit info.

And fill var_to_orbit_index_.

Definition at line 60 of file linear_constraint_manager.cc.

◆ AppearInFoldedProblem()

bool operations_research::sat::LinearConstraintSymmetrizer::AppearInFoldedProblem ( IntegerVariable var ) const

This will be only true for variable not appearing in any orbit and for the orbit sum variables.

Definition at line 210 of file linear_constraint_manager.cc.

◆ FoldLinearConstraint()

bool operations_research::sat::LinearConstraintSymmetrizer::FoldLinearConstraint	(	LinearConstraint *	ct,
		bool *	folded = nullptr )

Given a constraint on the "original" model variables, try to construct a symmetric version of it using the orbit sum variables. This might fail if we encounter integer overflow. Returns true on success. On failure, the original constraints will not be usable.

Preconditions: All IntegerVariable must be positive. And the constraint lb/ub must be tight and not +/- int64_t max.

What we do here is basically equivalent to adding all the possible permutations (under the problem symmetry group) of the constraint together. When we do that all variables in the same orbit will have the same coefficient (

Todo: (user): think how to prove this properly and especially that the scaling is in 1/orbit_size) and will each appear once. We then substitute each sum by the sum over the orbit, and divide coefficient by their gcd.

Any solution of the original LP can be transformed to a solution of the folded LP with the same objective. So the folded LP will give us a tight and valid objective lower bound but with a lot less variables! This is an adaptation of "LP folding" to use in a MIP context. Introducing the orbit sum allow to propagates and add cuts as these sum are still integer for us.

The only issue is regarding scaling of the constraints. Basically each orbit sum variable will appear with a factor 1/orbit_size in the original constraint.

We will remap & scale the constraint. If not possible, we will drop it for now.

We assume the constraint had basic preprocessing with tight lb/ub for instance. First pass is to compute the scaling factor.

If we have an orbit of size one, or the variable is its own representative (orbit sum), skip.

Update the scaling factor.

No symmetric variables.

We need to multiply each term by scaling_factor / orbit_size.

Todo: (user): Now that we know the actual coefficient we could scale less. Maybe the coefficient of an orbit_var is already divisible by orbit_size.

Dividing by gcd can help.

Todo: (user): In some cases, this constraint will propagate/fix directly the orbit sum variables, we might want to propagate this in the cp world? This migth also remove bad scaling.

Definition at line 105 of file linear_constraint_manager.cc.