always-cautious/ortools-clone
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

[CP-SAT] more spans; one more case of preserving hints during presolve; new packing LNS; propagate objective in LNS

Browse Source
This commit is contained in:
Laurent Perron
2024-12-02 17:17:42 +01:00
parent c37c048b75
commit 0ad3c6c19e
23 changed files with 789 additions and 1179 deletions
Download Patch File Download Diff File Expand all files Collapse all files

2
ortools/sat/2d_rectangle_presolve_test.cc
View File

@@ -702,7 +702,7 @@ ShapePath TraceBoundary(
std::string RenderShapes(std::optional<Rectangle> bb,
absl::Span<const Rectangle> rectangles,
const std::vector<SingleShape>& shapes) {
absl::Span<const SingleShape> shapes) {
const std::vector<std::string> colors = {"black", "white", "orange",
"cyan", "yellow", "purple"};
std::stringstream ss;

5
ortools/sat/BUILD.bazel
View File

@@ -949,6 +949,7 @@ cc_library(
"//ortools/util:logging",
"//ortools/util:sorted_interval_list",
"@com_google_absl//absl/log:check",
"@com_google_absl//absl/types:span",
],
)
@@ -1442,6 +1443,7 @@ cc_library(
":cp_model_cc_proto",
":cp_model_utils",
":integer",
":integer_base",
":presolve_context",
":presolve_util",
":util",
@@ -1469,7 +1471,7 @@ cc_test(
srcs = ["var_domination_test.cc"],
deps = [
":cp_model_cc_proto",
":integer",
":integer_base",
":model",
":presolve_context",
":var_domination",
@@ -3207,6 +3209,7 @@ cc_library(
"@com_google_absl//absl/container:flat_hash_set",
"@com_google_absl//absl/log:check",
"@com_google_absl//absl/meta:type_traits",
"@com_google_absl//absl/types:span",
],
)

10
ortools/sat/all_different.cc
View File

@@ -36,8 +36,9 @@ namespace operations_research {
namespace sat {
std::function<void(Model*)> AllDifferentBinary(
const std::vector<IntegerVariable>& vars) {
return [=](Model* model) {
absl::Span<const IntegerVariable> vars) {
return [=, vars = std::vector<IntegerVariable>(vars.begin(), vars.end())](
Model* model) {
// Fully encode all the given variables and construct a mapping value ->
// List of literal each indicating that a given variable takes this value.
//
@@ -97,8 +98,9 @@ std::function<void(Model*)> AllDifferentOnBounds(
}
std::function<void(Model*)> AllDifferentAC(
const std::vector<IntegerVariable>& variables) {
return [=](Model* model) {
absl::Span<const IntegerVariable> variables) {
return [=, variables = std::vector<IntegerVariable>(
variables.begin(), variables.end())](Model* model) {
if (variables.size() < 3) return;
AllDifferentConstraint* constraint = new AllDifferentConstraint(

4
ortools/sat/all_different.h
View File

@@ -36,7 +36,7 @@ namespace sat {
// encodes all the variables and simply enforces a <= 1 constraint on each
// possible values.
std::function<void(Model*)> AllDifferentBinary(
const std::vector<IntegerVariable>& vars);
absl::Span<const IntegerVariable> vars);
// Enforces that the given tuple of variables takes different values.
// Same as AllDifferentBinary() but use a different propagator that only enforce
@@ -62,7 +62,7 @@ std::function<void(Model*)> AllDifferentOnBounds(
//
// This will fully encode variables.
std::function<void(Model*)> AllDifferentAC(
const std::vector<IntegerVariable>& variables);
absl::Span<const IntegerVariable> variables);
// Implementation of AllDifferentAC().
class AllDifferentConstraint : PropagatorInterface {

19
ortools/sat/circuit.cc
View File

@@ -21,6 +21,7 @@
#include "absl/container/flat_hash_set.h"
#include "absl/log/check.h"
#include "absl/meta/type_traits.h"
#include "absl/types/span.h"
#include "ortools/base/logging.h"
#include "ortools/graph/strongly_connected_components.h"
#include "ortools/sat/integer.h"
@@ -33,9 +34,9 @@ namespace operations_research {
namespace sat {
CircuitPropagator::CircuitPropagator(const int num_nodes,
const std::vector<int>& tails,
const std::vector<int>& heads,
const std::vector<Literal>& literals,
absl::Span<const int> tails,
absl::Span<const int> heads,
absl::Span<const Literal> literals,
Options options, Model* model)
: num_nodes_(num_nodes),
options_(options),
@@ -483,7 +484,7 @@ bool NoCyclePropagator::Propagate() {
CircuitCoveringPropagator::CircuitCoveringPropagator(
std::vector<std::vector<Literal>> graph,
const std::vector<int>& distinguished_nodes, Model* model)
absl::Span<const int> distinguished_nodes, Model* model)
: graph_(std::move(graph)),
num_nodes_(graph_.size()),
trail_(model->GetOrCreate<Trail>()) {
@@ -626,8 +627,9 @@ bool CircuitCoveringPropagator::Propagate() {
}
std::function<void(Model*)> ExactlyOnePerRowAndPerColumn(
const std::vector<std::vector<Literal>>& graph) {
return [=](Model* model) {
absl::Span<const std::vector<Literal>> graph) {
return [=, graph = std::vector<std::vector<Literal>>(
graph.begin(), graph.end())](Model* model) {
const int n = graph.size();
std::vector<Literal> exactly_one_constraint;
exactly_one_constraint.reserve(n);
@@ -695,9 +697,10 @@ void LoadSubcircuitConstraint(int num_nodes, const std::vector<int>& tails,
}
std::function<void(Model*)> CircuitCovering(
const std::vector<std::vector<Literal>>& graph,
absl::Span<const std::vector<Literal>> graph,
const std::vector<int>& distinguished_nodes) {
return [=](Model* model) {
return [=, graph = std::vector<std::vector<Literal>>(
graph.begin(), graph.end())](Model* model) {
CircuitCoveringPropagator* constraint =
new CircuitCoveringPropagator(graph, distinguished_nodes, model);
constraint->RegisterWith(model->GetOrCreate<GenericLiteralWatcher>());

13
ortools/sat/circuit.h
View File

@@ -21,6 +21,7 @@
#include "absl/container/btree_set.h"
#include "absl/container/flat_hash_map.h"
#include "absl/types/span.h"
#include "ortools/base/logging.h"
#include "ortools/base/types.h"
#include "ortools/graph/strongly_connected_components.h"
@@ -53,9 +54,9 @@ class CircuitPropagator : PropagatorInterface, ReversibleInterface {
// The constraints take a sparse representation of a graph on [0, n). Each arc
// being present when the given literal is true.
CircuitPropagator(int num_nodes, const std::vector<int>& tails,
const std::vector<int>& heads,
const std::vector<Literal>& literals, Options options,
CircuitPropagator(int num_nodes, absl::Span<const int> tails,
absl::Span<const int> heads,
absl::Span<const Literal> literals, Options options,
Model* model);
// This type is neither copyable nor movable.
@@ -173,7 +174,7 @@ class NoCyclePropagator : PropagatorInterface, ReversibleInterface {
class CircuitCoveringPropagator : PropagatorInterface, ReversibleInterface {
public:
CircuitCoveringPropagator(std::vector<std::vector<Literal>> graph,
const std::vector<int>& distinguished_nodes,
absl::Span<const int> distinguished_nodes,
Model* model);
void SetLevel(int level) final;
@@ -254,9 +255,9 @@ void LoadSubcircuitConstraint(int num_nodes, const std::vector<int>& tails,
// TODO(user): Change to a sparse API like for the function above.
std::function<void(Model*)> ExactlyOnePerRowAndPerColumn(
const std::vector<std::vector<Literal>>& graph);
absl::Span<const std::vector<Literal>> graph);
std::function<void(Model*)> CircuitCovering(
const std::vector<std::vector<Literal>>& graph,
absl::Span<const std::vector<Literal>> graph,
const std::vector<int>& distinguished_nodes);
} // namespace sat

9
ortools/sat/cp_constraints.h
View File

@@ -161,10 +161,13 @@ inline std::function<void(Model*)> GreaterThanAtLeastOneOf(
// Note(user): If there is just one or two candidates, this doesn't add
// anything.
inline std::function<void(Model*)> PartialIsOneOfVar(
IntegerVariable target_var, const std::vector<IntegerVariable>& vars,
const std::vector<Literal>& selectors) {
IntegerVariable target_var, absl::Span<const IntegerVariable> vars,
absl::Span<const Literal> selectors) {
CHECK_EQ(vars.size(), selectors.size());
return [=](Model* model) {
return [=,
selectors = std::vector<Literal>(selectors.begin(), selectors.end()),
vars = std::vector<IntegerVariable>(vars.begin(), vars.end())](
Model* model) {
const std::vector<IntegerValue> offsets(vars.size(), IntegerValue(0));
if (vars.size() > 2) {
// Propagate the min.

6
ortools/sat/cp_model_expand.cc
View File

@@ -1351,8 +1351,8 @@ void ExpandNegativeTable(ConstraintProto* ct, PresolveContext* context) {
// We list for each tuple the possible values the variable can take.
// If the list is empty, then this encode "any value".
void ProcessOneCompressedColumn(
int variable, const std::vector<int>& tuple_literals,
const std::vector<absl::InlinedVector<int64_t, 2>>& values,
int variable, absl::Span<const int> tuple_literals,
absl::Span<const absl::InlinedVector<int64_t, 2>> values,
std::optional<int> table_is_active_literal, PresolveContext* context) {
DCHECK_EQ(tuple_literals.size(), values.size());
@@ -1656,7 +1656,7 @@ bool ReduceTableInPresenceOfUniqueVariableWithCosts(
// is called. Some checks will fail otherwise.
void CompressAndExpandPositiveTable(ConstraintProto* ct,
bool last_column_is_cost,
const std::vector<int>& vars,
absl::Span<const int> vars,
std::vector<std::vector<int64_t>>* tuples,
PresolveContext* context) {
const int num_tuples_before_compression = tuples->size();

104
ortools/sat/cp_model_lns.cc
View File

@@ -825,7 +825,7 @@ struct IndexedRectangle {
};
void InsertRectanglePredecences(
const std::vector<IndexedRectangle>& rectangles,
absl::Span<const IndexedRectangle> rectangles,
absl::flat_hash_set<std::pair<int, int>>* precedences) {
// TODO(user): Refine set of interesting points.
std::vector<IntegerValue> interesting_points;
@@ -1148,7 +1148,7 @@ void NeighborhoodGeneratorHelper::AddSolutionHinting(
Neighborhood NeighborhoodGeneratorHelper::RelaxGivenVariables(
const CpSolverResponse& initial_solution,
const std::vector<int>& relaxed_variables) const {
absl::Span<const int> relaxed_variables) const {
std::vector<bool> relaxed_variables_set(model_proto_.variables_size(), false);
for (const int var : relaxed_variables) relaxed_variables_set[var] = true;
absl::flat_hash_set<int> fixed_variables;
@@ -1737,8 +1737,8 @@ namespace {
// Create a constraint sum (X - LB) + sum (UB - X) <= rhs.
ConstraintProto DistanceToBoundsSmallerThanConstraint(
const std::vector<std::pair<int, int64_t>>& dist_to_lower_bound,
const std::vector<std::pair<int, int64_t>>& dist_to_upper_bound,
absl::Span<const std::pair<int, int64_t>> dist_to_lower_bound,
absl::Span<const std::pair<int, int64_t>> dist_to_upper_bound,
const int64_t rhs) {
DCHECK_GE(rhs, 0);
ConstraintProto new_constraint;
@@ -2290,6 +2290,84 @@ Neighborhood RandomRectanglesPackingNeighborhoodGenerator::Generate(
return helper_.FixGivenVariables(initial_solution, variables_to_freeze);
}
Neighborhood RectanglesPackingRelaxOneNeighborhoodGenerator::Generate(
const CpSolverResponse& initial_solution, SolveData& data,
absl::BitGenRef random) {
// First pick one rectangle.
const std::vector<ActiveRectangle> all_active_rectangles =
helper_.GetActiveRectangles(initial_solution);
if (all_active_rectangles.size() <= 1) return helper_.FullNeighborhood();
const ActiveRectangle& base_rectangle =
all_active_rectangles[absl::Uniform<int>(random, 0,
all_active_rectangles.size())];
const auto get_rectangle = [&initial_solution, helper = &helper_](
const ActiveRectangle& rectangle) {
const int x_interval_idx = rectangle.x_interval;
const int y_interval_idx = rectangle.y_interval;
const ConstraintProto& x_interval_ct =
helper->ModelProto().constraints(x_interval_idx);
const ConstraintProto& y_interval_ct =
helper->ModelProto().constraints(y_interval_idx);
return Rectangle{.x_min = GetLinearExpressionValue(
x_interval_ct.interval().start(), initial_solution),
.x_max = GetLinearExpressionValue(
x_interval_ct.interval().end(), initial_solution),
.y_min = GetLinearExpressionValue(
y_interval_ct.interval().start(), initial_solution),
.y_max = GetLinearExpressionValue(
y_interval_ct.interval().end(), initial_solution)};
};
const Rectangle center_rect = get_rectangle(base_rectangle);
// Now compute a neighborhood around that rectangle. In this neighborhood
// we prefer a "Square" region around the initial rectangle center rather than
// a circle.
//
// Note that we only consider two rectangles as potential neighbors if they
// are part of the same no_overlap_2d constraint.
absl::flat_hash_set<int> variables_to_freeze;
std::vector<std::pair<int, double>> distances;
distances.reserve(all_active_rectangles.size());
for (int i = 0; i < all_active_rectangles.size(); ++i) {
const ActiveRectangle& rectangle = all_active_rectangles[i];
InsertVariablesFromConstraint(helper_.ModelProto(), rectangle.x_interval,
variables_to_freeze);
InsertVariablesFromConstraint(helper_.ModelProto(), rectangle.y_interval,
variables_to_freeze);
const Rectangle rect = get_rectangle(rectangle);
const bool same_no_overlap_as_center_rect = absl::c_any_of(
base_rectangle.no_overlap_2d_constraints, [&rectangle](const int c) {
return rectangle.no_overlap_2d_constraints.contains(c);
});
if (same_no_overlap_as_center_rect) {
distances.push_back(
{i, CenterToCenterLInfinityDistance(center_rect, rect)});
}
}
std::sort(distances.begin(), distances.end(),
[](const auto& a, const auto& b) { return a.second < b.second; });
const int num_to_sample = data.difficulty * all_active_rectangles.size();
absl::flat_hash_set<int> variables_to_relax;
const int num_to_relax = std::min<int>(distances.size(), num_to_sample);
for (int i = 0; i < num_to_relax; ++i) {
const int rectangle_idx = distances[i].first;
const ActiveRectangle& rectangle = all_active_rectangles[rectangle_idx];
InsertVariablesFromConstraint(helper_.ModelProto(), rectangle.x_interval,
variables_to_relax);
InsertVariablesFromConstraint(helper_.ModelProto(), rectangle.y_interval,
variables_to_relax);
}
for (const int v : variables_to_relax) {
variables_to_freeze.erase(v);
}
return helper_.FixGivenVariables(initial_solution, variables_to_freeze);
}
Neighborhood RectanglesPackingRelaxTwoNeighborhoodsGenerator::Generate(
const CpSolverResponse& initial_solution, SolveData& data,
absl::BitGenRef random) {
@@ -2327,22 +2405,16 @@ Neighborhood RectanglesPackingRelaxTwoNeighborhoodsGenerator::Generate(
y_interval_ct.interval().end(), initial_solution)};
};
// TODO(user): This computes the distance between the center of the
// rectangles. We could use the real distance between the closest points, but
// not sure it is worth the extra complexity.
const auto compute_rectangle_distance = [](const Rectangle& rect1,
const Rectangle& rect2) {
return (static_cast<double>(rect1.x_min.value()) + rect1.x_max.value() -
rect2.x_min.value() - rect2.x_max.value()) *
(static_cast<double>(rect1.y_min.value()) + rect1.y_max.value() -
rect2.y_min.value() - rect2.y_max.value());
};
const Rectangle rect1 = get_rectangle(chosen_rectangle_1);
const Rectangle rect2 = get_rectangle(chosen_rectangle_2);
// Now compute a neighborhood around each rectangle. Note that we only
// consider two rectangles as potential neighbors if they are part of the same
// no_overlap_2d constraint.
//
// TODO(user): This computes the distance between the center of the
// rectangles. We could use the real distance between the closest points, but
// not sure it is worth the extra complexity.
absl::flat_hash_set<int> variables_to_freeze;
std::vector<std::pair<int, double>> distances1;
std::vector<std::pair<int, double>> distances2;
@@ -2367,10 +2439,10 @@ Neighborhood RectanglesPackingRelaxTwoNeighborhoodsGenerator::Generate(
return rectangle.no_overlap_2d_constraints.contains(c);
});
if (same_no_overlap_as_rect1) {
distances1.push_back({i, compute_rectangle_distance(rect1, rect)});
distances1.push_back({i, CenterToCenterL2Distance(rect1, rect)});
}
if (same_no_overlap_as_rect2) {
distances2.push_back({i, compute_rectangle_distance(rect2, rect)});
distances2.push_back({i, CenterToCenterL2Distance(rect2, rect)});
}
}
const int num_to_sample_each =

21
ortools/sat/cp_model_lns.h
View File

@@ -116,7 +116,7 @@ class NeighborhoodGeneratorHelper : public SubSolver {
// variables in relaxed_variables.
Neighborhood RelaxGivenVariables(
const CpSolverResponse& initial_solution,
const std::vector<int>& relaxed_variables) const;
absl::Span<const int> relaxed_variables) const;
// Returns a trivial model by fixing all active variables to the initial
// solution values.
@@ -361,7 +361,11 @@ class NeighborhoodGenerator {
public:
NeighborhoodGenerator(absl::string_view name,
NeighborhoodGeneratorHelper const* helper)
: name_(name), helper_(*helper), difficulty_(0.5) {}
: name_(name),
helper_(*helper),
deterministic_limit_(
helper->Parameters().lns_initial_deterministic_limit()),
difficulty_(helper->Parameters().lns_initial_difficulty()) {}
virtual ~NeighborhoodGenerator() = default;
using ActiveRectangle = NeighborhoodGeneratorHelper::ActiveRectangle;
@@ -721,6 +725,19 @@ class RandomRectanglesPackingNeighborhoodGenerator
SolveData& data, absl::BitGenRef random) final;
};
// Only make sense for problems with no_overlap_2d constraints. This selects one
// random rectangles and relax the closest rectangles to it.
class RectanglesPackingRelaxOneNeighborhoodGenerator
: public NeighborhoodGenerator {
public:
explicit RectanglesPackingRelaxOneNeighborhoodGenerator(
NeighborhoodGeneratorHelper const* helper, absl::string_view name)
: NeighborhoodGenerator(name, helper) {}
Neighborhood Generate(const CpSolverResponse& initial_solution,
SolveData& data, absl::BitGenRef random) final;
};
// Only make sense for problems with no_overlap_2d constraints. This selects two
// random rectangles and relax them alongside the closest rectangles to each one
// of them. The idea is that this will find a better solution when there is a

5
ortools/sat/cp_model_postsolve.cc
View File

@@ -19,6 +19,7 @@
#include <vector>
#include "absl/log/check.h"
#include "absl/types/span.h"
#include "ortools/base/logging.h"
#include "ortools/port/proto_utils.h"
#include "ortools/sat/cp_model.pb.h"
@@ -226,7 +227,7 @@ int64_t EvaluateLinearExpression(const LinearExpressionProto& expr,
}
bool LinearExpressionIsFixed(const LinearExpressionProto& expr,
const std::vector<Domain>& domains) {
absl::Span<const Domain> domains) {
for (const int var : expr.vars()) {
if (!domains[var].IsFixed()) return false;
}
@@ -335,7 +336,7 @@ void PostsolveIntProd(const ConstraintProto& ct, std::vector<Domain>* domains) {
void PostsolveResponse(const int64_t num_variables_in_original_model,
const CpModelProto& mapping_proto,
const std::vector<int>& postsolve_mapping,
absl::Span<const int> postsolve_mapping,
std::vector<int64_t>* solution) {
CHECK_EQ(solution->size(), postsolve_mapping.size());

3
ortools/sat/cp_model_postsolve.h
View File

@@ -17,6 +17,7 @@
#include <cstdint>
#include <vector>
#include "absl/types/span.h"
#include "ortools/base/types.h"
#include "ortools/sat/cp_model.pb.h"
#include "ortools/util/logging.h"
@@ -45,7 +46,7 @@ namespace sat {
// chosen values? The feature might never be needed though.
void PostsolveResponse(int64_t num_variables_in_original_model,
const CpModelProto& mapping_proto,
const std::vector<int>& postsolve_mapping,
absl::Span<const int> postsolve_mapping,
std::vector<int64_t>* solution);
// Try to postsolve with a "best-effort" the reduced domain from the presolved

119
ortools/sat/cp_model_presolve.cc
View File

@@ -7031,6 +7031,7 @@ void CpModelPresolver::RunPropagatorsForConstraint(const ConstraintProto& ct) {
local_params.set_use_conservative_scale_overload_checker(true);
local_params.set_use_dual_scheduling_heuristics(true);
model.GetOrCreate<TimeLimit>()->MergeWithGlobalTimeLimit(time_limit_);
std::vector<int> variable_mapping;
CreateValidModelWithSingleConstraint(ct, context_, &variable_mapping,
&tmp_model_);
@@ -7813,6 +7814,73 @@ void CpModelPresolver::ShiftObjectiveWithExactlyOnes() {
}
}
bool CpModelPresolver::PropagateObjective() {
if (!context_->working_model->has_objective()) return true;
if (context_->ModelIsUnsat()) return false;
context_->WriteObjectiveToProto();
int64_t min_activity = 0;
int64_t max_variation = 0;
const CpObjectiveProto& objective = context_->working_model->objective();
const int num_terms = objective.vars().size();
for (int i = 0; i < num_terms; ++i) {
const int var = objective.vars(i);
const int64_t coeff = objective.coeffs(i);
CHECK(RefIsPositive(var));
CHECK_NE(coeff, 0);
const int64_t domain_min = context_->MinOf(var);
const int64_t domain_max = context_->MaxOf(var);
if (coeff > 0) {
min_activity += coeff * domain_min;
} else {
min_activity += coeff * domain_max;
}
const int64_t variation = std::abs(coeff) * (domain_max - domain_min);
max_variation = std::max(max_variation, variation);
}
// Infeasible ?
const int64_t slack =
CapSub(ReadDomainFromProto(objective).Max(), min_activity);
if (slack < 0) {
return context_->NotifyThatModelIsUnsat(
"infeasible while propagating objective");
}
// No propagation ?
if (max_variation <= slack) return true;
int num_propagations = 0;
for (int i = 0; i < num_terms; ++i) {
const int var = objective.vars(i);
const int64_t coeff = objective.coeffs(i);
const int64_t domain_min = context_->MinOf(var);
const int64_t domain_max = context_->MaxOf(var);
const int64_t new_diff = slack / std::abs(coeff);
if (new_diff >= domain_max - domain_min) continue;
++num_propagations;
if (coeff > 0) {
if (!context_->IntersectDomainWith(
var, Domain(domain_min, domain_min + new_diff))) {
return false;
}
} else {
if (!context_->IntersectDomainWith(
var, Domain(domain_max - new_diff, domain_max))) {
return false;
}
}
}
CHECK_GT(num_propagations, 0);
context_->UpdateRuleStats("objective: restricted var domains by propagation",
num_propagations);
return true;
}
// Expand the objective expression in some easy cases.
//
// The ideas is to look at all the "tight" equality constraints. These should
@@ -12895,25 +12963,43 @@ bool ModelCopy::CopyAllDiff(const ConstraintProto& ct) {
}
bool ModelCopy::CopyLinMax(const ConstraintProto& ct) {
ConstraintProto* new_ct = context_->working_model->add_constraints();
// We will create it lazily if we end up copying something.
ConstraintProto* new_ct = nullptr;
// Regroup all constant terms and copy the other.
int64_t max_of_fixed_terms = std::numeric_limits<int64_t>::min();
for (const auto& expr : ct.lin_max().exprs()) {
CopyLinearExpression(expr, new_ct->mutable_lin_max()->add_exprs());
auto& last_expr = *new_ct->mutable_lin_max()->mutable_exprs(
new_ct->lin_max().exprs_size() - 1);
if (last_expr.vars().empty() && new_ct->lin_max().exprs().size() > 1) {
LinearExpressionProto* first_expr =
new_ct->mutable_lin_max()->mutable_exprs(0);
if (first_expr->vars().empty()) {
// We have two constants, keep the largest.
first_expr->set_offset(
std::max(first_expr->offset(), last_expr.offset()));
new_ct->mutable_lin_max()->mutable_exprs()->RemoveLast();
} else {
// Put the constant in the first position.
last_expr.Swap(first_expr);
if (context_->IsFixed(expr)) {
max_of_fixed_terms =
std::max(max_of_fixed_terms, context_->FixedValue(expr));
} else {
// copy.
if (new_ct == nullptr) {
new_ct = context_->working_model->add_constraints();
}
CopyLinearExpression(expr, new_ct->mutable_lin_max()->add_exprs());
}
}
// If we have no non-fixed expression, we can just fix the target when it
// involve at most one variable.
if (new_ct == nullptr && ct.enforcement_literal().empty() &&
ct.lin_max().target().vars().size() <= 1) {
context_->UpdateRuleStats("lin_max: all exprs fixed during copy");
return context_->IntersectDomainWith(ct.lin_max().target(),
Domain(max_of_fixed_terms));
}
// Otherwise, add a constant term if needed.
if (max_of_fixed_terms > std::numeric_limits<int64_t>::min()) {
if (new_ct == nullptr) {
new_ct = context_->working_model->add_constraints();
}
new_ct->mutable_lin_max()->add_exprs()->set_offset(max_of_fixed_terms);
}
// Finish by copying the target.
if (new_ct == nullptr) return false; // No expr == unsat.
CopyLinearExpression(ct.lin_max().target(),
new_ct->mutable_lin_max()->mutable_target());
return true;
@@ -13576,6 +13662,9 @@ CpSolverStatus CpModelPresolver::Presolve() {
context_->UpdateRuleStats("presolve: iteration");
const int64_t old_num_presolve_op = context_->num_presolve_operations;
// Propagate the objective.
if (!PropagateObjective()) return InfeasibleStatus();
// 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

4
ortools/sat/cp_model_presolve.h
View File

@@ -254,6 +254,10 @@ class CpModelPresolver {
// Converts bool_or and at_most_one of size 2 to bool_and.
void ConvertToBoolAnd();
// Sometimes an upper bound on the objective can reduce the domains of many
// variables. This "propagates" the objective like a normal linear constraint.
bool PropagateObjective();
// Try to reformulate the objective in term of "base" variables. This is
// mainly useful for core based approach where having more terms in the
// objective (but with a same trivial lower bound) should help.

65
ortools/sat/cp_model_solver.cc
View File

@@ -759,6 +759,53 @@ bool VarIsFixed(const CpModelProto& model_proto, int i) {
model_proto.variables(i).domain(1);
}
// Note that we restrict the objective to be <= so that the hint is still
// feasible. Alternatively, we could look for < hint value if we only want
// better solution.
void RestrictObjectiveUsingHint(CpModelProto* model_proto) {
if (!model_proto->has_objective()) return;
if (!model_proto->has_solution_hint()) return;
// We will abort if the hint is not complete, ignoring fixed variables.
const int num_vars = model_proto->variables().size();
int num_filled = 0;
std::vector<bool> filled(num_vars, false);
std::vector<int64_t> solution(num_vars, 0);
for (int var = 0; var < num_vars; ++var) {
if (VarIsFixed(*model_proto, var)) {
solution[var] = model_proto->variables(var).domain(0);
filled[var] = true;
++num_filled;
}
}
const auto& hint_proto = model_proto->solution_hint();
const int num_hinted = hint_proto.vars().size();
for (int i = 0; i < num_hinted; ++i) {
const int var = hint_proto.vars(i);
CHECK(RefIsPositive(var));
if (filled[var]) continue;
const int64_t value = hint_proto.values(i);
solution[var] = value;
filled[var] = true;
++num_filled;
}
if (num_filled != num_vars) return;
const int64_t obj_upper_bound =
ComputeInnerObjective(model_proto->objective(), solution);
const Domain restriction =
Domain(std::numeric_limits<int64_t>::min(), obj_upper_bound);
if (model_proto->objective().domain().empty()) {
FillDomainInProto(restriction, model_proto->mutable_objective());
} else {
FillDomainInProto(ReadDomainFromProto(model_proto->objective())
.IntersectionWith(restriction),
model_proto->mutable_objective());
}
}
// Returns false if there is a complete solution hint that is infeasible, or
// true otherwise.
bool TestSolutionHintForFeasibility(const CpModelProto& model_proto,
@@ -1347,6 +1394,12 @@ class LnsSolver : public SubSolver {
TestSolutionHintForFeasibility(lns_fragment, /*logger=*/nullptr);
}
// If we use a hint, we will restrict the objective to be <= to the one
// of the hint. This is helpful on some model where doing so can cause
// the presolve to restrict the domain of many variables. Note that the
// hint will still be feasible as we use <= and not <.
RestrictObjectiveUsingHint(&lns_fragment);
CpModelProto debug_copy;
if (absl::GetFlag(FLAGS_cp_model_dump_problematic_lns)) {
// We need to make a copy because the presolve is destructive.
@@ -1777,12 +1830,18 @@ void SolveCpModelParallel(SharedClasses* shared, Model* global_model) {
const bool has_no_overlap2d =
!helper->TypeToConstraints(ConstraintProto::kNoOverlap2D).empty();
if (has_no_overlap2d) {
if (name_filter.Keep("packing_rectangles_lns")) {
if (name_filter.Keep("packing_random_lns")) {
reentrant_interleaved_subsolvers.push_back(std::make_unique<LnsSolver>(
std::make_unique<RandomRectanglesPackingNeighborhoodGenerator>(
helper, name_filter.LastName()),
lns_params, helper, shared));
}
if (name_filter.Keep("packing_square_lns")) {
reentrant_interleaved_subsolvers.push_back(std::make_unique<LnsSolver>(
std::make_unique<RectanglesPackingRelaxOneNeighborhoodGenerator>(
helper, name_filter.LastName()),
lns_params, helper, shared));
}
if (name_filter.Keep("packing_swap_lns")) {
reentrant_interleaved_subsolvers.push_back(std::make_unique<LnsSolver>(
std::make_unique<RectanglesPackingRelaxTwoNeighborhoodsGenerator>(
@@ -2012,8 +2071,8 @@ void SolveCpModelParallel(SharedClasses* shared, Model* global_model) {
// If the option use_sat_inprocessing is true, then before post-solving a
// solution, we need to make sure we add any new clause required for postsolving
// to the mapping_model.
void AddPostsolveClauses(const std::vector<int>& postsolve_mapping,
Model* model, CpModelProto* mapping_proto) {
void AddPostsolveClauses(absl::Span<const int> postsolve_mapping, Model* model,
CpModelProto* mapping_proto) {
auto* mapping = model->GetOrCreate<CpModelMapping>();
auto* postsolve = model->GetOrCreate<PostsolveClauses>();
for (const auto& clause : postsolve->clauses) {

22
ortools/sat/diffn_util.h
View File

@@ -120,6 +120,28 @@ inline IntegerValue Rectangle::IntersectArea(const Rectangle& other) const {
}
}
// Returns the L2 distance between the centers of the two rectangles.
inline double CenterToCenterL2Distance(const Rectangle& a, const Rectangle& b) {
const double diff_x =
(static_cast<double>(a.x_min.value()) + a.x_max.value()) / 2.0 -
(static_cast<double>(b.x_min.value()) + b.x_max.value()) / 2.0;
const double diff_y =
(static_cast<double>(a.y_min.value()) + a.y_max.value()) / 2.0 -
(static_cast<double>(b.y_min.value()) + b.y_max.value()) / 2.0;
return std::sqrt(diff_x * diff_x + diff_y * diff_y);
}
inline double CenterToCenterLInfinityDistance(const Rectangle& a,
const Rectangle& b) {
const double diff_x =
(static_cast<double>(a.x_min.value()) + a.x_max.value()) / 2.0 -
(static_cast<double>(b.x_min.value()) + b.x_max.value()) / 2.0;
const double diff_y =
(static_cast<double>(a.y_min.value()) + a.y_max.value()) / 2.0 -
(static_cast<double>(b.y_min.value()) + b.y_max.value()) / 2.0;
return std::max(std::abs(diff_x), std::abs(diff_y));
}
// Creates a graph when two nodes are connected iff their rectangles overlap.
// Then partition into connected components.
//

18
ortools/sat/diffn_util_test.cc
View File

@@ -50,6 +50,24 @@ using ::testing::ElementsAreArray;
using ::testing::UnorderedElementsAre;
using ::testing::UnorderedElementsAreArray;
TEST(CenterToCenterDistanceTest, BasicTest) {
Rectangle a, b;
a.x_min = 0;
a.x_max = 2;
a.y_min = 0;
a.y_max = 2;
b.x_min = 0;
b.x_max = 10;
b.y_min = 0;
b.y_max = 10;
// This is just the distance between (1,1) and (5,5) which should be sqrt(32).
EXPECT_EQ(CenterToCenterL2Distance(a, b), std::sqrt(32));
// Now this is 4.
EXPECT_EQ(CenterToCenterLInfinityDistance(a, b), 4.0);
}
TEST(GetOverlappingRectangleComponentsTest, NoComponents) {
EXPECT_TRUE(GetOverlappingRectangleComponents({}, {}).empty());
IntegerValue zero(0);

602
ortools/sat/fuzz_testdata/MultipleCumulativesA
View File

@@ -1,608 +1,326 @@
# proto-file: ortools/sat/cp_model.proto
# proto-message: operations_research.sat.CpModelProto
variables {
domain: 0
domain: 1024
}
variables {
domain: 0
domain: 3
}
variables {
domain: 0
domain: 3
}
variables {
domain: 1
domain: 4
}
variables {
domain: 0
domain: 3
}
variables {
domain: 0
domain: 3
}
variables {
domain: 1
domain: 4
}
variables {
domain: 0
domain: 3
}
variables {
domain: 0
domain: 3
}
variables {
domain: 1
domain: 4
}
variables {
domain: 0
domain: 4
}
variables {
domain: 0
domain: 4
}
variables {
domain: 0
domain: 4
}
variables {
domain: 0
domain: 4
}
variables {
domain: 0
domain: 4
}
variables {
domain: 0
domain: 4
}
variables {
domain: 0
domain: 1
}
variables {
domain: 0
domain: 1
}
variables {
domain: 0
domain: 512
}
variables {
domain: 0
domain: 512
}
variables {
domain: 0
domain: 2048
}
variables {
domain: 0
domain: 512
}
variables {
domain: 0
domain: 1
}
variables {
domain: 0
domain: 1
}
variables {
domain: 0
domain: 1
}
variables { domain: [0, 1024] }
variables { domain: [0, 3] }
variables { domain: [0, 3] }
variables { domain: [1, 4] }
variables { domain: [0, 3] }
variables { domain: [0, 3] }
variables { domain: [1, 4] }
variables { domain: [0, 3] }
variables { domain: [0, 3] }
variables { domain: [1, 4] }
variables { domain: [0, 4] }
variables { domain: [0, 4] }
variables { domain: [0, 4] }
variables { domain: [0, 4] }
variables { domain: [0, 4] }
variables { domain: [0, 4] }
variables { domain: [0, 1] }
variables { domain: [0, 1] }
variables { domain: [0, 512] }
variables { domain: [0, 512] }
variables { domain: [0, 2048] }
variables { domain: [0, 512] }
variables { domain: [0, 1] }
variables { domain: [0, 1] }
variables { domain: [0, 1] }
constraints {
linear {
vars: 2
vars: 1
coeffs: 1
coeffs: -1
domain: -9223372036854775808
domain: 0
vars: [2, 1]
coeffs: [1, -1]
domain: [-9223372036854775808, 0]
}
}
constraints {
linear {
vars: 3
vars: 1
coeffs: 1
coeffs: -1
domain: 1
domain: 9223372036854775807
vars: [3, 1]
coeffs: [1, -1]
domain: [1, 9223372036854775807]
}
}
constraints {
linear {
vars: 5
vars: 4
coeffs: 1
coeffs: -1
domain: -9223372036854775808
domain: 0
vars: [5, 4]
coeffs: [1, -1]
domain: [-9223372036854775808, 0]
}
}
constraints {
linear {
vars: 6
vars: 4
coeffs: 1
coeffs: -1
domain: 1
domain: 9223372036854775807
vars: [6, 4]
coeffs: [1, -1]
domain: [1, 9223372036854775807]
}
}
constraints {
linear {
vars: 8
vars: 7
coeffs: 1
coeffs: -1
domain: -9223372036854775808
domain: 0
vars: [8, 7]
coeffs: [1, -1]
domain: [-9223372036854775808, 0]
}
}
constraints {
linear {
vars: 9
vars: 7
coeffs: 1
coeffs: -1
domain: 1
domain: 9223372036854775807
vars: [9, 7]
coeffs: [1, -1]
domain: [1, 9223372036854775807]
}
}
constraints {
linear {
vars: 3
vars: 1
vars: 10
coeffs: -1
coeffs: 1
coeffs: 1
domain: -1
domain: -1
vars: [3, 1, 10]
coeffs: [-1, 1, 1]
domain: [-1, -1]
}
}
constraints {
interval {
start {
vars: 1
coeffs: 1
offset: 1
}
end {
vars: 3
coeffs: 1
}
size {
vars: 10
coeffs: 1
}
start { vars: [1] coeffs: [1] offset: 1 }
end { vars: [3] coeffs: [1] }
size { vars: [10] coeffs: [1] }
}
}
constraints {
linear {
vars: 1
vars: 2
vars: 11
coeffs: -1
coeffs: 1
coeffs: 1
domain: 0
domain: 0
vars: [1, 2, 11]
coeffs: [-1, 1, 1]
domain: [0, 0]
}
}
constraints {
interval {
start {
vars: 2
coeffs: 1
}
end {
vars: 1
coeffs: 1
}
size {
vars: 11
coeffs: 1
}
start { vars: [2] coeffs: [1] }
end { vars: [1] coeffs: [1] }
size { vars: [11] coeffs: [1] }
}
}
constraints {
linear {
vars: 6
vars: 4
vars: 12
coeffs: -1
coeffs: 1
coeffs: 1
domain: -1
domain: -1
vars: [6, 4, 12]
coeffs: [-1, 1, 1]
domain: [-1, -1]
}
}
constraints {
interval {
start {
vars: 4
coeffs: 1
offset: 1
}
end {
vars: 6
coeffs: 1
}
size {
vars: 12
coeffs: 1
}
start { vars: [4] coeffs: [1] offset: 1 }
end { vars: [6] coeffs: [1] }
size { vars: [12] coeffs: [1] }
}
}
constraints {
linear {
vars: 4
vars: 5
vars: 13
coeffs: -1
coeffs: 1
coeffs: 1
domain: 0
domain: 0
vars: [4, 5, 13]
coeffs: [-1, 1, 1]
domain: [0, 0]
}
}
constraints {
interval {
start {
vars: 5
coeffs: 1
}
end {
vars: 4
coeffs: 1
}
size {
vars: 13
coeffs: 1
}
start { vars: [5] coeffs: [1] }
end { vars: [4] coeffs: [1] }
size { vars: [13] coeffs: [1] }
}
}
constraints {
linear {
vars: 9
vars: 7
vars: 14
coeffs: -1
coeffs: 1
coeffs: 1
domain: -1
domain: -1
vars: [9, 7, 14]
coeffs: [-1, 1, 1]
domain: [-1, -1]
}
}
constraints {
interval {
start {
vars: 7
coeffs: 1
offset: 1
}
end {
vars: 9
coeffs: 1
}
size {
vars: 14
coeffs: 1
}
start { vars: [7] coeffs: [1] offset: 1 }
end { vars: [9] coeffs: [1] }
size { vars: [14] coeffs: [1] }
}
}
constraints {
linear {
vars: 7
vars: 8
vars: 15
coeffs: -1
coeffs: 1
coeffs: 1
domain: 0
domain: 0
vars: [7, 8, 15]
coeffs: [-1, 1, 1]
domain: [0, 0]
}
}
constraints {
interval {
start {
vars: 8
coeffs: 1
}
end {
vars: 7
coeffs: 1
}
size {
vars: 15
coeffs: 1
}
start { vars: [8] coeffs: [1] }
end { vars: [7] coeffs: [1] }
size { vars: [15] coeffs: [1] }
}
}
constraints {
linear {
vars: 5
vars: 1
coeffs: 1
coeffs: -1
domain: -9223372036854775808
domain: 0
vars: [5, 1]
coeffs: [1, -1]
domain: [-9223372036854775808, 0]
}
}
constraints {
linear {
vars: 6
vars: 1
coeffs: 1
coeffs: -1
domain: 1
domain: 9223372036854775807
vars: [6, 1]
coeffs: [1, -1]
domain: [1, 9223372036854775807]
}
}
constraints {
enforcement_literal: -17
enforcement_literal: [-17]
linear {
vars: 4
vars: 1
coeffs: 1
coeffs: -1
domain: 0
domain: 0
vars: [4, 1]
coeffs: [1, -1]
domain: [0, 0]
}
}
constraints {
enforcement_literal: 16
enforcement_literal: [16]
interval {
start {
vars: 1
coeffs: 1
}
end {
vars: 1
coeffs: 1
offset: 1
}
size {
offset: 1
}
start { vars: [1] coeffs: [1] }
end { vars: [1] coeffs: [1] offset: 1 }
size { offset: 1 }
}
}
constraints {
interval {
start {
vars: 4
coeffs: 1
}
end {
vars: 4
coeffs: 1
offset: 1
}
size {
offset: 1
}
start { vars: [4] coeffs: [1] }
end { vars: [4] coeffs: [1] offset: 1 }
size { offset: 1 }
}
}
constraints {
linear {
vars: 8
vars: 4
coeffs: 1
coeffs: -1
domain: -9223372036854775808
domain: 0
vars: [8, 4]
coeffs: [1, -1]
domain: [-9223372036854775808, 0]
}
}
constraints {
linear {
vars: 9
vars: 4
coeffs: 1
coeffs: -1
domain: 1
domain: 9223372036854775807
vars: [9, 4]
coeffs: [1, -1]
domain: [1, 9223372036854775807]
}
}
constraints {
enforcement_literal: -18
enforcement_literal: [-18]
linear {
vars: 7
vars: 4
coeffs: 1
coeffs: -1
domain: 0
domain: 0
vars: [7, 4]
coeffs: [1, -1]
domain: [0, 0]
}
}
constraints {
enforcement_literal: 17
enforcement_literal: [17]
interval {
start {
vars: 4
coeffs: 1
}
end {
vars: 4
coeffs: 1
offset: 1
}
size {
offset: 1
}
start { vars: [4] coeffs: [1] }
end { vars: [4] coeffs: [1] offset: 1 }
size { offset: 1 }
}
}
constraints {
linear {
vars: 7
coeffs: 1
domain: 0
domain: 0
vars: [7]
coeffs: [1]
domain: [0, 0]
}
}
constraints {
linear {
vars: 1
coeffs: 1
domain: 1
domain: 1
vars: [1]
coeffs: [1]
domain: [1, 1]
}
}
constraints {
linear {
vars: 18
vars: 0
coeffs: 2
coeffs: -1
domain: -9223372036854775808
domain: 0
vars: [18, 0]
coeffs: [2, -1]
domain: [-9223372036854775808, 0]
}
}
constraints {
cumulative {
capacity {
vars: 18
coeffs: 1
}
intervals: 7
intervals: 11
intervals: 15
demands {
offset: 1
}
demands {
offset: 1
}
demands {
offset: 2
}
capacity { vars: [18] coeffs: [1] }
intervals: [7, 11, 15]
demands { offset: 1 }
demands { offset: 1 }
demands { offset: 2 }
}
}
constraints {
linear {
vars: 19
vars: 0
coeffs: 2
coeffs: -1
domain: -9223372036854775808
domain: 0
vars: [19, 0]
coeffs: [2, -1]
domain: [-9223372036854775808, 0]
}
}
constraints {
cumulative {
capacity {
vars: 19
coeffs: 1
}
intervals: 9
intervals: 13
intervals: 17
demands {
offset: 1
}
demands {
offset: 1
}
demands {
offset: 2
}
capacity { vars: [19] coeffs: [1] }
intervals: [9, 13, 17]
demands { offset: 1 }
demands { offset: 1 }
demands { offset: 2 }
}
}
constraints {
linear {
vars: 20
vars: 0
coeffs: 1
coeffs: -2
domain: -9223372036854775808
domain: 0
vars: [20, 0]
coeffs: [1, -2]
domain: [-9223372036854775808, 0]
}
}
constraints {
cumulative {
capacity {
vars: 20
coeffs: 1
}
intervals: 21
intervals: 26
demands {
offset: 1
}
demands {
offset: 2
}
capacity { vars: [20] coeffs: [1] }
intervals: [21, 26]
demands { offset: 1 }
demands { offset: 2 }
}
}
constraints {
linear {
vars: 21
vars: 0
coeffs: 2
coeffs: -1
domain: -9223372036854775808
domain: 0
vars: [21, 0]
coeffs: [2, -1]
domain: [-9223372036854775808, 0]
}
}
constraints {
cumulative {
capacity {
vars: 21
coeffs: 1
}
intervals: 22
demands {
offset: 1
}
capacity { vars: [21] coeffs: [1] }
intervals: [22]
demands { offset: 1 }
}
}
constraints {
enforcement_literal: 22
enforcement_literal: [22]
linear {
vars: 2
vars: 3
coeffs: 1
coeffs: -1
domain: -1
domain: -1
vars: [2, 3]
coeffs: [1, -1]
domain: [-1, -1]
}
}
constraints {
enforcement_literal: 23
enforcement_literal: [23]
linear {
vars: 5
vars: 6
coeffs: 1
coeffs: -1
domain: -1
domain: -1
vars: [5, 6]
coeffs: [1, -1]
domain: [-1, -1]
}
}
constraints {
enforcement_literal: 24
enforcement_literal: [24]
linear {
vars: 8
vars: 9
coeffs: 1
coeffs: -1
domain: -1
domain: -1
vars: [8, 9]
coeffs: [1, -1]
domain: [-1, -1]
}
}
objective {
vars: 0
coeffs: 1
vars: [0]
coeffs: [1]
}

895
ortools/sat/fuzz_testdata/MultipleCumulativesB
View File

File diff suppressed because it is too large Load Diff

4
ortools/sat/parameters_validation.cc
View File

@@ -93,6 +93,10 @@ std::string ValidateParameters(const SatParameters& params) {
TEST_IS_FINITE(symmetry_detection_deterministic_time_limit);
TEST_IS_FINITE(variable_activity_decay);
TEST_IS_FINITE(lns_initial_difficulty);
TEST_IS_FINITE(lns_initial_deterministic_limit);
TEST_IN_RANGE(lns_initial_difficulty, 0.0, 1.0);
TEST_POSITIVE(at_most_one_max_expansion_size);
TEST_NOT_NAN(max_time_in_seconds);

6
ortools/sat/sat_parameters.proto
View File

@@ -23,7 +23,7 @@ option java_multiple_files = true;
// Contains the definitions for all the sat algorithm parameters and their
// default values.
//
// NEXT TAG: 307
// NEXT TAG: 309
message SatParameters {
// In some context, like in a portfolio of search, it makes sense to name a
// given parameters set for logging purpose.
@@ -1213,6 +1213,10 @@ message SatParameters {
// LNS parameters.
// Initial parameters for neighborhood generation.
optional double lns_initial_difficulty = 307 [default = 0.5];
optional double lns_initial_deterministic_limit = 308 [default = 0.1];
// Testing parameters used to disable all lns workers.
optional bool use_lns = 283 [default = true];

30
ortools/sat/var_domination.cc
View File

@@ -39,7 +39,7 @@
#include "ortools/base/strong_vector.h"
#include "ortools/sat/cp_model.pb.h"
#include "ortools/sat/cp_model_utils.h"
#include "ortools/sat/integer.h"
#include "ortools/sat/integer_base.h"
#include "ortools/sat/presolve_context.h"
#include "ortools/sat/presolve_util.h"
#include "ortools/sat/util.h"
@@ -850,8 +850,10 @@ bool DualBoundStrengthening::Strengthen(PresolveContext* context) {
context->deductions.ImpliedDomain(enf, positive_ref));
if (implied.IsEmpty()) {
context->UpdateRuleStats("dual: fix variable");
context->UpdateLiteralSolutionHint(enf, false);
if (!context->SetLiteralToFalse(enf)) return false;
if (!context->IntersectDomainWith(positive_ref, Domain(bound))) {
if (!context->IntersectDomainWithAndUpdateHint(positive_ref,
Domain(bound))) {
return false;
}
continue;
@@ -860,7 +862,8 @@ bool DualBoundStrengthening::Strengthen(PresolveContext* context) {
// Corner case.
if (implied.FixedValue() == bound) {
context->UpdateRuleStats("dual: fix variable");
if (!context->IntersectDomainWith(positive_ref, implied)) {
if (!context->IntersectDomainWithAndUpdateHint(positive_ref,
implied)) {
return false;
}
continue;
@@ -925,6 +928,7 @@ bool DualBoundStrengthening::Strengthen(PresolveContext* context) {
.IntersectionWith(var_domain);
if (rhs.IsEmpty()) {
context->UpdateRuleStats("linear1: infeasible");
context->UpdateLiteralSolutionHint(ct.enforcement_literal(0), false);
if (!context->SetLiteralToFalse(ct.enforcement_literal(0))) {
return false;
}
@@ -1866,8 +1870,9 @@ bool ExploitDominanceRelations(const VarDomination& var_domination,
// TODO(user): It look like testing this is not really necessary.
// The reduction done by this class seem to be order independent.
bool ok = true;
for (const IntegerVariable dom :
var_domination.DominatingVariables(var)) {
const absl::Span<const IntegerVariable> dominating_vars =
var_domination.DominatingVariables(var);
for (const IntegerVariable dom : dominating_vars) {
// Note that we assumed that a fixed point was reached before this
// is called, so modified_domains should have been empty as we
// entered this function. If not, the code is still correct, but we
@@ -1888,9 +1893,18 @@ bool ExploitDominanceRelations(const VarDomination& var_domination,
increase_is_forbidden[var] = true;
context->UpdateRuleStats(
"domination: dual strenghtening using dominance");
if (!context->IntersectDomainWithAndUpdateHint(
ref, Domain(context->MinOf(ref), lb))) {
return false;
const Domain reduced_domain = Domain(context->MinOf(ref), lb);
if (dominating_vars.empty()) {
if (!context->IntersectDomainWithAndUpdateHint(ref,
reduced_domain)) {
return false;
}
} else {
MaybeUpdateRefHintFromDominance(*context, ref, reduced_domain,
dominating_vars);
if (!context->IntersectDomainWith(ref, reduced_domain)) {
return false;
}
}
// The rest of the loop only care about Booleans.

2
ortools/sat/var_domination_test.cc
View File

@@ -17,7 +17,7 @@
#include "ortools/base/gmock.h"
#include "ortools/base/parse_test_proto.h"
#include "ortools/sat/cp_model.pb.h"
#include "ortools/sat/integer.h"
#include "ortools/sat/integer_base.h"
#include "ortools/sat/model.h"
#include "ortools/sat/presolve_context.h"
#include "ortools/util/sorted_interval_list.h"