diff --git a/ortools/sat/BUILD.bazel b/ortools/sat/BUILD.bazel index 11263baba3..b9b0fa7d2f 100644 --- a/ortools/sat/BUILD.bazel +++ b/ortools/sat/BUILD.bazel @@ -1873,6 +1873,7 @@ cc_library( ":sat_base", ":sat_parameters_cc_proto", "//ortools/base", + "//ortools/base:mathlimits", "//ortools/base:mathutil", "//ortools/base:stl_util", "//ortools/util:random_engine", diff --git a/ortools/sat/python/cp_model_test.py b/ortools/sat/python/cp_model_test.py index 31060a4c77..3b70696175 100644 --- a/ortools/sat/python/cp_model_test.py +++ b/ortools/sat/python/cp_model_test.py @@ -1014,6 +1014,12 @@ class CpModelTest(absltest.TestCase): self.assertEqual(size_expr, 2) self.assertEqual(str(end_expr), "(x + 2)") + def testAbsentInterval(self): + print("testInterval") + model = cp_model.CpModel() + i = model.new_optional_interval_var(1, 0, 1, False, "") + self.assertEqual(0, i.index) + def testOptionalInterval(self): print("testOptionalInterval") model = cp_model.CpModel() diff --git a/ortools/sat/samples/code_samples.bzl b/ortools/sat/samples/code_samples.bzl index 7e352a4fc8..92f9ebde9d 100644 --- a/ortools/sat/samples/code_samples.bzl +++ b/ortools/sat/samples/code_samples.bzl @@ -16,7 +16,6 @@ load("@pip_deps//:requirements.bzl", "requirement") load("@rules_python//python:defs.bzl", "py_binary", "py_test") - def code_sample_cc(name): native.cc_binary( name = name + "_cc", diff --git a/ortools/sat/sat_parameters.proto b/ortools/sat/sat_parameters.proto index 9a0eda5be3..c98489d3a1 100644 --- a/ortools/sat/sat_parameters.proto +++ b/ortools/sat/sat_parameters.proto @@ -1094,7 +1094,7 @@ message SatParameters { // Minimum number of restarts before a worker will replace a subtree // that looks "bad" based on the average LBD of learned clauses. optional int32 shared_tree_worker_min_restarts_per_subtree = 282 - [default = 32]; + [default = 1]; // If true, workers share more of the information from their local trail. // Specifically, literals implied by the shared tree decisions and diff --git a/ortools/sat/util.h b/ortools/sat/util.h index fb5f337ee1..9fe0a1548f 100644 --- a/ortools/sat/util.h +++ b/ortools/sat/util.h @@ -36,6 +36,7 @@ #include "absl/strings/string_view.h" #include "absl/types/span.h" #include "ortools/base/logging.h" +#include "ortools/base/mathlimits.h" #include "ortools/sat/model.h" #include "ortools/sat/sat_base.h" #include "ortools/sat/sat_parameters.pb.h" diff --git a/ortools/sat/work_assignment.cc b/ortools/sat/work_assignment.cc index 78cd47482f..23cc13a254 100644 --- a/ortools/sat/work_assignment.cc +++ b/ortools/sat/work_assignment.cc @@ -626,15 +626,15 @@ bool SharedTreeWorker::AddImplications() { rev_num_processed_implications_.resize(level + 1, 0); auto& num_processed_implications = rev_num_processed_implications_[level]; reversible_int_repository_->SaveState(&num_processed_implications); - absl::Span implied_literals = - assigned_tree_.Implications(level).subspan(num_processed_implications); + absl::Span implied_literals = + absl::MakeConstSpan(assigned_tree_implications_[level - 1]) + .subspan(num_processed_implications); bool added_clause = false; - for (const ProtoLiteral& impl : implied_literals) { - Literal lit(DecodeDecision(impl)); + for (Literal impl : implied_literals) { ++num_processed_implications; - if (sat_solver_->Assignment().LiteralIsTrue(lit)) continue; + if (sat_solver_->Assignment().LiteralIsTrue(impl)) continue; added_clause = true; - if (!AddDecisionImplication(lit, level)) return true; + if (!AddDecisionImplication(impl, level)) return true; } if (objective_ != nullptr && objective_->objective_var != kNoIntegerVariable) { @@ -687,10 +687,19 @@ bool SharedTreeWorker::SyncWithLocalTrail() { << " assigned=" << assigned_tree_.MaxLevel(); manager_->CloseTree(assigned_tree_, level + 1); assigned_tree_literals_.clear(); + assigned_tree_implications_.clear(); sat_solver_->Backtrack(0); } else { // The next level is implied by the current one. assigned_tree_.SetLevelImplied(level + 1); + if (level > 0) { + assigned_tree_implications_[level - 1].insert( + assigned_tree_implications_[level - 1].end(), + assigned_tree_implications_[level].begin(), + assigned_tree_implications_[level].end()); + } + assigned_tree_implications_.erase(assigned_tree_implications_.begin() + + level); assigned_tree_literals_.erase(assigned_tree_literals_.begin() + level); } } @@ -760,6 +769,7 @@ void SharedTreeWorker::MaybeProposeSplit() { manager_->ProposeSplit(assigned_tree_, *encoded); if (assigned_tree_.MaxLevel() > assigned_tree_literals_.size()) { assigned_tree_literals_.push_back(split_decision); + assigned_tree_implications_.push_back({}); } CHECK_EQ(assigned_tree_literals_.size(), assigned_tree_.MaxLevel()); } @@ -808,9 +818,15 @@ bool SharedTreeWorker::SyncWithSharedTree() { VLOG(2) << "Assigned level: " << assigned_tree_.MaxLevel() << " " << parameters_->name(); assigned_tree_literals_.clear(); + assigned_tree_implications_.clear(); for (int i = 1; i <= assigned_tree_.MaxLevel(); ++i) { assigned_tree_literals_.push_back( DecodeDecision(assigned_tree_.Decision(i))); + std::vector implications; + for (const ProtoLiteral& impl : assigned_tree_.Implications(i)) { + implications.push_back(DecodeDecision(impl)); + } + assigned_tree_implications_.push_back(std::move(implications)); } return true; } diff --git a/ortools/sat/work_assignment.h b/ortools/sat/work_assignment.h index 8d45bc7227..44b65fa103 100644 --- a/ortools/sat/work_assignment.h +++ b/ortools/sat/work_assignment.h @@ -67,6 +67,7 @@ class ProtoLiteral { return H::combine(std::move(h), literal.proto_var_, literal.lb_); } + // Note you should only decode integer literals at the root level. Literal Decode(CpModelMapping*, IntegerEncoder*) const; static std::optional Encode(Literal, CpModelMapping*, IntegerEncoder*); @@ -324,6 +325,7 @@ class SharedTreeWorker { ProtoTrail assigned_tree_; std::vector assigned_tree_literals_; + std::vector> assigned_tree_implications_; // How many restarts had happened when the current tree was assigned? int64_t tree_assignment_restart_ = -1;