operations_research::sat::LevelZeroEquality Class Reference

#include <integer_expr.h>

Inheritance diagram for operations_research::sat::LevelZeroEquality:

Public Member Functions
	LevelZeroEquality (IntegerVariable target, const std::vector< IntegerVariable > &vars, const std::vector< IntegerValue > &coeffs, Model *model)
bool	Propagate () final

Detailed Description

This assumes target = SUM_i coeffs[i] * vars[i], and detects that the target must be of the form (a*X + b).

This propagator is quite specific and runs only at level zero. For now, this is mainly used for the objective variable. As we fix terms with high objective coefficient, it is possible the only terms left have a common divisor. This close app2-2.mps in less than a second instead of running forever to prove the optimal (in single thread).

Definition at line 177 of file integer_expr.h.

Constructor & Destructor Documentation

LevelZeroEquality()

operations_research::sat::LevelZeroEquality::LevelZeroEquality	(	IntegerVariable	target,
		const std::vector< IntegerVariable > &	vars,
		const std::vector< IntegerValue > &	coeffs,
		Model *	model )

Definition at line 487 of file integer_expr.cc.

Member Function Documentation

Propagate()

bool operations_research::sat::LevelZeroEquality::Propagate ( )

finalvirtual

Todo

(user): We could go even further than just the GCD, and do more arithmetic to tighten the target bounds. See for instance a problem like ej.mps.gz that we don't solve easily, but has just 3 variables! the goal is to minimize X, given 31013 X - 41014 Y - 51015 Z = -31013 (all >=0, Y and Z bounded with high values). I know some MIP solvers have a basic linear diophantine equation support.

Todo

(user): Once the GCD is not 1, we could at any level make sure the objective is of the correct form. For now, this only happen in a few miplib problem that we close quickly, so I didn't add the extra code yet.

Implements operations_research::sat::PropagatorInterface.

Definition at line 511 of file integer_expr.cc.

---

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

• ortools/sat/integer_expr.h
• ortools/sat/integer_expr.cc