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

[CP-SAT] lots of fuzzer bugs fixed

Browse Source
This commit is contained in:
Laurent Perron
2024-12-18 18:00:30 +01:00
parent 0cc3096448
commit 925af8aa71
20 changed files with 598 additions and 57 deletions
Download Patch File Download Diff File Expand all files Collapse all files

2
ortools/sat/2d_rectangle_presolve.cc
View File

@@ -31,7 +31,7 @@
#include "absl/types/span.h"
#include "ortools/base/logging.h"
#include "ortools/base/stl_util.h"
#include "ortools/graph/max_flow.h"
#include "ortools/graph/minimum_vertex_cover.h"
#include "ortools/graph/strongly_connected_components.h"
#include "ortools/sat/diffn_util.h"
#include "ortools/sat/integer_base.h"

29
ortools/sat/BUILD.bazel
View File

@@ -523,6 +523,7 @@ cc_library(
deps = [
":circuit",
":clause",
":combine_solutions",
":cp_model_cc_proto",
":cp_model_checker",
":cp_model_lns",
@@ -3009,7 +3010,7 @@ cc_library(
":diffn_util",
":integer_base",
"//ortools/base:stl_util",
"//ortools/graph:max_flow",
"//ortools/graph:minimum_vertex_cover",
"//ortools/graph:strongly_connected_components",
"@com_google_absl//absl/algorithm:container",
"@com_google_absl//absl/container:btree",
@@ -3699,6 +3700,32 @@ cc_library(
],
)
cc_library(
name = "combine_solutions",
srcs = ["combine_solutions.cc"],
hdrs = ["combine_solutions.h"],
deps = [
":cp_model_cc_proto",
":cp_model_checker",
":synchronization",
"@com_google_absl//absl/log:check",
"@com_google_absl//absl/strings",
"@com_google_absl//absl/types:span",
],
)
cc_test(
name = "combine_solutions_test",
srcs = ["combine_solutions_test.cc"],
deps = [
":combine_solutions",
":model",
":synchronization",
"//ortools/base:gmock_main",
"//ortools/base:parse_test_proto",
],
)
cc_library(
name = "work_assignment",
srcs = ["work_assignment.cc"],

79
ortools/sat/combine_solutions.cc Normal file
View File

@@ -0,0 +1,79 @@
// Copyright 2010-2024 Google LLC
// Licensed under the Apache License, Version 2.0 (the "License");
// you may not use this file except in compliance with the License.
// You may obtain a copy of the License at
//
// http://www.apache.org/licenses/LICENSE-2.0
//
// Unless required by applicable law or agreed to in writing, software
// distributed under the License is distributed on an "AS IS" BASIS,
// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
// See the License for the specific language governing permissions and
// limitations under the License.
#include "ortools/sat/combine_solutions.h"
#include <cstdint>
#include <memory>
#include <optional>
#include <string>
#include <string_view>
#include <vector>
#include "absl/log/check.h"
#include "absl/strings/str_cat.h"
#include "absl/types/span.h"
#include "ortools/sat/cp_model_checker.h"
#include "ortools/sat/synchronization.h"
namespace operations_research {
namespace sat {
bool TrySolution(const CpModelProto& model, absl::Span<const int64_t> solution,
absl::Span<const int64_t> new_solution,
absl::Span<const int64_t> base_solution,
std::vector<int64_t>* new_combined_solution) {
new_combined_solution->resize(new_solution.size());
for (int i = 0; i < new_solution.size(); ++i) {
if (new_solution[i] != base_solution[i]) {
// A value that changed that we patch.
(*new_combined_solution)[i] = new_solution[i];
} else {
(*new_combined_solution)[i] = solution[i];
}
}
return SolutionIsFeasible(model, *new_combined_solution);
}
std::optional<std::vector<int64_t>> FindCombinedSolution(
const CpModelProto& model, absl::Span<const int64_t> new_solution,
absl::Span<const int64_t> base_solution,
const SharedResponseManager* response_manager, std::string* solution_info) {
CHECK_EQ(new_solution.size(), base_solution.size());
const std::vector<
std::shared_ptr<const SharedSolutionRepository<int64_t>::Solution>>
solutions = response_manager->SolutionsRepository().GetBestNSolutions(10);
for (int sol_idx = 0; sol_idx < solutions.size(); ++sol_idx) {
std::shared_ptr<const SharedSolutionRepository<int64_t>::Solution> s =
solutions[sol_idx];
DCHECK_EQ(s->variable_values.size(), new_solution.size());
if (s->variable_values == new_solution ||
s->variable_values == base_solution) {
continue;
}
std::vector<int64_t> new_combined_solution;
if (TrySolution(model, s->variable_values, new_solution, base_solution,
&new_combined_solution)) {
absl::StrAppend(solution_info, " [combined with: ",
std::string_view(solutions[sol_idx]->info).substr(0, 20),
"...]");
return new_combined_solution;
}
}
return std::nullopt;
}
} // namespace sat
} // namespace operations_research

40
ortools/sat/combine_solutions.h Normal file
View File

@@ -0,0 +1,40 @@
// Copyright 2010-2024 Google LLC
// Licensed under the Apache License, Version 2.0 (the "License");
// you may not use this file except in compliance with the License.
// You may obtain a copy of the License at
//
// http://www.apache.org/licenses/LICENSE-2.0
//
// Unless required by applicable law or agreed to in writing, software
// distributed under the License is distributed on an "AS IS" BASIS,
// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
// See the License for the specific language governing permissions and
// limitations under the License.
#ifndef OR_TOOLS_SAT_COMBINE_SOLUTIONS_H_
#define OR_TOOLS_SAT_COMBINE_SOLUTIONS_H_
#include <cstdint>
#include <optional>
#include <string>
#include <vector>
#include "absl/types/span.h"
#include "ortools/sat/cp_model.pb.h"
#include "ortools/sat/synchronization.h"
namespace operations_research {
namespace sat {
// Given a `new_solution` that was created by changing a bit a `base_solution`,
// try to apply the same changes to the other solutions stored in the
// `response_manager` and return any such generated solution that is valid.
std::optional<std::vector<int64_t>> FindCombinedSolution(
const CpModelProto& model, absl::Span<const int64_t> new_solution,
absl::Span<const int64_t> base_solution,
const SharedResponseManager* response_manager, std::string* solution_info);
} // namespace sat
} // namespace operations_research
#endif // OR_TOOLS_SAT_COMBINE_SOLUTIONS_H_

61
ortools/sat/combine_solutions_test.cc Normal file
View File

@@ -0,0 +1,61 @@
// Copyright 2010-2024 Google LLC
// Licensed under the Apache License, Version 2.0 (the "License");
// you may not use this file except in compliance with the License.
// You may obtain a copy of the License at
//
// http://www.apache.org/licenses/LICENSE-2.0
//
// Unless required by applicable law or agreed to in writing, software
// distributed under the License is distributed on an "AS IS" BASIS,
// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
// See the License for the specific language governing permissions and
// limitations under the License.
#include "ortools/sat/combine_solutions.h"
#include <cstdint>
#include <string>
#include <vector>
#include "gtest/gtest.h"
#include "ortools/base/gmock.h"
#include "ortools/base/parse_test_proto.h"
#include "ortools/sat/model.h"
#include "ortools/sat/synchronization.h"
namespace operations_research {
namespace sat {
namespace {
using ::google::protobuf::contrib::parse_proto::ParseTestProto;
using ::testing::ElementsAre;
using ::testing::Optional;
TEST(CombineSolutionsTest, BasicTest) {
const CpModelProto model = ParseTestProto(R"pb(
variables { domain: [ 0, 1 ] }
variables { domain: [ 0, 1 ] }
variables { domain: [ 0, 1 ] }
variables { domain: [ 0, 1 ] }
objective {
vars: [ 0, 1, 2, 3 ]
coeffs: [ 1, 1, 1, 1 ]
}
)pb");
const std::vector<int64_t> existing_solution = {1, 0, 0, 0};
const std::vector<int64_t> base_solution = {0, 1, 0, 0};
const std::vector<int64_t> new_solution = {0, 1, 1, 0};
Model m;
SharedResponseManager response_manager(&m);
response_manager.NewSolution(existing_solution, "existing", nullptr);
response_manager.NewSolution(base_solution, "base", nullptr);
response_manager.NewSolution(new_solution, "new", nullptr);
std::string solution_info;
const auto combined_solution = FindCombinedSolution(
model, new_solution, base_solution, &response_manager, &solution_info);
EXPECT_THAT(combined_solution, Optional(ElementsAre(1, 0, 1, 0)));
}
} // namespace
} // namespace sat
} // namespace operations_research

69
ortools/sat/cp_model_checker.cc
View File

@@ -105,13 +105,13 @@ std::string ValidateIntegerVariable(const CpModelProto& model, int v) {
// Internally, we often take the negation of a domain, and we also want to
// have sentinel values greater than the min/max of a variable domain, so
// the domain must fall in [kint64min + 2, kint64max - 1].
// the domain must fall in [-kint64max / 2, kint64max / 2].
const int64_t lb = proto.domain(0);
const int64_t ub = proto.domain(proto.domain_size() - 1);
if (lb < std::numeric_limits<int64_t>::min() + 2 ||
ub > std::numeric_limits<int64_t>::max() - 1) {
if (lb < -std::numeric_limits<int64_t>::max() / 2 ||
ub > std::numeric_limits<int64_t>::max() / 2) {
return absl::StrCat(
"var #", v, " domain do not fall in [kint64min + 2, kint64max - 1]. ",
"var #", v, " domain do not fall in [-kint64max / 2, kint64max / 2]. ",
ProtobufShortDebugString(proto));
}
@@ -361,8 +361,14 @@ std::string ValidateIntProdConstraint(const CpModelProto& model,
// Detect potential overflow.
Domain product_domain(1);
for (const LinearExpressionProto& expr : ct.int_prod().exprs()) {
product_domain = product_domain.ContinuousMultiplicationBy(
{MinOfExpression(model, expr), MaxOfExpression(model, expr)});
const int64_t min_expr = MinOfExpression(model, expr);
const int64_t max_expr = MaxOfExpression(model, expr);
if (min_expr == 0 && max_expr == 0) {
// An overflow multiplied by zero is still invalid.
continue;
}
product_domain =
product_domain.ContinuousMultiplicationBy({min_expr, max_expr});
}
if (product_domain.Max() <= -std ::numeric_limits<int64_t>::max() ||
@@ -918,11 +924,6 @@ std::string ValidateSearchStrategies(const CpModelProto& model) {
" has a domain too large to be used in a"
" SELECT_MEDIAN_VALUE value selection strategy");
}
if (PossibleIntegerOverflow(model, {ref}, {1})) {
// This will become an overflow if translated to an expr.
return absl::StrCat("Possible integer overflow in strategy: ",
ProtobufShortDebugString(strategy));
}
}
for (const LinearExpressionProto& expr : strategy.exprs()) {
for (const int var : expr.vars()) {
@@ -1025,9 +1026,6 @@ bool PossibleIntegerOverflow(const CpModelProto& model,
}
std::string ValidateCpModel(const CpModelProto& model, bool after_presolve) {
if (!after_presolve && model.has_symmetry()) {
return "The symmetry field should be empty and reserved for internal use.";
}
int64_t int128_overflow = 0;
for (int v = 0; v < model.variables_size(); ++v) {
RETURN_IF_NOT_EMPTY(ValidateIntegerVariable(model, v));
@@ -1637,18 +1635,43 @@ class ConstraintChecker {
const int num_arcs = ct.routes().tails_size();
int num_used_arcs = 0;
int num_self_arcs = 0;
// Compute the number of nodes.
int num_nodes = 0;
std::vector<int> tail_to_head;
for (int i = 0; i < num_arcs; ++i) {
num_nodes = std::max(num_nodes, 1 + ct.routes().tails(i));
num_nodes = std::max(num_nodes, 1 + ct.routes().heads(i));
}
std::vector<int> tail_to_head(num_nodes, -1);
std::vector<bool> has_incoming_arc(num_nodes, false);
std::vector<int> has_outgoing_arc(num_nodes, false);
std::vector<int> depot_nexts;
for (int i = 0; i < num_arcs; ++i) {
const int tail = ct.routes().tails(i);
const int head = ct.routes().heads(i);
num_nodes = std::max(num_nodes, 1 + tail);
num_nodes = std::max(num_nodes, 1 + head);
tail_to_head.resize(num_nodes, -1);
if (LiteralIsTrue(ct.routes().literals(i))) {
// Check for loops.
if (tail != 0) {
if (has_outgoing_arc[tail]) {
VLOG(1) << "routes: node " << tail << "has two outgoing arcs";
return false;
}
has_outgoing_arc[tail] = true;
}
if (head != 0) {
if (has_incoming_arc[head]) {
VLOG(1) << "routes: node " << head << "has two incoming arcs";
return false;
}
has_incoming_arc[head] = true;
}
if (tail == head) {
if (tail == 0) return false;
if (tail == 0) {
VLOG(1) << "Self loop on node 0 are forbidden.";
return false;
}
++num_self_arcs;
continue;
}
@@ -1656,7 +1679,7 @@ class ConstraintChecker {
if (tail == 0) {
depot_nexts.push_back(head);
} else {
if (tail_to_head[tail] != -1) return false;
DCHECK_EQ(tail_to_head[tail], -1);
tail_to_head[tail] = head;
}
}
@@ -1769,9 +1792,9 @@ class ConstraintChecker {
// This indicates that such a constraint was not added to the model.
// It should probably be a validation error, but it is hard to
// detect beforehand.
LOG(ERROR) << "Warning, an interval constraint was likely used "
"without a corresponding linear constraint linking "
"its start, size and end.";
VLOG(1) << "Warning, an interval constraint was likely used "
"without a corresponding linear constraint linking "
"its start, size and end.";
}
return false;
}

20
ortools/sat/cp_model_checker_test.cc
View File

@@ -289,30 +289,34 @@ TEST(ValidateCpModelTest, VariableLowerBoundTooLarge2) {
}
TEST(ValidateCpModelTest, VariableDomainOverflow) {
CHECK_EQ(std::numeric_limits<int64_t>::max() - 1,
int64_t{9223372036854775806});
CHECK_EQ(std::numeric_limits<int64_t>::max() / 2,
int64_t{4611686018427387903});
const CpModelProto model_ok = ParseTestProto(R"pb(
variables { name: 'a' domain: 0 domain: 9223372036854775806 }
variables {
name: 'a'
domain: -4611686018427387903
domain: 4611686018427387903
}
)pb");
EXPECT_TRUE(ValidateCpModel(model_ok).empty());
const CpModelProto model_bad0 = ParseTestProto(R"pb(
variables { name: 'a' domain: -1 domain: 9223372036854775806 }
variables { name: 'a' domain: 0 domain: 4611686018427387904 }
)pb");
EXPECT_THAT(ValidateCpModel(model_bad0), HasSubstr("overflow"));
EXPECT_THAT(ValidateCpModel(model_bad0), HasSubstr("do not fall in"));
const CpModelProto model_bad1 = ParseTestProto(R"pb(
variables { name: 'a' domain: -2 domain: 9223372036854775806 }
variables { name: 'a' domain: -4611686018427387904 domain: 0 }
)pb");
EXPECT_THAT(ValidateCpModel(model_bad1), HasSubstr("overflow"));
EXPECT_THAT(ValidateCpModel(model_bad1), HasSubstr("do not fall in"));
CHECK_EQ(std::numeric_limits<int64_t>::min() + 2,
int64_t{-9223372036854775806});
const CpModelProto model_bad2 = ParseTestProto(R"pb(
variables { name: 'a' domain: -9223372036854775806 domain: 2 }
)pb");
EXPECT_THAT(ValidateCpModel(model_bad2), HasSubstr("overflow"));
EXPECT_THAT(ValidateCpModel(model_bad2), HasSubstr("do not fall in"));
}
TEST(ValidateCpModelTest, ObjectiveOverflow) {

27
ortools/sat/cp_model_presolve.cc
View File

@@ -12539,6 +12539,7 @@ bool ModelCopy::ImportAndSimplifyConstraints(
const CpModelProto& in_model, bool first_copy,
std::function<bool(int)> active_constraints) {
context_->InitializeNewDomains();
if (context_->ModelIsUnsat()) return false;
const bool ignore_names = context_->params().ignore_names();
// If first_copy is true, we reorder the scheduling constraint to be sure they
@@ -12593,6 +12594,9 @@ bool ModelCopy::ImportAndSimplifyConstraints(
case ConstraintProto::kIntDiv:
if (!CopyIntDiv(ct, ignore_names)) return CreateUnsatModel(c, ct);
break;
case ConstraintProto::kIntMod:
if (!CopyIntMod(ct, ignore_names)) return CreateUnsatModel(c, ct);
break;
case ConstraintProto::kElement:
if (!CopyElement(ct)) return CreateUnsatModel(c, ct);
break;
@@ -13061,6 +13065,7 @@ bool ModelCopy::CopyTable(const ConstraintProto& ct) {
}
*new_ct->mutable_table()->mutable_values() = ct.table().values();
new_ct->mutable_table()->set_negated(ct.table().negated());
*new_ct->mutable_enforcement_literal() = ct.enforcement_literal();
return true;
}
@@ -13068,7 +13073,9 @@ bool ModelCopy::CopyTable(const ConstraintProto& ct) {
bool ModelCopy::CopyAllDiff(const ConstraintProto& ct) {
if (ct.all_diff().exprs().size() <= 1) return true;
ConstraintProto* new_ct = context_->working_model->add_constraints();
*new_ct = ct;
for (const LinearExpressionProto& expr : ct.all_diff().exprs()) {
CopyLinearExpression(expr, new_ct->mutable_all_diff()->add_exprs());
}
return true;
}
@@ -13201,6 +13208,19 @@ bool ModelCopy::CopyIntDiv(const ConstraintProto& ct, bool ignore_names) {
return true;
}
bool ModelCopy::CopyIntMod(const ConstraintProto& ct, bool ignore_names) {
ConstraintProto* new_ct = context_->working_model->add_constraints();
if (!ignore_names) {
new_ct->set_name(ct.name());
}
for (const LinearExpressionProto& expr : ct.int_mod().exprs()) {
CopyLinearExpression(expr, new_ct->mutable_int_mod()->add_exprs());
}
CopyLinearExpression(ct.int_mod().target(),
new_ct->mutable_int_mod()->mutable_target());
return true;
}
bool ModelCopy::AddLinearConstraintForInterval(const ConstraintProto& ct) {
// Add the linear constraint enforcement => (start + size == end).
//
@@ -13276,9 +13296,9 @@ void ModelCopy::CopyAndMapNoOverlap2D(const ConstraintProto& ct) {
bool ModelCopy::CopyAndMapCumulative(const ConstraintProto& ct) {
if (ct.cumulative().intervals().empty() &&
ct.cumulative().capacity().vars().empty()) {
context_->IsFixed(ct.cumulative().capacity())) {
// Trivial constraint, either obviously SAT or UNSAT.
return ct.cumulative().capacity().offset() >= 0;
return context_->FixedValue(ct.cumulative().capacity()) >= 0;
}
// Note that we don't copy names or enforcement_literal (not supported) here.
auto* new_ct =
@@ -14357,6 +14377,7 @@ bool CpModelPresolver::MaybeRemoveFixedVariables(
// case, and it comment nicely that we do require domains to be up to date
// in the context.
context_->InitializeNewDomains();
if (context_->ModelIsUnsat()) return false;
// Initialize the mapping to remove all fixed variables.
const int num_vars = context_->working_model->variables().size();

1
ortools/sat/cp_model_presolve.h
View File

@@ -445,6 +445,7 @@ class ModelCopy {
bool CopyElement(const ConstraintProto& ct);
bool CopyIntProd(const ConstraintProto& ct, bool ignore_names);
bool CopyIntDiv(const ConstraintProto& ct, bool ignore_names);
bool CopyIntMod(const ConstraintProto& ct, bool ignore_names);
bool CopyLinear(const ConstraintProto& ct);
bool CopyLinearExpression(const LinearExpressionProto& expr,
LinearExpressionProto* dst);

31
ortools/sat/cp_model_solver.cc
View File

@@ -22,6 +22,7 @@
#include <functional>
#include <limits>
#include <memory>
#include <optional>
#include <random>
#include <string>
#include <thread>
@@ -51,6 +52,7 @@
#include "google/protobuf/text_format.h"
#include "ortools/base/logging.h"
#include "ortools/port/proto_utils.h"
#include "ortools/sat/combine_solutions.h"
#include "ortools/sat/cp_model.pb.h"
#include "ortools/sat/cp_model_checker.h"
#include "ortools/sat/cp_model_lns.h"
@@ -1542,6 +1544,19 @@ class LnsSolver : public SubSolver {
}
}
if (new_solution && !base_response.solution().empty()) {
std::string combined_solution_info = solution_info;
std::optional<std::vector<int64_t>> combined_solution =
FindCombinedSolution(shared_->model_proto, solution_values,
base_response.solution(), shared_->response,
&combined_solution_info);
if (combined_solution.has_value()) {
shared_->response->NewSolution(combined_solution.value(),
combined_solution_info,
/*model=*/nullptr);
}
}
generator_->AddSolveData(data);
if (VLOG_IS_ON(2) && display_lns_info) {
@@ -2346,6 +2361,22 @@ CpSolverResponse SolveCpModel(const CpModelProto& model_proto, Model* model) {
return shared_response_manager->GetResponse();
}
if (context->working_model->has_symmetry()) {
SOLVER_LOG(logger, "Ignoring internal symmetry field");
context->working_model->clear_symmetry();
}
if (context->working_model->has_objective()) {
CpObjectiveProto* objective = context->working_model->mutable_objective();
if (objective->integer_scaling_factor() != 0 ||
objective->integer_before_offset() != 0 ||
objective->integer_after_offset() != 0) {
SOLVER_LOG(logger, "Ignoring internal objective.integer_* fields.");
objective->clear_integer_scaling_factor();
objective->clear_integer_before_offset();
objective->clear_integer_after_offset();
}
}
if (absl::GetFlag(FLAGS_cp_model_ignore_objective) &&
(context->working_model->has_objective() ||
context->working_model->has_floating_point_objective())) {

4
ortools/sat/cp_model_solver_helpers.cc
View File

@@ -1268,7 +1268,9 @@ void LoadCpModel(const CpModelProto& model_proto, Model* model) {
// so this might take more time than wanted.
if (parameters.cp_model_probing_level() > 1) {
Prober* prober = model->GetOrCreate<Prober>();
prober->ProbeBooleanVariables(/*deterministic_time_limit=*/1.0);
if (!prober->ProbeBooleanVariables(/*deterministic_time_limit=*/1.0)) {
return unsat();
}
if (!model->GetOrCreate<BinaryImplicationGraph>()
->ComputeTransitiveReduction()) {
return unsat();

1
ortools/sat/cp_model_solver_helpers.h
View File

@@ -36,6 +36,7 @@
ABSL_DECLARE_FLAG(bool, cp_model_dump_models);
ABSL_DECLARE_FLAG(std::string, cp_model_dump_prefix);
ABSL_DECLARE_FLAG(bool, cp_model_dump_problematic_lns);
ABSL_DECLARE_FLAG(bool, cp_model_dump_submodels);
namespace operations_research {

17
ortools/sat/cumulative_energy.cc
View File

@@ -110,6 +110,14 @@ bool CumulativeEnergyConstraint::Propagate() {
bool tree_has_mandatory_intervals = false;
const IntegerValue start_end_magnitude =
std::max(IntTypeAbs(helper_->EndMax(
helper_->TaskByDecreasingEndMax().front().task_index)),
IntTypeAbs(helper_->TaskByIncreasingStartMin().front().time));
if (ProdOverflow(start_end_magnitude, capacity_max)) {
return true;
}
// Main loop: insert tasks by increasing end_max, check for overloads.
const auto by_decreasing_end_max = helper_->TaskByDecreasingEndMax();
for (const auto [current_task, current_end] :
@@ -535,9 +543,14 @@ bool CumulativeDualFeasibleEnergyConstraint::Propagate() {
IntTypeAbs(helper_->TaskByIncreasingStartMin().front().time));
if (start_end_magnitude == 0) return true;
const IntegerValue max_energy =
CapProdI(CapProdI(start_end_magnitude, capacity_max), num_events);
if (max_energy == kMaxIntegerValue) {
return true;
}
const IntegerValue max_for_fixpoint_inverse =
std::numeric_limits<IntegerValue>::max() /
(num_events * capacity_max * start_end_magnitude);
std::numeric_limits<IntegerValue>::max() / max_energy;
theta_tree_.Reset(num_events);

182
ortools/sat/fuzz_testdata/NoOverlap2DOptimization Normal file
View File

@@ -0,0 +1,182 @@
# proto-file: ortools/sat/cp_model.proto
# proto-message: operations_research.sat.CpModelProto
variables: {
name: "x_0"
domain: [ 0, 80 ]
}
variables: {
name: "y_0"
domain: [ 0, 40 ]
}
variables: {
name: "x_1"
domain: [ 0, 80 ]
}
variables: {
name: "y_1"
domain: [ 0, 60 ]
}
variables: {
name: "x_2"
domain: [ 0, 90 ]
}
variables: {
name: "y_2"
domain: [ 0, 50 ]
}
variables: { domain: [ 1, 1 ] }
variables: { domain: [ 0, 200 ] }
variables: { domain: [ 0, 200 ] }
variables: { domain: [ 0, 200 ] }
variables: { domain: [ 0, 200 ] }
variables: { domain: [ 0, 200 ] }
variables: { domain: [ 0, 200 ] }
constraints: {
no_overlap_2d: {
x_intervals: [ 1, 3, 5 ]
y_intervals: [ 2, 4, 6 ]
}
}
constraints: {
name: "x_interval_0"
enforcement_literal: 6
interval: {
start: { vars: 0 coeffs: 1 }
end: { vars: 0 coeffs: 1 offset: 20 }
size: { offset: 20 }
}
}
constraints: {
name: "y_interval_0"
enforcement_literal: 6
interval: {
start: { vars: 1 coeffs: 1 }
end: { vars: 1 coeffs: 1 offset: 60 }
size: { offset: 60 }
}
}
constraints: {
name: "x_interval_1"
enforcement_literal: 6
interval: {
start: { vars: 2 coeffs: 1 }
end: { vars: 2 coeffs: 1 offset: 20 }
size: { offset: 20 }
}
}
constraints: {
name: "y_interval_1"
enforcement_literal: 6
interval: {
start: { vars: 3 coeffs: 1 }
end: { vars: 3 coeffs: 1 offset: 40 }
size: { offset: 40 }
}
}
constraints: {
name: "x_interval_2"
enforcement_literal: 6
interval: {
start: { vars: 4 coeffs: 1 }
end: { vars: 4 coeffs: 1 offset: 10 }
size: { offset: 10 }
}
}
constraints: {
name: "y_interval_2"
enforcement_literal: 6
interval: {
start: { vars: 5 coeffs: 1 }
end: { vars: 5 coeffs: 1 offset: 50 }
size: { offset: 50 }
}
}
constraints: {
linear: {
vars: [ 7, 0, 2 ]
coeffs: [ 1, -2, 2 ]
domain: [ 0, 9223372036854775807 ]
}
}
constraints: {
linear: {
vars: [ 7, 0, 2 ]
coeffs: [ 1, 2, -2 ]
domain: [ 0, 9223372036854775807 ]
}
}
constraints: {
linear: {
vars: [ 8, 0, 4 ]
coeffs: [ 1, -2, 2 ]
domain: [ 10, 9223372036854775807 ]
}
}
constraints: {
linear: {
vars: [ 8, 0, 4 ]
coeffs: [ 1, 2, -2 ]
domain: [ -10, 9223372036854775807 ]
}
}
constraints: {
linear: {
vars: [ 9, 2, 4 ]
coeffs: [ 1, -2, 2 ]
domain: [ 10, 9223372036854775807 ]
}
}
constraints: {
linear: {
vars: [ 9, 2, 4 ]
coeffs: [ 1, 2, -2 ]
domain: [ -10, 9223372036854775807 ]
}
}
constraints: {
linear: {
vars: [ 10, 1, 3 ]
coeffs: [ 1, -2, 2 ]
domain: [ 20, 9223372036854775807 ]
}
}
constraints: {
linear: {
vars: [ 10, 1, 3 ]
coeffs: [ 1, 2, -2 ]
domain: [ -20, 9223372036854775807 ]
}
}
constraints: {
linear: {
vars: [ 11, 1, 5 ]
coeffs: [ 1, -2, 2 ]
domain: [ 10, 9223372036854775807 ]
}
}
constraints: {
linear: {
vars: [ 11, 1, 5 ]
coeffs: [ 1, 2, -2 ]
domain: [ -10, 9223372036854775807 ]
}
}
constraints: {
linear: {
vars: [ 12, 3, 5 ]
coeffs: [ 1, -2, 2 ]
domain: [ -10, 9223372036854775807 ]
}
}
constraints: {
linear: {
vars: [ 12, 3, 5 ]
coeffs: [ 1, 2, -2 ]
domain: [ 10, 9223372036854775807 ]
}
}
objective: {
vars: [ 7, 8, 9, 10, 11, 12 ]
coeffs: [ 1, 1, 1, 1, 1, 1 ]
}

13
ortools/sat/intervals.cc
View File

@@ -849,11 +849,14 @@ void SchedulingConstraintHelper::ImportOtherReasons(
}
std::string SchedulingConstraintHelper::TaskDebugString(int t) const {
return absl::StrCat("t=", t, " is_present=", IsPresent(t), " size=[",
SizeMin(t).value(), ",", SizeMax(t).value(), "]",
" start=[", StartMin(t).value(), ",", StartMax(t).value(),
"]", " end=[", EndMin(t).value(), ",", EndMax(t).value(),
"]");
return absl::StrCat("t=", t, " is_present=",
(IsPresent(t) ? "1"
: IsAbsent(t) ? "0"
: "?"),
" size=[", SizeMin(t).value(), ",", SizeMax(t).value(),
"]", " start=[", StartMin(t).value(), ",",
StartMax(t).value(), "]", " end=[", EndMin(t).value(),
",", EndMax(t).value(), "]");
}
IntegerValue SchedulingConstraintHelper::GetMinOverlap(int t,

15
ortools/sat/intervals.h
View File

@@ -519,6 +519,17 @@ class SchedulingConstraintHelper : public PropagatorInterface {
int CurrentDecisionLevel() const { return trail_->CurrentDecisionLevel(); }
private:
// Tricky: when a task is optional, it is possible it size min is negative,
// but we know that if a task is present, its size should be >= 0. So in the
// reason, when we need the size_min and it is currently negative, we can just
// ignore it and use zero instead.
AffineExpression NegatedSizeOrZero(int t) {
if (integer_trail_->LowerBound(sizes_[t]) <= 0) {
return AffineExpression(0);
}
return sizes_[t].Negated();
}
// Generic reason for a <= upper_bound, given that a = b + c in case the
// current upper bound of a is not good enough.
void AddGenericReason(const AffineExpression& a, IntegerValue upper_bound,
@@ -877,7 +888,7 @@ inline void SchedulingConstraintHelper::AddStartMaxReason(
int t, IntegerValue upper_bound) {
AddOtherReason(t);
DCHECK(!IsAbsent(t));
AddGenericReason(starts_[t], upper_bound, ends_[t], sizes_[t].Negated());
AddGenericReason(starts_[t], upper_bound, ends_[t], NegatedSizeOrZero(t));
}
inline void SchedulingConstraintHelper::AddEndMinReason(
@@ -885,7 +896,7 @@ inline void SchedulingConstraintHelper::AddEndMinReason(
AddOtherReason(t);
DCHECK(!IsAbsent(t));
AddGenericReason(minus_ends_[t], -lower_bound, minus_starts_[t],
sizes_[t].Negated());
NegatedSizeOrZero(t));
}
inline void SchedulingConstraintHelper::AddEndMaxReason(

4
ortools/sat/linear_relaxation.cc
View File

@@ -964,6 +964,10 @@ void AddCumulativeRelaxation(const AffineExpression& capacity,
//
// TODO(user): In some cases, we could have only one task that can be
// first.
if (ProdOverflow(std::max(-min_of_starts, max_of_ends),
integer_trail->UpperBound(capacity))) {
return;
}
const AffineExpression span_start = min_of_starts;
const AffineExpression span_end =
makespan.has_value() ? makespan.value() : max_of_ends;

26
ortools/sat/shaving_solver.cc
View File

@@ -74,8 +74,7 @@ std::function<void()> ObjectiveShavingSolver::GenerateTask(int64_t task_id) {
objective_ub_ = shared_->response->GetInnerObjectiveUpperBound();
}
return [this, task_id]() {
if (ResetModel(task_id)) {
SolveLoadedCpModel(local_proto_, local_sat_model_.get());
if (ResetAndSolveModel(task_id)) {
const CpSolverResponse local_response =
local_sat_model_->GetOrCreate<SharedResponseManager>()->GetResponse();
@@ -150,7 +149,7 @@ std::string ObjectiveShavingSolver::Info() {
" csts=", local_proto_.constraints().size(), ")");
}
bool ObjectiveShavingSolver::ResetModel(int64_t task_id) {
bool ObjectiveShavingSolver::ResetAndSolveModel(int64_t task_id) {
local_sat_model_ = std::make_unique<Model>(name());
*local_sat_model_->GetOrCreate<SatParameters>() = local_params_;
local_sat_model_->GetOrCreate<SatParameters>()->set_random_seed(
@@ -202,16 +201,24 @@ bool ObjectiveShavingSolver::ResetModel(int64_t task_id) {
local_proto_.mutable_variables(local_proto_.objective().vars(0));
const Domain reduced_var_domain = obj_domain.IntersectionWith(
Domain(obj_var->domain(0), obj_var->domain(1)));
if (reduced_var_domain.IsEmpty()) {
return false;
}
FillDomainInProto(reduced_var_domain, obj_var);
} else {
auto* obj = local_proto_.add_constraints()->mutable_linear();
*obj->mutable_vars() = local_proto_.objective().vars();
*obj->mutable_coeffs() = local_proto_.objective().coeffs();
if (obj_domain.IsEmpty()) {
return false;
}
FillDomainInProto(obj_domain, obj);
}
// Clear the objective.
local_proto_.clear_objective();
local_proto_.set_name(
absl::StrCat(local_proto_.name(), "_obj_shaving_", objective_lb.value()));
// Dump?
if (absl::GetFlag(FLAGS_cp_model_dump_submodels)) {
@@ -316,8 +323,7 @@ std::function<void()> VariablesShavingSolver::GenerateTask(int64_t task_id) {
Model local_sat_model;
CpModelProto shaving_proto;
State state;
if (ResetModel(task_id, &state, &local_sat_model, &shaving_proto)) {
SolveLoadedCpModel(shaving_proto, &local_sat_model);
if (ResetAndSolveModel(task_id, &state, &local_sat_model, &shaving_proto)) {
const CpSolverResponse local_response =
local_sat_model.GetOrCreate<SharedResponseManager>()->GetResponse();
ProcessLocalResponse(local_response, state);
@@ -498,9 +504,9 @@ void VariablesShavingSolver::CopyModelConnectedToVar(
}
}
bool VariablesShavingSolver::ResetModel(int64_t task_id, State* state,
Model* local_sat_model,
CpModelProto* shaving_proto) {
bool VariablesShavingSolver::ResetAndSolveModel(int64_t task_id, State* state,
Model* local_sat_model,
CpModelProto* shaving_proto) {
*local_sat_model->GetOrCreate<SatParameters>() = local_params_;
local_sat_model->GetOrCreate<SatParameters>()->set_random_seed(
CombineSeed(local_params_.random_seed(), task_id));
@@ -519,6 +525,9 @@ bool VariablesShavingSolver::ResetModel(int64_t task_id, State* state,
time_limit->GetElapsedDeterministicTime() +
local_params_.shaving_search_deterministic_time());
shaving_proto->set_name(absl::StrCat("shaving_var_", state->var_index,
(state->minimize ? "_min" : "_max")));
// Presolve if asked.
if (local_params_.cp_model_presolve()) {
std::vector<int> postsolve_mapping;
@@ -550,6 +559,7 @@ bool VariablesShavingSolver::ResetModel(int64_t task_id, State* state,
if (time_limit->LimitReached()) return false;
LoadCpModel(*shaving_proto, local_sat_model);
SolveLoadedCpModel(*shaving_proto, local_sat_model);
return true;
}

6
ortools/sat/shaving_solver.h
View File

@@ -51,7 +51,7 @@ class ObjectiveShavingSolver : public SubSolver {
private:
std::string Info();
bool ResetModel(int64_t task_id);
bool ResetAndSolveModel(int64_t task_id);
// This is fixed at construction.
SatParameters local_params_;
@@ -114,8 +114,8 @@ class VariablesShavingSolver : public SubSolver {
CpModelProto* shaving_proto)
ABSL_SHARED_LOCKS_REQUIRED(mutex_);
bool ResetModel(int64_t task_id, State* state, Model* local_sat_model,
CpModelProto* shaving_proto);
bool ResetAndSolveModel(int64_t task_id, State* state, Model* local_sat_model,
CpModelProto* shaving_proto);
// This is fixed at construction.
SatParameters local_params_;

28
ortools/sat/synchronization.h
View File

@@ -14,6 +14,7 @@
#ifndef OR_TOOLS_SAT_SYNCHRONIZATION_H_
#define OR_TOOLS_SAT_SYNCHRONIZATION_H_
#include <algorithm>
#include <array>
#include <atomic>
#include <cstddef>
@@ -26,6 +27,7 @@
#include <utility>
#include <vector>
#include "absl/algorithm/container.h"
#include "absl/base/thread_annotations.h"
#include "absl/container/btree_map.h"
#include "absl/container/flat_hash_map.h"
@@ -104,6 +106,8 @@ class SharedSolutionRepository {
// You shouldn't call this if NumSolutions() is zero.
int64_t GetBestRank() const;
std::vector<std::shared_ptr<const Solution>> GetBestNSolutions(int n) const;
// Returns the variable value of variable 'var_index' from solution
// 'solution_index' where solution_index must be smaller than NumSolutions()
// and 'var_index' must be smaller than number of variables.
@@ -829,6 +833,30 @@ int64_t SharedSolutionRepository<ValueType>::GetBestRank() const {
return solutions_[0]->rank;
}
template <typename ValueType>
std::vector<std::shared_ptr<
const typename SharedSolutionRepository<ValueType>::Solution>>
SharedSolutionRepository<ValueType>::GetBestNSolutions(int n) const {
absl::MutexLock mutex_lock(&mutex_);
// Sorted and unique.
DCHECK(absl::c_is_sorted(
solutions_,
[](const std::shared_ptr<const Solution>& a,
const std::shared_ptr<const Solution>& b) { return *a < *b; }));
DCHECK(absl::c_adjacent_find(solutions_,
[](const std::shared_ptr<const Solution>& a,
const std::shared_ptr<const Solution>& b) {
return *a == *b;
}) == solutions_.end());
std::vector<std::shared_ptr<const Solution>> result;
const int num_solutions = std::min(static_cast<int>(solutions_.size()), n);
result.reserve(num_solutions);
for (int i = 0; i < num_solutions; ++i) {
result.push_back(solutions_[i]);
}
return result;
}
template <typename ValueType>
ValueType SharedSolutionRepository<ValueType>::GetVariableValueInSolution(
int var_index, int solution_index) const {