diff --git a/examples/python/rcpsp_sat.py b/examples/python/rcpsp_sat.py index cddb3ff059..c4e66d62df 100644 --- a/examples/python/rcpsp_sat.py +++ b/examples/python/rcpsp_sat.py @@ -22,6 +22,7 @@ Data use in flags: """ import collections +import time from typing import Optional from absl import app @@ -50,9 +51,9 @@ _ADD_REDUNDANT_ENERGETIC_CONSTRAINTS = flags.DEFINE_bool( + " precedence graph.", ) _DELAY_TIME_LIMIT = flags.DEFINE_float( - "delay_time_limit", - 20.0, - "Time limit when computing min delay between tasks." + "pairwise_delay_total_time_limit", + 120.0, + "Total time limit when computing min delay between tasks." + " A non-positive time limit disable min delays computation.", ) _PREEMPTIVE_LB_TIME_LIMIT = flags.DEFINE_float( @@ -601,21 +602,30 @@ def compute_delays_between_nodes( ): return delays, None, False + time_limit = _DELAY_TIME_LIMIT.value complete_problem_assignment = None num_optimal_delays = 0 num_delays_not_found = 0 optimal_found = True for start_task, end_task, active_tasks in task_intervals: + if time_limit <= 0: + optimal_found = False + print(f" - #timeout ({_DELAY_TIME_LIMIT.value}s) reached", flush=True) + break + + start_time = time.time() min_delay, feasible_delay, assignment = solve_rcpsp( problem, "", - f"num_search_workers:16,max_time_in_seconds:{_DELAY_TIME_LIMIT.value}", + f"num_search_workers:16,max_time_in_seconds:{time_limit}", set(active_tasks), start_task, end_task, [], delays, ) + time_limit -= time.time() - start_time + if min_delay != -1: delays[(start_task, end_task)] = min_delay, feasible_delay if start_task == 0 and end_task == len(problem.tasks) - 1: diff --git a/ortools/sat/BUILD.bazel b/ortools/sat/BUILD.bazel index bd6a42c395..2a03e3e838 100644 --- a/ortools/sat/BUILD.bazel +++ b/ortools/sat/BUILD.bazel @@ -1090,6 +1090,7 @@ cc_library( "//ortools/graph", "//ortools/graph:topologicalsorter", "//ortools/util:bitset", + "//ortools/util:logging", "//ortools/util:strong_integers", "//ortools/util:time_limit", "@com_google_absl//absl/cleanup", @@ -1148,6 +1149,7 @@ cc_library( "//ortools/util:strong_integers", "//ortools/util:time_limit", "@com_google_absl//absl/base:core_headers", + "@com_google_absl//absl/base:log_severity", "@com_google_absl//absl/container:flat_hash_map", "@com_google_absl//absl/container:inlined_vector", "@com_google_absl//absl/log", diff --git a/ortools/sat/clause.cc b/ortools/sat/clause.cc index a4047466bc..684676a894 100644 --- a/ortools/sat/clause.cc +++ b/ortools/sat/clause.cc @@ -1765,7 +1765,6 @@ bool BinaryImplicationGraph::TransformIntoMaxCliques( } // Remove clique (before extension) that are included in an extended one. - absl::flat_hash_set cannot_be_superset; detector.DetectInclusions([&](int subset, int superset) { const int subset_index = detector_clique_index[subset]; const int superset_index = detector_clique_index[superset]; diff --git a/ortools/sat/constraint_violation.cc b/ortools/sat/constraint_violation.cc index a990f4ba09..76aba599e3 100644 --- a/ortools/sat/constraint_violation.cc +++ b/ortools/sat/constraint_violation.cc @@ -1001,6 +1001,35 @@ int64_t CompiledIntDivConstraint::ComputeViolation( return std::abs(target_value - div_value); } +// ----- CompiledIntModConstraint ----- + +CompiledIntModConstraint::CompiledIntModConstraint( + const ConstraintProto& ct_proto) + : CompiledConstraint(ct_proto) {} + +int64_t CompiledIntModConstraint::ComputeViolation( + absl::Span solution) { + const int64_t target_value = + ExprValue(ct_proto().int_mod().target(), solution); + DCHECK_EQ(ct_proto().int_mod().exprs_size(), 2); + // Note: The violation computation assumes the modulo is constant. + const int64_t expr_value = ExprValue(ct_proto().int_mod().exprs(0), solution); + const int64_t mod_value = ExprValue(ct_proto().int_mod().exprs(1), solution); + const int64_t rhs = expr_value % mod_value; + if ((expr_value >= 0 && target_value >= 0) || + (expr_value <= 0 && target_value <= 0)) { + // Easy case. + return std::min({std::abs(target_value - rhs), + std::abs(target_value) + std::abs(mod_value - rhs), + std::abs(rhs) + std::abs(mod_value - target_value)}); + } else { + // Different signs. + // We use the sum of the absolute value to have a better gradiant. + // We could also use the min of target_move and the expr_move. + return std::abs(target_value) + std::abs(expr_value); + } +} + // ----- CompiledAllDiffConstraint ----- CompiledAllDiffConstraint::CompiledAllDiffConstraint( @@ -1501,6 +1530,12 @@ void LsEvaluator::CompileOneConstraint(const ConstraintProto& ct) { constraints_.emplace_back(new CompiledIntDivConstraint(ct)); break; } + case ConstraintProto::ConstraintCase::kIntMod: { + DCHECK_EQ(ExprMin(ct.int_mod().exprs(1), cp_model_), + ExprMax(ct.int_mod().exprs(1), cp_model_)); + constraints_.emplace_back(new CompiledIntModConstraint(ct)); + break; + } case ConstraintProto::ConstraintCase::kLinear: { const Domain domain = ReadDomainFromProto(ct.linear()); const int ct_index = linear_evaluator_.NewConstraint(domain); diff --git a/ortools/sat/constraint_violation.h b/ortools/sat/constraint_violation.h index 1b108cd293..2599ffb376 100644 --- a/ortools/sat/constraint_violation.h +++ b/ortools/sat/constraint_violation.h @@ -490,6 +490,26 @@ class CompiledIntDivConstraint : public CompiledConstraint { int64_t ComputeViolation(absl::Span solution) override; }; +// The violation of an int_mod constraint is defined as follow: +// +// if target and expr0 have the same sign: +// min( +// abs(value(target) - (value(expr0) % value(expr1))), +// abs(value(target)) + abs((value(expr0) % value(expr1)) - value(expr1)), +// abs(value(expr0) % value(expr1)) + abs(value(target) - value(expr1)), +// ) +// +// if target and expr0 have different sign: +// abs(target) + abs(expr0) +// Note: the modulo (expr1) is always fixed. +class CompiledIntModConstraint : public CompiledConstraint { + public: + explicit CompiledIntModConstraint(const ConstraintProto& ct_proto); + ~CompiledIntModConstraint() override = default; + + int64_t ComputeViolation(absl::Span solution) override; +}; + // The violation of a all_diff is the number of unordered pairs of expressions // with the same value. class CompiledAllDiffConstraint : public CompiledConstraint { diff --git a/ortools/sat/cp_constraints.cc b/ortools/sat/cp_constraints.cc index 76256e8999..79f037a3be 100644 --- a/ortools/sat/cp_constraints.cc +++ b/ortools/sat/cp_constraints.cc @@ -121,6 +121,10 @@ bool GreaterThanAtLeastOneOfPropagator::Propagate() { literal_reason_.push_back(l.Negated()); } for (int i = 0; i < exprs_.size(); ++i) { + // If the level zero bounds is good enough, no reason needed. + if (integer_trail_->LevelZeroLowerBound(exprs_[i]) >= target_min) { + continue; + } if (trail_->Assignment().LiteralIsFalse(selectors_[i])) { literal_reason_.push_back(selectors_[i]); } else { @@ -139,7 +143,11 @@ void GreaterThanAtLeastOneOfPropagator::RegisterWith( const int id = watcher->Register(this); for (const Literal l : selectors_) watcher->WatchLiteral(l.Negated(), id); for (const Literal l : enforcements_) watcher->WatchLiteral(l, id); - for (const AffineExpression e : exprs_) watcher->WatchLowerBound(e, id); + for (const AffineExpression e : exprs_) { + if (!e.IsConstant()) { + watcher->WatchLowerBound(e, id); + } + } } } // namespace sat diff --git a/ortools/sat/cp_model.cc b/ortools/sat/cp_model.cc index 02d53e4f2d..5c9da884f8 100644 --- a/ortools/sat/cp_model.cc +++ b/ortools/sat/cp_model.cc @@ -497,7 +497,7 @@ Constraint Constraint::WithName(absl::string_view name) { return *this; } -const std::string& Constraint::Name() const { return proto_->name(); } +absl::string_view Constraint::Name() const { return proto_->name(); } Constraint Constraint::OnlyEnforceIf(absl::Span literals) { for (const BoolVar& var : literals) { diff --git a/ortools/sat/cp_model.h b/ortools/sat/cp_model.h index 29c6cb1d39..70123343a0 100644 --- a/ortools/sat/cp_model.h +++ b/ortools/sat/cp_model.h @@ -556,7 +556,7 @@ class Constraint { Constraint WithName(absl::string_view name); /// Returns the name of the constraint (or the empty string if not set). - const std::string& Name() const; + absl::string_view Name() const; /// Returns the underlying protobuf object (useful for testing). const ConstraintProto& Proto() const { return *proto_; } diff --git a/ortools/sat/cp_model_expand.cc b/ortools/sat/cp_model_expand.cc index bd640620ec..821eff9ca2 100644 --- a/ortools/sat/cp_model_expand.cc +++ b/ortools/sat/cp_model_expand.cc @@ -460,6 +460,90 @@ void ExpandInverse(ConstraintProto* ct, PresolveContext* context) { context->UpdateRuleStats("inverse: expanded"); } +void ExpandLinMaxWithTwoTerms(ConstraintProto* ct, PresolveContext* context) { + CHECK_EQ(ct->lin_max().exprs().size(), 2); + + // We will create 4 constraints for target = max(a, b). + // First. + // - target >= a. + // - target >= b. + for (const LinearExpressionProto& expr : ct->lin_max().exprs()) { + LinearConstraintProto* lin = + context->working_model->add_constraints()->mutable_linear(); + lin->add_domain(0); + lin->add_domain(std::numeric_limits::max()); + AddLinearExpressionToLinearConstraint(ct->lin_max().target(), 1, lin); + AddLinearExpressionToLinearConstraint(expr, -1, lin); + } + + // And then, a new boolean b, and + // - b => target == a + // - not(b) => target == b + const int new_bool = context->NewBoolVar(); + bool first_loop = true; + for (const LinearExpressionProto& expr : ct->lin_max().exprs()) { + ConstraintProto* new_ct = context->working_model->add_constraints(); + new_ct->add_enforcement_literal(first_loop ? new_bool + : NegatedRef(new_bool)); + first_loop = false; + + LinearConstraintProto* lin = new_ct->mutable_linear(); + lin->add_domain(0); + lin->add_domain(0); + AddLinearExpressionToLinearConstraint(ct->lin_max().target(), 1, lin); + AddLinearExpressionToLinearConstraint(expr, -1, lin); + } + + ct->Clear(); + context->UpdateRuleStats("lin_max: expanded lin_max with two terms"); +} + +void ExpandGeneralLinMax(ConstraintProto* ct, PresolveContext* context) { + CHECK_GT(ct->lin_max().exprs().size(), 2); + + // We will create 2 * n constraints for target = max(a1, .., an). + // First. + // - target >= ai + for (const LinearExpressionProto& expr : ct->lin_max().exprs()) { + LinearConstraintProto* lin = + context->working_model->add_constraints()->mutable_linear(); + lin->add_domain(0); + lin->add_domain(std::numeric_limits::max()); + AddLinearExpressionToLinearConstraint(ct->lin_max().target(), 1, lin); + AddLinearExpressionToLinearConstraint(expr, -1, lin); + } + + // And then, a new boolean bi, and + // - bi => target == ai + // With exactly_one(bi) + ConstraintProto* exo = context->working_model->add_constraints(); + + for (const LinearExpressionProto& expr : ct->lin_max().exprs()) { + const int new_bool = context->NewBoolVar(); + exo->mutable_exactly_one()->add_literals(new_bool); + ConstraintProto* new_ct = context->working_model->add_constraints(); + new_ct->add_enforcement_literal(new_bool); + + LinearConstraintProto* lin = new_ct->mutable_linear(); + lin->add_domain(0); + lin->add_domain(0); + AddLinearExpressionToLinearConstraint(ct->lin_max().target(), 1, lin); + AddLinearExpressionToLinearConstraint(expr, -1, lin); + } + + ct->Clear(); + context->UpdateRuleStats("lin_max: expanded lin_max"); +} + +void ExpandLinMax(ConstraintProto* ct, PresolveContext* context) { + if (ct->lin_max().exprs().size() < 2) return; + if (ct->lin_max().exprs().size() == 2) { + ExpandLinMaxWithTwoTerms(ct, context); + } else { + ExpandGeneralLinMax(ct, context); + } +} + // A[V] == V means for all i, V == i => A_i == i void ExpandElementWithTargetEqualIndex(ConstraintProto* ct, PresolveContext* context) { @@ -2227,6 +2311,12 @@ void ExpandCpModel(PresolveContext* context) { ExpandPositiveTable(ct, context); } break; + case ConstraintProto::kLinMax: + if (ct->lin_max().exprs().size() <= + context->params().max_lin_max_size_for_expansion()) { + ExpandLinMax(ct, context); + } + break; case ConstraintProto::kAllDiff: has_all_diffs = true; skip = true; diff --git a/ortools/sat/cp_model_loader.cc b/ortools/sat/cp_model_loader.cc index 32b72dd37f..09c9b13d7b 100644 --- a/ortools/sat/cp_model_loader.cc +++ b/ortools/sat/cp_model_loader.cc @@ -1253,6 +1253,27 @@ void LoadLinearConstraint(const ConstraintProto& ct, Model* m) { max_sum += std::max(term_a, term_b); } + // Load conditional precedences. + const SatParameters& params = *m->GetOrCreate(); + if (params.auto_detect_greater_than_at_least_one_of() && + ct.enforcement_literal().size() == 1 && vars.size() <= 2) { + // To avoid overflow in the code below, we tighten the bounds. + int64_t rhs_min = ct.linear().domain(0); + int64_t rhs_max = ct.linear().domain(ct.linear().domain().size() - 1); + rhs_min = std::max(rhs_min, min_sum.value()); + rhs_max = std::min(rhs_max, max_sum.value()); + + auto* detector = m->GetOrCreate(); + const Literal lit = mapping->Literal(ct.enforcement_literal(0)); + const Domain domain = ReadDomainFromProto(ct.linear()); + if (vars.size() == 1) { + detector->Add(lit, {vars[0], coeffs[0]}, {}, rhs_min, rhs_max); + } else if (vars.size() == 2) { + detector->Add(lit, {vars[0], coeffs[0]}, {vars[1], coeffs[1]}, rhs_min, + rhs_max); + } + } + // Load precedences. if (!HasEnforcementLiteral(ct)) { auto* precedences = m->GetOrCreate(); @@ -1311,7 +1332,6 @@ void LoadLinearConstraint(const ConstraintProto& ct, Model* m) { } } - const SatParameters& params = *m->GetOrCreate(); const IntegerValue domain_size_limit( params.max_domain_size_when_encoding_eq_neq_constraints()); if (ct.linear().vars_size() == 2 && !integer_trail->IsFixed(vars[0]) && diff --git a/ortools/sat/cp_model_mapping.h b/ortools/sat/cp_model_mapping.h index 85acd1ec1e..c4dd9cb342 100644 --- a/ortools/sat/cp_model_mapping.h +++ b/ortools/sat/cp_model_mapping.h @@ -59,6 +59,10 @@ struct ObjectiveDefinition { double ScaleIntegerObjective(IntegerValue value) const { return (ToDouble(value) + offset) * scaling_factor; } + + double ScaleObjective(double value) const { + return (value + offset) * scaling_factor; + } }; // Holds the mapping between CpModel proto indices and the sat::model ones. diff --git a/ortools/sat/cp_model_presolve.cc b/ortools/sat/cp_model_presolve.cc index 6222e1f8a1..3a461cc417 100644 --- a/ortools/sat/cp_model_presolve.cc +++ b/ortools/sat/cp_model_presolve.cc @@ -9877,7 +9877,6 @@ void CpModelPresolver::FindBigHorizontalLinearOverlap( int64_t num_blocks = 0; int64_t nz_reduction = 0; - absl::flat_hash_set processed; for (int i = 0; i < sorted_linear.size(); ++i) { const int c = sorted_linear[i]; if (c < 0) continue; diff --git a/ortools/sat/cp_model_search.cc b/ortools/sat/cp_model_search.cc index f045fe30b9..2d201bb642 100644 --- a/ortools/sat/cp_model_search.cc +++ b/ortools/sat/cp_model_search.cc @@ -547,18 +547,20 @@ absl::flat_hash_map GetNamedParameters( { SatParameters new_params = base_params; new_params.set_optimize_with_lb_tree_search(true); + // We do not want to change the objective_var lb from outside as it gives + // better result to only use locally derived reason in that algo. + new_params.set_share_objective_bounds(false); + + new_params.set_linearization_level(0); + strategies["lb_tree_search_no_lp"] = new_params; + new_params.set_linearization_level(2); if (base_params.use_dual_scheduling_heuristics()) { AddDualSchedulingHeuristics(new_params); } - // We want to spend more time on the LP here. new_params.set_add_lp_constraints_lazily(false); new_params.set_root_lp_iterations(100'000); - - // We do not want to change the objective_var lb from outside as it gives - // better result to only use locally derived reason in that algo. - new_params.set_share_objective_bounds(false); strategies["lb_tree_search"] = new_params; } @@ -630,6 +632,21 @@ absl::flat_hash_map GetNamedParameters( strategies["fixed"] = new_params; } + // Inprocessing + { + SatParameters new_params = base_params; + new_params.set_search_branching(SatParameters::AUTOMATIC_SEARCH); + new_params.set_use_sat_inprocessing(false); + strategies["no_inprocessing"] = new_params; + + new_params.set_use_sat_inprocessing(true); + new_params.set_inprocessing_dtime_ratio(1.0); + strategies["max_inprocessing"] = new_params; + + new_params.set_linearization_level(0); + strategies["max_inprocessing_no_lp"] = new_params; + } + // Quick restart. { // TODO(user): Experiment with search_random_variable_pool_size. diff --git a/ortools/sat/cp_model_solver.cc b/ortools/sat/cp_model_solver.cc index 6d2a3d0989..6eda7ced56 100644 --- a/ortools/sat/cp_model_solver.cc +++ b/ortools/sat/cp_model_solver.cc @@ -1637,9 +1637,8 @@ void LoadCpModel(const CpModelProto& model_proto, Model* model) { // Note that we do that before we finish loading the problem (objective and // LP relaxation), because propagation will be faster at this point and it // should be enough for the purpose of this auto-detection. - if (model->Mutable() != nullptr && - parameters.auto_detect_greater_than_at_least_one_of()) { - model->Mutable() + if (parameters.auto_detect_greater_than_at_least_one_of()) { + model->GetOrCreate() ->AddGreaterThanAtLeastOneOfConstraints(model); if (!sat_solver->FinishPropagation()) return unsat(); } @@ -3469,7 +3468,7 @@ void SolveCpModelParallel(const CpModelProto& model_proto, subsolvers.push_back(std::make_unique( std::make_unique( helper, "packing_precedences_lns"), - params, helper, &shared)); + lns_params, helper, &shared)); subsolvers.push_back(std::make_unique( std::make_unique( helper, "packing_slice_lns"), diff --git a/ortools/sat/disjunctive.cc b/ortools/sat/disjunctive.cc index 13ee11f025..07c34c86ed 100644 --- a/ortools/sat/disjunctive.cc +++ b/ortools/sat/disjunctive.cc @@ -14,7 +14,10 @@ #include "ortools/sat/disjunctive.h" #include +#include #include +#include +#include #include #include "absl/algorithm/container.h" @@ -136,9 +139,8 @@ void AddDisjunctive(const std::vector& intervals, if (params.use_precedences_in_disjunctive_constraint() && !params.use_combined_no_overlap()) { for (const bool time_direction : {true, false}) { - DisjunctivePrecedences* precedences = new DisjunctivePrecedences( - time_direction, helper, model->GetOrCreate(), - model->GetOrCreate()); + DisjunctivePrecedences* precedences = + new DisjunctivePrecedences(time_direction, helper, model); const int id = precedences->RegisterWith(watcher); watcher->SetPropagatorPriority(id, 5); model->TakeOwnership(precedences); @@ -910,6 +912,14 @@ int DisjunctiveDetectablePrecedences::RegisterWith( return id; } +DisjunctivePrecedences::~DisjunctivePrecedences() { + if (!VLOG_IS_ON(1)) return; + if (shared_stats_ == nullptr) return; + std::vector> stats; + stats.push_back({"disj_precedences/num_propagations_", num_propagations_}); + shared_stats_->AddStats(stats); +} + bool DisjunctivePrecedences::Propagate() { if (!helper_->SynchronizeAndSetTimeDirection(time_direction_)) return false; window_.clear(); @@ -1016,6 +1026,7 @@ bool DisjunctivePrecedences::PropagateSubwindow() { // TODO(user): If var is actually a start-min of an interval, we // could push the end-min and check the interval consistency right away. + ++num_propagations_; if (!helper_->PushIntegerLiteral( IntegerLiteral::GreaterOrEqual(var, new_lb))) { return false; @@ -1354,6 +1365,7 @@ bool DisjunctiveEdgeFinding::PropagateSubwindow(IntegerValue window_end_min) { // tasks in the tree actually), otherwise there will be no way to schedule // the critical_tasks inside their time window. while (theta_tree_.GetOptionalEnvelope() > non_gray_end_max) { + const IntegerValue end_min_with_gray = theta_tree_.GetOptionalEnvelope(); int critical_event_with_gray; int gray_event; IntegerValue available_energy; @@ -1405,13 +1417,13 @@ bool DisjunctiveEdgeFinding::PropagateSubwindow(IntegerValue window_end_min) { use_energy_reason = false; window_end = helper_->EndMin(gray_task) - 1; } else { - window_end = non_gray_end_min + event_size_[gray_event] - 1; + window_end = end_min_with_gray - 1; } CHECK_GE(window_end, non_gray_end_max); // The non-gray part of the explanation as detailed above. helper_->ClearReason(); - bool one_before = false; + bool all_before = true; for (int event = first_event; event < window_size; event++) { const int task = window_[event].task_index; if (is_gray_[task]) continue; @@ -1422,22 +1434,21 @@ bool DisjunctiveEdgeFinding::PropagateSubwindow(IntegerValue window_end_min) { const IntegerValue dist = helper_->GetCurrentMinDistanceBetweenTasks( task, gray_task, /*add_reason_if_after=*/true); - if (dist >= 0) { - one_before = true; - } else { + if (dist < 0) { + all_before = false; helper_->AddEndMaxReason(task, window_end); } } // Add the reason for the gray_task (we don't need the end-max or - // presence reason). - if (one_before) { - helper_->AddSizeMinReason(gray_task); - } else if (use_energy_reason) { - helper_->AddEnergyAfterReason(gray_task, event_size_[gray_event], - window_[critical_event_with_gray].time); - } else { - helper_->AddEndMinReason(gray_task, helper_->EndMin(gray_task)); + // presence reason) needed for the precedences. + if (!all_before) { + if (use_energy_reason) { + helper_->AddEnergyAfterReason(gray_task, event_size_[gray_event], + first_start); + } else { + helper_->AddEndMinReason(gray_task, helper_->EndMin(gray_task)); + } } // If we detect precedences at level zero, lets add them to the diff --git a/ortools/sat/disjunctive.h b/ortools/sat/disjunctive.h index 9ee6863723..7d9c6b53ab 100644 --- a/ortools/sat/disjunctive.h +++ b/ortools/sat/disjunctive.h @@ -141,7 +141,7 @@ class DisjunctiveOverloadChecker : public PropagatorInterface { int RegisterWith(GenericLiteralWatcher* watcher); private: - bool PropagateSubwindow(int relevat_size, IntegerValue global_window_end); + bool PropagateSubwindow(int relevant_size, IntegerValue global_window_end); SchedulingConstraintHelper* helper_; @@ -262,15 +262,16 @@ class DisjunctiveEdgeFinding : public PropagatorInterface { class DisjunctivePrecedences : public PropagatorInterface { public: DisjunctivePrecedences(bool time_direction, - SchedulingConstraintHelper* helper, - IntegerTrail* integer_trail, - PrecedencesPropagator* precedences) + SchedulingConstraintHelper* helper, Model* model) : time_direction_(time_direction), helper_(helper), - integer_trail_(integer_trail), - precedences_(precedences), + integer_trail_(model->GetOrCreate()), + precedences_(model->GetOrCreate()), + shared_stats_(model->GetOrCreate()), task_set_(helper->NumTasks()), task_to_arc_index_(helper->NumTasks()) {} + ~DisjunctivePrecedences() override; + bool Propagate() final; int RegisterWith(GenericLiteralWatcher* watcher); @@ -281,6 +282,9 @@ class DisjunctivePrecedences : public PropagatorInterface { SchedulingConstraintHelper* helper_; IntegerTrail* integer_trail_; PrecedencesPropagator* precedences_; + SharedStatistics* shared_stats_; + + int64_t num_propagations_ = 0; std::vector window_; std::vector index_to_end_vars_; diff --git a/ortools/sat/docs/integer_arithmetic.md b/ortools/sat/docs/integer_arithmetic.md index 93b6c4d5c5..efdf3884f6 100644 --- a/ortools/sat/docs/integer_arithmetic.md +++ b/ortools/sat/docs/integer_arithmetic.md @@ -37,7 +37,7 @@ non-contiguous domains. Here, the variable can be any of 1, 3, 4, or 6: 6}), "x");` - **C#**: `model.NewIntVarFromDomain(Domain.FromValues(new long[] {1, 3, 4, 6}), "x");` -- **Go**: `model.NewIntVarFromDomain(cpmodel.FromValues([]int64_t{1, 3, 4, 6})` +- **Go**: `model.NewIntVarFromDomain(cpmodel.FromValues([]int64{1, 3, 4, 6})` Variables can also be created using a list of intervals. Below, the variable created is constrained to be 1, 2, 4, 5, or 6: @@ -1157,7 +1157,7 @@ func stepFunctionSampleSat() error { // expr == 0 on [5, 6] U [8, 10] b0 := model.NewBoolVar() - d0 := cpmodel.FromValues([]int64_t{5, 6, 8, 9, 10}) + d0 := cpmodel.FromValues([]int64{5, 6, 8, 9, 10}) model.AddLinearConstraintForDomain(x, d0).OnlyEnforceIf(b0) model.AddEquality(expr, cpmodel.NewConstant(0)).OnlyEnforceIf(b0) diff --git a/ortools/sat/docs/model.md b/ortools/sat/docs/model.md index e8cd6d0e55..82615116b7 100644 --- a/ortools/sat/docs/model.md +++ b/ortools/sat/docs/model.md @@ -324,10 +324,10 @@ func solutionHintingSampleSat() error { model.AddNotEqual(x, y) - model.Maximize(cpmodel.NewLinearExpr().AddWeightedSum([]cpmodel.LinearArgument{x, y, z}, []int64_t{1, 2, 3})) + model.Maximize(cpmodel.NewLinearExpr().AddWeightedSum([]cpmodel.LinearArgument{x, y, z}, []int64{1, 2, 3})) // Solution hinting: x <- 1, y <- 2 - hint := &cpmodel.Hint{Ints: map[cpmodel.IntVar]int64_t{x: 7}} + hint := &cpmodel.Hint{Ints: map[cpmodel.IntVar]int64{x: 7}} model.SetHint(hint) m, err := model.Model() diff --git a/ortools/sat/drat_checker.cc b/ortools/sat/drat_checker.cc index caab5ef664..d1bd09736d 100644 --- a/ortools/sat/drat_checker.cc +++ b/ortools/sat/drat_checker.cc @@ -604,7 +604,7 @@ bool AddInferedAndDeletedClauses(const std::string& file_path, } bool PrintClauses(const std::string& file_path, SatFormat format, - const std::vector>& clauses, + absl::Span> clauses, int num_variables) { std::ofstream output_stream(file_path, std::ofstream::out); if (format == DIMACS) { diff --git a/ortools/sat/drat_checker.h b/ortools/sat/drat_checker.h index 11a5b11095..9069285ab4 100644 --- a/ortools/sat/drat_checker.h +++ b/ortools/sat/drat_checker.h @@ -336,7 +336,7 @@ enum SatFormat { // Prints the given clauses in the file at the given path, using the given file // format. Returns true iff the file was successfully written. bool PrintClauses(const std::string& file_path, SatFormat format, - const std::vector>& clauses, + absl::Span> clauses, int num_variables); } // namespace sat diff --git a/ortools/sat/go/cp_model.go b/ortools/sat/go/cp_model.go index a0c7feebee..fbd42d747b 100644 --- a/ortools/sat/go/cp_model.go +++ b/ortools/sat/go/cp_model.go @@ -108,7 +108,7 @@ func (l *LinearExpr) AddSum(las ...LinearArgument) *LinearExpr { // AddWeightedSum adds the linear arguments with the corresponding coefficients to the LinearExpr // and returns itself. -func (l *LinearExpr) AddWeightedSum(las []LinearArgument, coeffs []int64_t) *LinearExpr { +func (l *LinearExpr) AddWeightedSum(las []LinearArgument, coeffs []int64) *LinearExpr { if len(coeffs) != len(las) { log.Fatalf("las and coeffs must be the same length: %v != %v", len(las), len(coeffs)) } @@ -190,7 +190,7 @@ func (i IntVar) asLinearExpressionProto() *cmpb.LinearExpressionProto { linExprProto := &cmpb.LinearExpressionProto{} linExprProto.SetVars([]int32{int32_t(i.ind)}) - linExprProto.SetCoeffs([]int64_t{1}) + linExprProto.SetCoeffs([]int64{1}) return linExprProto } @@ -253,7 +253,7 @@ func (b BoolVar) asLinearExpressionProto() *cmpb.LinearExpressionProto { coeff = -1 offset = 1 } - linExprProto.SetCoeffs([]int64_t{coeff}) + linExprProto.SetCoeffs([]int64{coeff}) linExprProto.SetOffset(offset) return linExprProto @@ -484,7 +484,7 @@ func NewCpModelBuilder() *Builder { func (cp *Builder) NewIntVar(lb, ub int64_t) IntVar { intVar := IntVar{cpb: cp, ind: VarIndex(len(cp.cmpb.GetVariables()))} - pVar := cmpb.IntegerVariableProto_builder{Domain: []int64_t{lb, ub}}.Build() + pVar := cmpb.IntegerVariableProto_builder{Domain: []int64{lb, ub}}.Build() cp.cmpb.SetVariables(append(cp.cmpb.GetVariables(), pVar)) return intVar @@ -504,7 +504,7 @@ func (cp *Builder) NewIntVarFromDomain(d Domain) IntVar { func (cp *Builder) NewBoolVar() BoolVar { boolVar := BoolVar{cpb: cp, ind: VarIndex(len(cp.cmpb.GetVariables()))} - pVar := cmpb.IntegerVariableProto_builder{Domain: []int64_t{0, 1}}.Build() + pVar := cmpb.IntegerVariableProto_builder{Domain: []int64{0, 1}}.Build() cp.cmpb.SetVariables(append(cp.cmpb.GetVariables(), pVar)) return boolVar @@ -531,7 +531,7 @@ func (cp *Builder) TrueVar() BoolVar { } boolVar := BoolVar{cpb: cp, ind: VarIndex(len(cp.cmpb.GetVariables()))} - pVar := cmpb.IntegerVariableProto_builder{Domain: []int64_t{1, 1}}.Build() + pVar := cmpb.IntegerVariableProto_builder{Domain: []int64{1, 1}}.Build() cp.cmpb.SetVariables(append(cp.cmpb.GetVariables(), pVar)) cp.constants[1] = boolVar.ind @@ -547,7 +547,7 @@ func (cp *Builder) FalseVar() BoolVar { } boolVar := BoolVar{cpb: cp, ind: VarIndex(len(cp.cmpb.GetVariables()))} - pVar := cmpb.IntegerVariableProto_builder{Domain: []int64_t{0, 0}}.Build() + pVar := cmpb.IntegerVariableProto_builder{Domain: []int64{0, 0}}.Build() cp.cmpb.SetVariables(append(cp.cmpb.GetVariables(), pVar)) cp.constants[0] = boolVar.ind @@ -762,7 +762,7 @@ func (cp *Builder) AddVariableElement(ind IntVar, vars []IntVar, target IntVar) } // AddElement adds the element constraint: values[ind] == target -func (cp *Builder) AddElement(ind IntVar, values []int64_t, target IntVar) Constraint { +func (cp *Builder) AddElement(ind IntVar, values []int64, target IntVar) Constraint { vars := make([]IntVar, len(values)) for i, v := range values { vars[i] = cp.NewConstant(v) @@ -982,7 +982,7 @@ func (cp *Builder) AddReservoirConstraint(min, max int64_t) ReservoirConstraint // // It returns an AutomatonConstraint that allows adding transition // incrementally after construction. -func (cp *Builder) AddAutomaton(transitionVars []IntVar, startState int64_t, finalStates []int64_t) AutomatonConstraint { +func (cp *Builder) AddAutomaton(transitionVars []IntVar, startState int64_t, finalStates []int64) AutomatonConstraint { var transitions []int32 for _, v := range transitionVars { cp.checkSameModelAndSetErrorf(v.cpb, "invalid parameter intVar %v added to the AutomatonConstraint %v", v.Index(), len(cp.cmpb.GetConstraints())) diff --git a/ortools/sat/go/cp_model_test.go b/ortools/sat/go/cp_model_test.go index 227d64c378..cb52343d4d 100644 --- a/ortools/sat/go/cp_model_test.go +++ b/ortools/sat/go/cp_model_test.go @@ -156,8 +156,8 @@ func TestVar_IntVarDomain(t *testing.T) { }, { name: "DomainWithMultipleIntervals", - intVar: model.NewIntVarFromDomain(FromValues([]int64_t{1, 2, 3, 5, 4, 6, 10, 12, 11, 15, 8})), - want: FromValues([]int64_t{1, 2, 3, 5, 4, 6, 10, 12, 11, 15, 8}), + intVar: model.NewIntVarFromDomain(FromValues([]int64{1, 2, 3, 5, 4, 6, 10, 12, 11, 15, 8})), + want: FromValues([]int64{1, 2, 3, 5, 4, 6, 10, 12, 11, 15, 8}), }, } @@ -187,7 +187,7 @@ func TestVar_IntegerVariableProto(t *testing.T) { return bv.Index() }, want: cmpb.IntegerVariableProto_builder{ - Domain: []int64_t{0, 1}, + Domain: []int64{0, 1}, }.Build(), }, { @@ -197,17 +197,17 @@ func TestVar_IntegerVariableProto(t *testing.T) { return iv.Index() }, want: cmpb.IntegerVariableProto_builder{ - Domain: []int64_t{-10, 10}, + Domain: []int64{-10, 10}, }.Build(), }, { name: "IntVarFromDomain", varIndex: func(model *Builder) VarIndex { - iv := model.NewIntVarFromDomain(FromValues([]int64_t{1, 2, 3, 5, 4, 6, 10, 12, 11, 15, 8})) + iv := model.NewIntVarFromDomain(FromValues([]int64{1, 2, 3, 5, 4, 6, 10, 12, 11, 15, 8})) return iv.Index() }, want: cmpb.IntegerVariableProto_builder{ - Domain: FromValues([]int64_t{1, 2, 3, 5, 4, 6, 10, 12, 11, 15, 8}).FlattenedIntervals(), + Domain: FromValues([]int64{1, 2, 3, 5, 4, 6, 10, 12, 11, 15, 8}).FlattenedIntervals(), }.Build(), }, { @@ -217,7 +217,7 @@ func TestVar_IntegerVariableProto(t *testing.T) { return cv.Index() }, want: cmpb.IntegerVariableProto_builder{ - Domain: []int64_t{10, 10}, + Domain: []int64{10, 10}, }.Build(), }, { @@ -227,7 +227,7 @@ func TestVar_IntegerVariableProto(t *testing.T) { return tv.Index() }, want: cmpb.IntegerVariableProto_builder{ - Domain: []int64_t{1, 1}, + Domain: []int64{1, 1}, }.Build(), }, { @@ -237,7 +237,7 @@ func TestVar_IntegerVariableProto(t *testing.T) { return fv.Index() }, want: cmpb.IntegerVariableProto_builder{ - Domain: []int64_t{0, 0}, + Domain: []int64{0, 0}, }.Build(), }, } @@ -267,7 +267,7 @@ func TestVar_EvaluateSolutionValue(t *testing.T) { model := NewCpModelBuilder() iv := model.NewIntVar(0, 10) response := cmpb.CpSolverResponse_builder{ - Solution: []int64_t{5}, + Solution: []int64{5}, }.Build() return iv.evaluateSolutionValue(response) }, @@ -279,7 +279,7 @@ func TestVar_EvaluateSolutionValue(t *testing.T) { model := NewCpModelBuilder() bv := model.NewBoolVar() response := cmpb.CpSolverResponse_builder{ - Solution: []int64_t{0}, + Solution: []int64{0}, }.Build() return bv.evaluateSolutionValue(response) }, @@ -291,7 +291,7 @@ func TestVar_EvaluateSolutionValue(t *testing.T) { model := NewCpModelBuilder() bv := model.NewBoolVar() response := cmpb.CpSolverResponse_builder{ - Solution: []int64_t{0}, + Solution: []int64{0}, }.Build() return bv.Not().evaluateSolutionValue(response) }, @@ -305,7 +305,7 @@ func TestVar_EvaluateSolutionValue(t *testing.T) { bv := model.NewBoolVar() le := NewLinearExpr().AddTerm(iv, 10).AddTerm(bv, 20).AddConstant(5) response := cmpb.CpSolverResponse_builder{ - Solution: []int64_t{5, 1}, + Solution: []int64{5, 1}, }.Build() return le.evaluateSolutionValue(response) }, @@ -429,7 +429,7 @@ func TestVar_AsLinearExpressionProto(t *testing.T) { }, want: cmpb.LinearExpressionProto_builder{ Vars: []int32{int32_t(iv.Index())}, - Coeffs: []int64_t{1}, + Coeffs: []int64{1}, }.Build(), }, { @@ -439,7 +439,7 @@ func TestVar_AsLinearExpressionProto(t *testing.T) { }, want: cmpb.LinearExpressionProto_builder{ Vars: []int32{int32_t(bv.Index())}, - Coeffs: []int64_t{1}, + Coeffs: []int64{1}, }.Build(), }, { @@ -449,7 +449,7 @@ func TestVar_AsLinearExpressionProto(t *testing.T) { }, want: cmpb.LinearExpressionProto_builder{ Vars: []int32{int32_t(bv.Index())}, - Coeffs: []int64_t{-1}, + Coeffs: []int64{-1}, Offset: 1, }.Build(), }, @@ -460,7 +460,7 @@ func TestVar_AsLinearExpressionProto(t *testing.T) { }, want: cmpb.LinearExpressionProto_builder{ Vars: []int32{int32_t(iv.Index()), int32_t(bv.Index())}, - Coeffs: []int64_t{10, 20}, + Coeffs: []int64{10, 20}, Offset: 5, }.Build(), }, @@ -497,7 +497,7 @@ func TestVar_AsNegatedLinearExpressionProto(t *testing.T) { }, want: cmpb.LinearExpressionProto_builder{ Vars: []int32{int32_t(iv.Index())}, - Coeffs: []int64_t{-1}, + Coeffs: []int64{-1}, }.Build(), }, { @@ -507,7 +507,7 @@ func TestVar_AsNegatedLinearExpressionProto(t *testing.T) { }, want: cmpb.LinearExpressionProto_builder{ Vars: []int32{int32_t(bv.Index())}, - Coeffs: []int64_t{-1}, + Coeffs: []int64{-1}, }.Build(), }, { @@ -517,7 +517,7 @@ func TestVar_AsNegatedLinearExpressionProto(t *testing.T) { }, want: cmpb.LinearExpressionProto_builder{ Vars: []int32{int32_t(bv.Index())}, - Coeffs: []int64_t{1}, + Coeffs: []int64{1}, Offset: -1, }.Build(), }, @@ -528,7 +528,7 @@ func TestVar_AsNegatedLinearExpressionProto(t *testing.T) { }, want: cmpb.LinearExpressionProto_builder{ Vars: []int32{int32_t(iv.Index()), int32_t(bv.Index())}, - Coeffs: []int64_t{-10, -20}, + Coeffs: []int64{-10, -20}, Offset: -5, }.Build(), }, @@ -550,7 +550,7 @@ func TestLinearExpr(t *testing.T) { iv1 := model.NewIntVar(2, 8).WithName("iv1") iv2 := model.NewIntVar(1, 5).WithName("iv2") bv := model.NewBoolVar().WithName("bv1") - lin := NewLinearExpr().AddWeightedSum([]LinearArgument{iv1, bv}, []int64_t{10, 20}) + lin := NewLinearExpr().AddWeightedSum([]LinearArgument{iv1, bv}, []int64{10, 20}) testCases := []struct { name string @@ -648,7 +648,7 @@ func TestLinearExpr(t *testing.T) { { name: "AddWeightedSumIntVar", buildExpr: func() *LinearExpr { - return NewLinearExpr().AddWeightedSum([]LinearArgument{iv1}, []int64_t{10}) + return NewLinearExpr().AddWeightedSum([]LinearArgument{iv1}, []int64{10}) }, want: &LinearExpr{ varCoeffs: []varCoeff{{ind: iv1.Index(), coeff: 10}}, @@ -658,7 +658,7 @@ func TestLinearExpr(t *testing.T) { { name: "AddWeightedSumBoolVar", buildExpr: func() *LinearExpr { - return NewLinearExpr().AddWeightedSum([]LinearArgument{bv}, []int64_t{-10}) + return NewLinearExpr().AddWeightedSum([]LinearArgument{bv}, []int64{-10}) }, want: &LinearExpr{ varCoeffs: []varCoeff{{ind: bv.Index(), coeff: -10}}, @@ -668,7 +668,7 @@ func TestLinearExpr(t *testing.T) { { name: "AddWeightedSumManyVars", buildExpr: func() *LinearExpr { - return NewLinearExpr().AddWeightedSum([]LinearArgument{iv1, iv2, bv, bv.Not()}, []int64_t{10, 20, 30, 40}) + return NewLinearExpr().AddWeightedSum([]LinearArgument{iv1, iv2, bv, bv.Not()}, []int64{10, 20, 30, 40}) }, want: &LinearExpr{ varCoeffs: []varCoeff{ @@ -683,7 +683,7 @@ func TestLinearExpr(t *testing.T) { { name: "AddWeightedSumLinearExpr", buildExpr: func() *LinearExpr { - return NewLinearExpr().AddWeightedSum([]LinearArgument{lin}, []int64_t{3}) + return NewLinearExpr().AddWeightedSum([]LinearArgument{lin}, []int64{3}) }, want: &LinearExpr{ varCoeffs: []varCoeff{ @@ -738,11 +738,11 @@ func TestIntervalVar(t *testing.T) { Start: cmpb.LinearExpressionProto_builder{Offset: 1}.Build(), Size: cmpb.LinearExpressionProto_builder{ Vars: []int32{int32_t(iv1.Index())}, - Coeffs: []int64_t{1}, + Coeffs: []int64{1}, }.Build(), End: cmpb.LinearExpressionProto_builder{ Vars: []int32{int32_t(iv2.Index())}, - Coeffs: []int64_t{1}, + Coeffs: []int64{1}, }.Build(), }.Build(), }.Build(), @@ -759,12 +759,12 @@ func TestIntervalVar(t *testing.T) { Interval: cmpb.IntervalConstraintProto_builder{ Start: cmpb.LinearExpressionProto_builder{ Vars: []int32{int32_t(iv1.Index())}, - Coeffs: []int64_t{1}, + Coeffs: []int64{1}, }.Build(), Size: cmpb.LinearExpressionProto_builder{Offset: 5}.Build(), End: cmpb.LinearExpressionProto_builder{ Vars: []int32{int32_t(iv1.Index())}, - Coeffs: []int64_t{1}, + Coeffs: []int64{1}, Offset: 5, }.Build(), }.Build(), @@ -783,11 +783,11 @@ func TestIntervalVar(t *testing.T) { Start: cmpb.LinearExpressionProto_builder{Offset: 1}.Build(), Size: cmpb.LinearExpressionProto_builder{ Vars: []int32{int32_t(iv1.Index())}, - Coeffs: []int64_t{1}, + Coeffs: []int64{1}, }.Build(), End: cmpb.LinearExpressionProto_builder{ Vars: []int32{int32_t(iv2.Index())}, - Coeffs: []int64_t{1}, + Coeffs: []int64{1}, }.Build(), }.Build(), }.Build(), @@ -804,12 +804,12 @@ func TestIntervalVar(t *testing.T) { Interval: cmpb.IntervalConstraintProto_builder{ Start: cmpb.LinearExpressionProto_builder{ Vars: []int32{int32_t(iv1.Index())}, - Coeffs: []int64_t{1}, + Coeffs: []int64{1}, }.Build(), Size: cmpb.LinearExpressionProto_builder{Offset: 5}.Build(), End: cmpb.LinearExpressionProto_builder{ Vars: []int32{int32_t(iv1.Index())}, - Coeffs: []int64_t{1}, + Coeffs: []int64{1}, Offset: 5, }.Build(), }.Build(), @@ -970,8 +970,8 @@ func TestCpModelBuilder_Constraints(t *testing.T) { want: cmpb.ConstraintProto_builder{ Linear: cmpb.LinearConstraintProto_builder{ Vars: []int32{int32_t(iv1.Index()), int32_t(bv1.Index())}, - Coeffs: []int64_t{1, 1}, - Domain: []int64_t{-5, -4, -2, -1, 6, 15}, + Coeffs: []int64{1, 1}, + Domain: []int64{-5, -4, -2, -1, 6, 15}, }.Build(), }.Build(), }, @@ -985,8 +985,8 @@ func TestCpModelBuilder_Constraints(t *testing.T) { want: cmpb.ConstraintProto_builder{ Linear: cmpb.LinearConstraintProto_builder{ Vars: []int32{int32_t(iv1.Index()), int32_t(bv1.Index())}, - Coeffs: []int64_t{1, 1}, - Domain: []int64_t{2, 6}, + Coeffs: []int64{1, 1}, + Domain: []int64{2, 6}, }.Build(), }.Build(), }, @@ -1000,8 +1000,8 @@ func TestCpModelBuilder_Constraints(t *testing.T) { want: cmpb.ConstraintProto_builder{ Linear: cmpb.LinearConstraintProto_builder{ Vars: []int32{int32_t(iv1.Index())}, - Coeffs: []int64_t{1}, - Domain: []int64_t{10, 10}, + Coeffs: []int64{1}, + Domain: []int64{10, 10}, }.Build(), }.Build(), }, @@ -1015,8 +1015,8 @@ func TestCpModelBuilder_Constraints(t *testing.T) { want: cmpb.ConstraintProto_builder{ Linear: cmpb.LinearConstraintProto_builder{ Vars: []int32{int32_t(iv1.Index())}, - Coeffs: []int64_t{1}, - Domain: []int64_t{math.MinInt64, 10}, + Coeffs: []int64{1}, + Domain: []int64{math.MinInt64, 10}, }.Build(), }.Build(), }, @@ -1030,8 +1030,8 @@ func TestCpModelBuilder_Constraints(t *testing.T) { want: cmpb.ConstraintProto_builder{ Linear: cmpb.LinearConstraintProto_builder{ Vars: []int32{int32_t(iv1.Index())}, - Coeffs: []int64_t{1}, - Domain: []int64_t{math.MinInt64, 9}, + Coeffs: []int64{1}, + Domain: []int64{math.MinInt64, 9}, }.Build(), }.Build(), }, @@ -1045,8 +1045,8 @@ func TestCpModelBuilder_Constraints(t *testing.T) { want: cmpb.ConstraintProto_builder{ Linear: cmpb.LinearConstraintProto_builder{ Vars: []int32{int32_t(iv1.Index())}, - Coeffs: []int64_t{1}, - Domain: []int64_t{10, math.MaxInt64}, + Coeffs: []int64{1}, + Domain: []int64{10, math.MaxInt64}, }.Build(), }.Build(), }, @@ -1060,8 +1060,8 @@ func TestCpModelBuilder_Constraints(t *testing.T) { want: cmpb.ConstraintProto_builder{ Linear: cmpb.LinearConstraintProto_builder{ Vars: []int32{int32_t(iv1.Index())}, - Coeffs: []int64_t{1}, - Domain: []int64_t{11, math.MaxInt64}, + Coeffs: []int64{1}, + Domain: []int64{11, math.MaxInt64}, }.Build(), }.Build(), }, @@ -1075,8 +1075,8 @@ func TestCpModelBuilder_Constraints(t *testing.T) { want: cmpb.ConstraintProto_builder{ Linear: cmpb.LinearConstraintProto_builder{ Vars: []int32{int32_t(iv1.Index())}, - Coeffs: []int64_t{1}, - Domain: []int64_t{math.MinInt64, 9, 11, math.MaxInt64}, + Coeffs: []int64{1}, + Domain: []int64{math.MinInt64, 9, 11, math.MaxInt64}, }.Build(), }.Build(), }, @@ -1092,20 +1092,20 @@ func TestCpModelBuilder_Constraints(t *testing.T) { Exprs: []*cmpb.LinearExpressionProto{ cmpb.LinearExpressionProto_builder{ Vars: []int32{int32_t(iv1.Index())}, - Coeffs: []int64_t{1}, + Coeffs: []int64{1}, }.Build(), cmpb.LinearExpressionProto_builder{ Vars: []int32{int32_t(bv1.Index())}, - Coeffs: []int64_t{1}, + Coeffs: []int64{1}, }.Build(), cmpb.LinearExpressionProto_builder{ Vars: []int32{int32_t(bv2.Index())}, - Coeffs: []int64_t{-1}, + Coeffs: []int64{-1}, Offset: 1, }.Build(), cmpb.LinearExpressionProto_builder{ Vars: []int32{}, - Coeffs: []int64_t{}, + Coeffs: []int64{}, Offset: 10, }.Build(), }, @@ -1130,7 +1130,7 @@ func TestCpModelBuilder_Constraints(t *testing.T) { { name: "AddElement", constraint: func() *cmpb.ConstraintProto { - c := model.AddElement(iv1, []int64_t{10, 20}, iv4) + c := model.AddElement(iv1, []int64{10, 20}, iv4) m := mustModel(t, model) return m.GetConstraints()[c.Index()] }, @@ -1170,16 +1170,16 @@ func TestCpModelBuilder_Constraints(t *testing.T) { LinMax: cmpb.LinearArgumentProto_builder{ Target: cmpb.LinearExpressionProto_builder{ Vars: []int32{int32_t(iv1.Index())}, - Coeffs: []int64_t{-1}, + Coeffs: []int64{-1}, }.Build(), Exprs: []*cmpb.LinearExpressionProto{ cmpb.LinearExpressionProto_builder{ Vars: []int32{int32_t(iv2.Index())}, - Coeffs: []int64_t{-1}, + Coeffs: []int64{-1}, }.Build(), cmpb.LinearExpressionProto_builder{ Vars: []int32{int32_t(iv3.Index())}, - Coeffs: []int64_t{-1}, + Coeffs: []int64{-1}, }.Build(), }, }.Build(), @@ -1196,16 +1196,16 @@ func TestCpModelBuilder_Constraints(t *testing.T) { LinMax: cmpb.LinearArgumentProto_builder{ Target: cmpb.LinearExpressionProto_builder{ Vars: []int32{int32_t(iv1.Index())}, - Coeffs: []int64_t{1}, + Coeffs: []int64{1}, }.Build(), Exprs: []*cmpb.LinearExpressionProto{ cmpb.LinearExpressionProto_builder{ Vars: []int32{int32_t(iv2.Index())}, - Coeffs: []int64_t{1}, + Coeffs: []int64{1}, }.Build(), cmpb.LinearExpressionProto_builder{ Vars: []int32{int32_t(iv3.Index())}, - Coeffs: []int64_t{1}, + Coeffs: []int64{1}, }.Build(), }, }.Build(), @@ -1222,16 +1222,16 @@ func TestCpModelBuilder_Constraints(t *testing.T) { IntProd: cmpb.LinearArgumentProto_builder{ Target: cmpb.LinearExpressionProto_builder{ Vars: []int32{int32_t(iv1.Index())}, - Coeffs: []int64_t{1}, + Coeffs: []int64{1}, }.Build(), Exprs: []*cmpb.LinearExpressionProto{ cmpb.LinearExpressionProto_builder{ Vars: []int32{int32_t(iv2.Index())}, - Coeffs: []int64_t{1}, + Coeffs: []int64{1}, }.Build(), cmpb.LinearExpressionProto_builder{ Vars: []int32{int32_t(iv3.Index())}, - Coeffs: []int64_t{1}, + Coeffs: []int64{1}, }.Build(), }, }.Build(), @@ -1248,16 +1248,16 @@ func TestCpModelBuilder_Constraints(t *testing.T) { IntDiv: cmpb.LinearArgumentProto_builder{ Target: cmpb.LinearExpressionProto_builder{ Vars: []int32{int32_t(iv1.Index())}, - Coeffs: []int64_t{1}, + Coeffs: []int64{1}, }.Build(), Exprs: []*cmpb.LinearExpressionProto{ cmpb.LinearExpressionProto_builder{ Vars: []int32{int32_t(iv2.Index())}, - Coeffs: []int64_t{1}, + Coeffs: []int64{1}, }.Build(), cmpb.LinearExpressionProto_builder{ Vars: []int32{int32_t(iv3.Index())}, - Coeffs: []int64_t{1}, + Coeffs: []int64{1}, }.Build(), }, }.Build(), @@ -1274,16 +1274,16 @@ func TestCpModelBuilder_Constraints(t *testing.T) { LinMax: cmpb.LinearArgumentProto_builder{ Target: cmpb.LinearExpressionProto_builder{ Vars: []int32{int32_t(iv1.Index())}, - Coeffs: []int64_t{1}, + Coeffs: []int64{1}, }.Build(), Exprs: []*cmpb.LinearExpressionProto{ cmpb.LinearExpressionProto_builder{ Vars: []int32{int32_t(iv2.Index())}, - Coeffs: []int64_t{1}, + Coeffs: []int64{1}, }.Build(), cmpb.LinearExpressionProto_builder{ Vars: []int32{int32_t(iv2.Index())}, - Coeffs: []int64_t{-1}, + Coeffs: []int64{-1}, }.Build(), }, }.Build(), @@ -1300,16 +1300,16 @@ func TestCpModelBuilder_Constraints(t *testing.T) { IntMod: cmpb.LinearArgumentProto_builder{ Target: cmpb.LinearExpressionProto_builder{ Vars: []int32{int32_t(iv1.Index())}, - Coeffs: []int64_t{1}, + Coeffs: []int64{1}, }.Build(), Exprs: []*cmpb.LinearExpressionProto{ cmpb.LinearExpressionProto_builder{ Vars: []int32{int32_t(iv2.Index())}, - Coeffs: []int64_t{1}, + Coeffs: []int64{1}, }.Build(), cmpb.LinearExpressionProto_builder{ Vars: []int32{int32_t(iv3.Index())}, - Coeffs: []int64_t{1}, + Coeffs: []int64{1}, }.Build(), }, }.Build(), @@ -1388,7 +1388,7 @@ func TestCpModelBuilder_Constraints(t *testing.T) { want: cmpb.ConstraintProto_builder{ Table: cmpb.TableConstraintProto_builder{ Vars: []int32{int32_t(iv1.Index()), int32_t(iv2.Index())}, - Values: []int64_t{0, 2, 1, 3}, + Values: []int64{0, 2, 1, 3}, }.Build(), }.Build(), }, @@ -1407,7 +1407,7 @@ func TestCpModelBuilder_Constraints(t *testing.T) { TimeExprs: []*cmpb.LinearExpressionProto{ cmpb.LinearExpressionProto_builder{ Vars: []int32{int32_t(iv1.Index())}, - Coeffs: []int64_t{2}, + Coeffs: []int64{2}, }.Build(), }, LevelChanges: []*cmpb.LinearExpressionProto{ @@ -1422,7 +1422,7 @@ func TestCpModelBuilder_Constraints(t *testing.T) { { name: "AddAutomaton", constraint: func() *cmpb.ConstraintProto { - c := model.AddAutomaton([]IntVar{iv1, iv2}, 0, []int64_t{5, 10}) + c := model.AddAutomaton([]IntVar{iv1, iv2}, 0, []int64{5, 10}) c.AddTransition(0, 1, 10) c.AddTransition(2, 3, 15) m := mustModel(t, model) @@ -1432,10 +1432,10 @@ func TestCpModelBuilder_Constraints(t *testing.T) { Automaton: cmpb.AutomatonConstraintProto_builder{ Vars: []int32{int32_t(iv1.Index()), int32_t(iv2.Index())}, StartingState: 0, - FinalStates: []int64_t{5, 10}, - TransitionTail: []int64_t{0, 2}, - TransitionHead: []int64_t{1, 3}, - TransitionLabel: []int64_t{10, 15}, + FinalStates: []int64{5, 10}, + TransitionTail: []int64{0, 2}, + TransitionHead: []int64{1, 3}, + TransitionLabel: []int64{10, 15}, }.Build(), }.Build(), }, @@ -1451,13 +1451,13 @@ func TestCpModelBuilder_Constraints(t *testing.T) { Cumulative: cmpb.CumulativeConstraintProto_builder{ Capacity: cmpb.LinearExpressionProto_builder{ Vars: []int32{int32_t(iv1.Index())}, - Coeffs: []int64_t{1}, + Coeffs: []int64{1}, }.Build(), Intervals: []int32{int32_t(interval1.Index())}, Demands: []*cmpb.LinearExpressionProto{ cmpb.LinearExpressionProto_builder{ Vars: []int32{int32_t(iv2.Index())}, - Coeffs: []int64_t{1}, + Coeffs: []int64{1}, }.Build(), }, }.Build(), @@ -1486,7 +1486,7 @@ func TestCpModelBuilder_Minimize(t *testing.T) { m := mustModel(t, model) want := cmpb.CpObjectiveProto_builder{ Vars: []int32{int32_t(iv1.Index()), int32_t(iv2.Index())}, - Coeffs: []int64_t{3, 5}, + Coeffs: []int64{3, 5}, }.Build() got := m.GetObjective() @@ -1504,7 +1504,7 @@ func TestCpModelBuilder_Maximize(t *testing.T) { model.Maximize(NewLinearExpr().AddTerm(iv1, 3).AddTerm(iv2, 5).AddConstant(7)) want := cmpb.CpObjectiveProto_builder{ Vars: []int32{int32_t(iv1.Index()), int32_t(iv2.Index())}, - Coeffs: []int64_t{-3, -5}, + Coeffs: []int64{-3, -5}, ScalingFactor: -1.0, Offset: -7, }.Build() @@ -1562,12 +1562,12 @@ func TestCpModelBuilder_ConstantVars(t *testing.T) { func TestCpModelBuilder_IndexValueSlices(t *testing.T) { indices := []int32{5, 1, 3} - values := []int64_t{10, 11, 8} + values := []int64{10, 11, 8} sort.Sort(indexValueSlices{indices, values}) wantIndices := []int32{1, 3, 5} - wantValues := []int64_t{11, 8, 10} + wantValues := []int64{11, 8, 10} if diff := cmp.Diff(wantIndices, indices); diff != "" { t.Errorf("Sort indexValueSlices return unexpected indices diff (-want+got): %v", diff) @@ -1584,7 +1584,7 @@ func TestCpModelBuilder_SetHint(t *testing.T) { bv1 := model.NewBoolVar() bv2 := model.NewBoolVar() hint := &Hint{ - Ints: map[IntVar]int64_t{iv: 7}, + Ints: map[IntVar]int64{iv: 7}, Bools: map[BoolVar]bool{bv2.Not(): false, bv1: true}, } model.SetHint(hint) @@ -1593,7 +1593,7 @@ func TestCpModelBuilder_SetHint(t *testing.T) { got := m.GetSolutionHint() want := cmpb.PartialVariableAssignment_builder{ Vars: []int32{int32_t(iv.Index()), int32_t(bv1.Index()), int32_t(bv2.Index())}, - Values: []int64_t{7, 1, 1}, + Values: []int64{7, 1, 1}, }.Build() if diff := cmp.Diff(want, got, protocmp.Transform()); diff != "" { @@ -1608,7 +1608,7 @@ func TestCpModelBuilder_ClearHint(t *testing.T) { bv1 := model.NewBoolVar() bv2 := model.NewBoolVar() hint := &Hint{ - Ints: map[IntVar]int64_t{iv: 7}, + Ints: map[IntVar]int64{iv: 7}, Bools: map[BoolVar]bool{bv1: true, bv2.Not(): false}, } model.SetHint(hint) @@ -1759,7 +1759,7 @@ func TestCpModelBuilder_ErrorHandling(t *testing.T) { builder: func() *Builder { model1 := NewCpModelBuilder() model2 := NewCpModelBuilder() - model1.AddAutomaton([]IntVar{model2.NewIntVar(0, 10)}, 0, []int64_t{10}) + model1.AddAutomaton([]IntVar{model2.NewIntVar(0, 10)}, 0, []int64{10}) return model1 }, }, diff --git a/ortools/sat/go/domain.go b/ortools/sat/go/domain.go index f466f05df4..901e42614a 100644 --- a/ortools/sat/go/domain.go +++ b/ortools/sat/go/domain.go @@ -116,7 +116,7 @@ func NewDomain(left, right int64_t) Domain { // FromValues creates a new domain from `values`. `values` need not be // sorted and can repeat. -func FromValues(values []int64_t) Domain { +func FromValues(values []int64) Domain { var d Domain for _, v := range values { d.intervals = append(d.intervals, ClosedInterval{v, v}) @@ -138,7 +138,7 @@ func FromIntervals(intervals []ClosedInterval) Domain { // FromFlatIntervals creates a new domain from a flattened list of intervals. If there is an // interval where the start is greater than the end, the interval is considered empty. Returns // an error if the length of `values` is not even. -func FromFlatIntervals(values []int64_t) (Domain, error) { +func FromFlatIntervals(values []int64) (Domain, error) { if len(values) == 0 { return NewEmptyDomain(), nil } @@ -156,7 +156,7 @@ func FromFlatIntervals(values []int64_t) (Domain, error) { // FlattenedIntervals returns the flattened list of interval bounds of the domain. // For example, if Domain d is equal to `[0,2][5,5][9,10]` will return `[0,2,5,5,9,10]`. -func (d Domain) FlattenedIntervals() []int64_t { +func (d Domain) FlattenedIntervals() []int64 { var result []int64 for _, i := range d.intervals { result = append(result, i.Start, i.End) diff --git a/ortools/sat/go/domain_test.go b/ortools/sat/go/domain_test.go index 89bb4367d6..bfe0b13b97 100644 --- a/ortools/sat/go/domain_test.go +++ b/ortools/sat/go/domain_test.go @@ -71,23 +71,23 @@ func TestDomain_FromValues(t *testing.T) { want Domain }{ { - values: []int64_t{}, + values: []int64{}, want: Domain{}, }, { - values: []int64_t{4}, + values: []int64{4}, want: Domain{[]ClosedInterval{{4, 4}}}, }, { - values: []int64_t{1, 1, 3, 1, 2, 3, 2, 3}, + values: []int64{1, 1, 3, 1, 2, 3, 2, 3}, want: Domain{[]ClosedInterval{{1, 3}}}, }, { - values: []int64_t{1, 2, 3, 7, 8, -4}, + values: []int64{1, 2, 3, 7, 8, -4}, want: Domain{[]ClosedInterval{{-4, -4}, {1, 3}, {7, 8}}}, }, { - values: []int64_t{1, 2, 3, 5, 4, 6, 10, 12, 11, 15, 8}, + values: []int64{1, 2, 3, 5, 4, 6, 10, 12, 11, 15, 8}, want: Domain{[]ClosedInterval{{1, 6}, {8, 8}, {10, 12}, {15, 15}}}, }, } @@ -142,27 +142,27 @@ func TestDomain_FromFlatIntervals(t *testing.T) { wantError string }{ { - flatIntervals: []int64_t{}, + flatIntervals: []int64{}, wantDomain: Domain{}, }, { - flatIntervals: []int64_t{1}, + flatIntervals: []int64{1}, wantError: "must be a multiple of 2", }, { - flatIntervals: []int64_t{-1, 1, 3, 3, 5, 10}, + flatIntervals: []int64{-1, 1, 3, 3, 5, 10}, wantDomain: Domain{[]ClosedInterval{{-1, 1}, {3, 3}, {5, 10}}}, }, { - flatIntervals: []int64_t{3, 9, 6, 10}, + flatIntervals: []int64{3, 9, 6, 10}, wantDomain: Domain{[]ClosedInterval{{3, 10}}}, }, { - flatIntervals: []int64_t{3, 5, 5, 10}, + flatIntervals: []int64{3, 5, 5, 10}, wantDomain: Domain{[]ClosedInterval{{3, 10}}}, }, { - flatIntervals: []int64_t{5, 3, 4, -1}, + flatIntervals: []int64{5, 3, 4, -1}, wantDomain: Domain{}, }, } @@ -182,7 +182,7 @@ func TestDomain_FlattenedIntervals(t *testing.T) { d := Domain{[]ClosedInterval{{-1, 1}, {3, 3}, {5, 10}}} got := d.FlattenedIntervals() - want := []int64_t{-1, 1, 3, 3, 5, 10} + want := []int64{-1, 1, 3, 3, 5, 10} if diff := cmp.Diff(want, got); diff != "" { t.Errorf("FlattenedIntervals() returned with unexpected diff (-want+got);\n%s", diff) } diff --git a/ortools/sat/integer.cc b/ortools/sat/integer.cc index bb0fe330fc..c1707af415 100644 --- a/ortools/sat/integer.cc +++ b/ortools/sat/integer.cc @@ -197,20 +197,29 @@ void IntegerEncoder::AddImplications( if (!add_implications_) return; DCHECK_EQ(it->second, associated_lit); - // Literal(after) => associated_lit - auto after_it = it; - ++after_it; - if (after_it != map.end()) { - sat_solver_->AddClauseDuringSearch( - {after_it->second.Negated(), associated_lit}); - } - - // associated_lit => Literal(before) + // Tricky: We compute the literal first because AddClauseDuringSearch() might + // propagate at level zero and mess up the map. + LiteralIndex before_index = kNoLiteralIndex; if (it != map.begin()) { auto before_it = it; --before_it; + before_index = before_it->second.Index(); + } + LiteralIndex after_index = kNoLiteralIndex; + { + auto after_it = it; + ++after_it; + if (after_it != map.end()) after_index = after_it->second.Index(); + } + + // Then we add the two implications. + if (after_index != kNoLiteralIndex) { sat_solver_->AddClauseDuringSearch( - {associated_lit.Negated(), before_it->second}); + {Literal(after_index).Negated(), associated_lit}); + } + if (before_index != kNoLiteralIndex) { + sat_solver_->AddClauseDuringSearch( + {associated_lit.Negated(), Literal(before_index)}); } } @@ -2123,7 +2132,8 @@ bool GenericLiteralWatcher::Propagate(Trail* trail) { // // TODO(user): The queue will not be emptied, but I am not sure the solver // will be left in an usable state. Fix if it become needed to resume - // the solve from the last time it was interrupted. + // the solve from the last time it was interrupted. In particular, we might + // want to call UpdateCallingNeeds()? if (test_limit > 100) { test_limit = 0; if (time_limit_->LimitReached()) break; @@ -2234,8 +2244,12 @@ bool GenericLiteralWatcher::Propagate(Trail* trail) { void GenericLiteralWatcher::Untrail(const Trail& trail, int trail_index) { if (propagation_trail_index_ <= trail_index) { // Nothing to do since we found a conflict before Propagate() was called. - CHECK_EQ(propagation_trail_index_, trail_index) - << " level " << trail.CurrentDecisionLevel(); + if (DEBUG_MODE) { + // The assumption is not always true if we are currently aborting. + if (time_limit_->LimitReached()) return; + CHECK_EQ(propagation_trail_index_, trail_index) + << " level " << trail.CurrentDecisionLevel(); + } return; } diff --git a/ortools/sat/integer.h b/ortools/sat/integer.h index a4629893bd..42f0968268 100644 --- a/ortools/sat/integer.h +++ b/ortools/sat/integer.h @@ -300,9 +300,9 @@ struct AffineExpression { AffineExpression(IntegerVariable v) // NOLINT(runtime/explicit) : var(v), coeff(1) {} AffineExpression(IntegerVariable v, IntegerValue c) - : var(c > 0 ? v : NegationOf(v)), coeff(IntTypeAbs(c)) {} + : var(c >= 0 ? v : NegationOf(v)), coeff(IntTypeAbs(c)) {} AffineExpression(IntegerVariable v, IntegerValue c, IntegerValue cst) - : var(c > 0 ? v : NegationOf(v)), coeff(IntTypeAbs(c)), constant(cst) {} + : var(c >= 0 ? v : NegationOf(v)), coeff(IntTypeAbs(c)), constant(cst) {} // Returns the integer literal corresponding to expression >= value or // expression <= value. diff --git a/ortools/sat/lb_tree_search.cc b/ortools/sat/lb_tree_search.cc index 7d7e69db45..d7b127ddb9 100644 --- a/ortools/sat/lb_tree_search.cc +++ b/ortools/sat/lb_tree_search.cc @@ -47,7 +47,8 @@ namespace operations_research { namespace sat { LbTreeSearch::LbTreeSearch(Model* model) - : time_limit_(model->GetOrCreate()), + : name_(model->Name()), + time_limit_(model->GetOrCreate()), random_(model->GetOrCreate()), sat_solver_(model->GetOrCreate()), integer_encoder_(model->GetOrCreate()), @@ -298,8 +299,8 @@ SatSolver::Status LbTreeSearch::Search( const IntegerValue bound = nodes_[current_branch_[0]].MinObjective(); if (bound > current_objective_lb_) { shared_response_->UpdateInnerObjectiveBounds( - absl::StrCat("lb_tree_search (", SmallProgressString(), ") "), - bound, integer_trail_->LevelZeroUpperBound(objective_var_)); + absl::StrCat(name_, " (", SmallProgressString(), ") "), bound, + integer_trail_->LevelZeroUpperBound(objective_var_)); current_objective_lb_ = bound; if (VLOG_IS_ON(3)) DebugDisplayTree(current_branch_[0]); } diff --git a/ortools/sat/lb_tree_search.h b/ortools/sat/lb_tree_search.h index 8a72301aeb..60d7779b5b 100644 --- a/ortools/sat/lb_tree_search.h +++ b/ortools/sat/lb_tree_search.h @@ -138,6 +138,7 @@ class LbTreeSearch { std::string SmallProgressString() const; // Model singleton class used here. + const std::string name_; TimeLimit* time_limit_; ModelRandomGenerator* random_; SatSolver* sat_solver_; diff --git a/ortools/sat/linear_constraint.h b/ortools/sat/linear_constraint.h index f385e2d670..8b343343cb 100644 --- a/ortools/sat/linear_constraint.h +++ b/ortools/sat/linear_constraint.h @@ -15,6 +15,7 @@ #define OR_TOOLS_SAT_LINEAR_CONSTRAINT_H_ #include +#include #include #include #include diff --git a/ortools/sat/linear_programming_constraint.cc b/ortools/sat/linear_programming_constraint.cc index 42bb314e22..18a810cdc9 100644 --- a/ortools/sat/linear_programming_constraint.cc +++ b/ortools/sat/linear_programming_constraint.cc @@ -693,7 +693,9 @@ bool LinearProgrammingConstraint::SolveLp() { << " lvl:" << trail_->CurrentDecisionLevel() << " " << simplex_.GetProblemStatus() << " iter:" << simplex_.GetNumberOfIterations() - << " obj:" << simplex_.GetObjectiveValue(); + << " obj:" << simplex_.GetObjectiveValue() << " scaled:" + << objective_definition_->ScaleObjective( + simplex_.GetObjectiveValue()); if (simplex_.GetProblemStatus() == glop::ProblemStatus::OPTIMAL) { lp_solution_is_set_ = true; diff --git a/ortools/sat/linear_programming_constraint.h b/ortools/sat/linear_programming_constraint.h index e3dd67785a..125d3ca856 100644 --- a/ortools/sat/linear_programming_constraint.h +++ b/ortools/sat/linear_programming_constraint.h @@ -18,6 +18,7 @@ #include #include #include +#include #include #include #include diff --git a/ortools/sat/linear_propagation.cc b/ortools/sat/linear_propagation.cc index 87c5fc7f33..6d1e9a5151 100644 --- a/ortools/sat/linear_propagation.cc +++ b/ortools/sat/linear_propagation.cc @@ -23,6 +23,7 @@ #include #include +#include "absl/base/log_severity.h" #include "absl/container/flat_hash_map.h" #include "absl/container/inlined_vector.h" #include "absl/log/check.h" @@ -85,6 +86,20 @@ void CustomFifoQueue::Push(int id) { if (right_ == queue_.size()) right_ = 0; } +void CustomFifoQueue::FillAndSortTmpPositions(absl::Span elements) { + int index = 0; + const int capacity = queue_.size(); + for (const int id : elements) { + const int p = pos_[id]; + DCHECK_GE(p, 0); + DCHECK_EQ(queue_[p], id); + tmp_positions_[index++] = p >= left_ ? p : p + capacity; + } + std::sort(&tmp_positions_[0], &tmp_positions_[index]); + DCHECK(std::unique(&tmp_positions_[0], &tmp_positions_[index]) == + &tmp_positions_[index]); +} + void CustomFifoQueue::Reorder(absl::Span order) { if (order.size() <= 1) return; @@ -94,20 +109,12 @@ void CustomFifoQueue::Reorder(absl::Span order) { return ReorderDense(order); } - int index = 0; - for (const int id : order) { - const int p = pos_[id]; - DCHECK_GE(p, 0); - tmp_positions_[index++] = p >= left_ ? p : p + capacity; - } - std::sort(&tmp_positions_[0], &tmp_positions_[index]); - DCHECK(std::unique(&tmp_positions_[0], &tmp_positions_[index]) == - &tmp_positions_[index]); - - index = 0; - for (const int id : order) { - int p = tmp_positions_[index++]; + FillAndSortTmpPositions(order); + for (int i = 0; i < order.size(); ++i) { + int p = tmp_positions_[i]; if (p >= capacity) p -= capacity; + + const int id = order[i]; pos_[id] = p; queue_[p] = id; } @@ -144,20 +151,15 @@ void CustomFifoQueue::ReorderDense(absl::Span order) { DCHECK_EQ(order_index, order.size()); } +// TODO(user): combine this with reorder. +// This is slow, especially if we are dense. void CustomFifoQueue::SortByPos(absl::Span elements) { - std::sort(elements.begin(), elements.end(), - [this](const int id1, const int id2) { - const int p1 = pos_[id1]; - const int p2 = pos_[id2]; - if (p1 >= left_) { - if (p2 >= left_) return p1 < p2; - return true; - } else { - // p1 < left_. - if (p2 < left_) return p1 < p2; - return false; - } - }); + FillAndSortTmpPositions(elements); + const int capacity = queue_.size(); + for (int i = 0; i < elements.size(); ++i) { + const int p = tmp_positions_[i]; + elements[i] = queue_[p < capacity ? p : p - capacity]; + } } std::ostream& operator<<(std::ostream& os, const EnforcementStatus& e) { @@ -538,8 +540,12 @@ bool LinearPropagator::Propagate() { for (const IntegerVariable var : modified_vars_.PositionsSetAtLeastOnce()) { if (var >= var_to_constraint_ids_.size()) continue; SetPropagatedBy(var, -1); - AddWatchedToQueue(var); + AddWatchedToQueue(var, /*push_delayed_right_away=*/false); } + for (const int id : tmp_delayed_) { + AddToQueueIfNeeded(id); + } + tmp_delayed_.clear(); // We abort this propagator as soon as a Boolean is propagated, so that we // always finish the Boolean propagation first. This can happen when we push a @@ -549,13 +555,35 @@ bool LinearPropagator::Propagate() { // propagator might have pushed the same variable further. // // Empty FIFO queue. + // + // TODO(user): More than the propagation speed, I think it is important to + // have proper explanation, so if A pushes B, but later on the queue we have C + // that push A that push B again, that might be bad? We can try to avoid this + // even further, by organizing the queue in passes: + // - Scan all relevant constraints, remember who pushes but DO NOT push yet! + // - If no cycle, do not pushes constraint whose slack will changes due to + // other pushes. + // - consider the new constraint that need to be scanned and repeat. + // I think it is okay to scan twice the constraints that push something in + // order to get better explanation. We tend to diverge from the class shortest + // path algo in this regard. + // + // TODO(user): If we push the idea further, can we first compute the fix point + // without pushing anything, then compute a good order of constraints for the + // explanations? what is tricky is that we might need to "scan" more than once + // a constraint I think. ex: Y, Z, T >=0 + // - 2 * Y + Z + T <= 11 ==> Y <= 5, Z <= 11, T <= 11 (1) + // - Z + Y >= 6 ==> Z >= 1 + // - (1) again to push T <= 10 and reach the propagation fixed point. + bool result = true; + num_terms_for_dtime_update_ = 0; const int saved_index = trail_->Index(); while (!propagation_queue_.empty()) { const int id = propagation_queue_.Pop(); in_queue_[id] = false; if (!PropagateOneConstraint(id)) { - modified_vars_.ClearAndResize(integer_trail_->NumIntegerVariables()); - return false; + result = false; + break; } if (trail_->Index() > saved_index) { @@ -565,8 +593,10 @@ bool LinearPropagator::Propagate() { } // Clean-up modified_vars_ to do as little as possible on the next call. + time_limit_->AdvanceDeterministicTime( + static_cast(num_terms_for_dtime_update_) * 1e-9); modified_vars_.ClearAndResize(integer_trail_->NumIntegerVariables()); - return true; + return result; } // Adds a new constraint to the propagator. @@ -603,6 +633,7 @@ bool LinearPropagator::AddConstraint( } id_to_propagation_count_.push_back(0); + id_propagated_something_.push_back(false); variables_buffer_.insert(variables_buffer_.end(), vars.begin(), vars.end()); coeffs_buffer_.insert(coeffs_buffer_.end(), coeffs.begin(), coeffs.end()); CanonicalizeConstraint(id); @@ -671,7 +702,12 @@ bool LinearPropagator::AddConstraint( } // Propagate this new constraint. - return PropagateOneConstraint(id); + // TODO(user): Do we want to do that? + num_terms_for_dtime_update_ = 0; + const bool result = PropagateOneConstraint(id); + time_limit_->AdvanceDeterministicTime( + static_cast(num_terms_for_dtime_update_) * 1e-9); + return result; } absl::Span LinearPropagator::GetCoeffs( @@ -689,8 +725,8 @@ absl::Span LinearPropagator::GetVariables( void LinearPropagator::CanonicalizeConstraint(int id) { const ConstraintInfo& info = infos_[id]; - auto coeffs = GetCoeffs(info); - auto vars = GetVariables(info); + const auto coeffs = GetCoeffs(info); + const auto vars = GetVariables(info); for (int i = 0; i < vars.size(); ++i) { if (coeffs[i] < 0) { coeffs[i] = -coeffs[i]; @@ -705,17 +741,34 @@ bool LinearPropagator::PropagateOneConstraint(int id) { // default though, even VLOG_IS_ON(1) so we disable it. if (/* DISABLES CODE */ (false)) { ++num_scanned_; - if (id_scanned_at_least_once_[id]) { - ++num_extra_scans_; - } else { - id_scanned_at_least_once_.Set(id); + if (id < id_scanned_at_least_once_.size()) { + if (id_scanned_at_least_once_[id]) { + ++num_extra_scans_; + } else { + id_scanned_at_least_once_.Set(id); + } } } // Skip constraint not enforced or that cannot propagate if false. ConstraintInfo& info = infos_[id]; const EnforcementStatus enf_status = EnforcementStatus(info.enf_status); - DCHECK_EQ(enf_status, enforcement_propagator_->DebugStatus(info.enf_id)); + if (DEBUG_MODE) { + const EnforcementStatus debug_status = + enforcement_propagator_->DebugStatus(info.enf_id); + if (enf_status != debug_status) { + if (enf_status == EnforcementStatus::CANNOT_PROPAGATE && + debug_status == EnforcementStatus::IS_FALSE) { + // This case might happen because in our two watched literals scheme, + // we might watch two unassigned literal without knowing another one is + // already false. + } else { + LOG(FATAL) << "Enforcement status not up to date: " << enf_status + << " vs debug: " << debug_status; + } + } + } + if (enf_status == EnforcementStatus::IS_FALSE || enf_status == EnforcementStatus::CANNOT_PROPAGATE) { DCHECK(!in_queue_[id]); @@ -732,44 +785,72 @@ bool LinearPropagator::PropagateOneConstraint(int id) { // Compute the slack and max_variations_ of each variables. // We also filter out fixed variables in a reversible way. IntegerValue implied_lb(0); - auto vars = GetVariables(info); - auto coeffs = GetCoeffs(info); + const auto vars = GetVariables(info); IntegerValue max_variation(0); bool first_change = true; - time_limit_->AdvanceDeterministicTime(static_cast(info.rev_size) * - 1e-9); - for (int i = 0; i < info.rev_size;) { - const IntegerVariable var = vars[i]; - const IntegerValue coeff = coeffs[i]; - const IntegerValue lb = integer_trail_->LowerBound(var); - const IntegerValue ub = integer_trail_->UpperBound(var); - if (lb == ub) { - if (first_change) { - // Note that we can save at most one state per fixed var. Also at - // level zero we don't save anything. - rev_int_repository_->SaveState(&info.rev_size); - rev_integer_value_repository_->SaveState(&info.rev_rhs); - first_change = false; + num_terms_for_dtime_update_ += info.rev_size; + IntegerValue* max_variations = max_variations_.data(); + if (info.all_coeffs_are_one) { + // TODO(user): Avoid duplication? + for (int i = 0; i < info.rev_size;) { + const IntegerVariable var = vars[i]; + const IntegerValue lb = integer_trail_->LowerBound(var); + const IntegerValue ub = integer_trail_->UpperBound(var); + if (lb == ub) { + if (first_change) { + // Note that we can save at most one state per fixed var. Also at + // level zero we don't save anything. + rev_int_repository_->SaveState(&info.rev_size); + rev_integer_value_repository_->SaveState(&info.rev_rhs); + first_change = false; + } + info.rev_size--; + std::swap(vars[i], vars[info.rev_size]); + info.rev_rhs -= lb; + } else { + implied_lb += lb; + max_variations[i] = (ub - lb); + max_variation = std::max(max_variation, max_variations[i]); + ++i; + } + } + } else { + const auto coeffs = GetCoeffs(info); + for (int i = 0; i < info.rev_size;) { + const IntegerVariable var = vars[i]; + const IntegerValue coeff = coeffs[i]; + const IntegerValue lb = integer_trail_->LowerBound(var); + const IntegerValue ub = integer_trail_->UpperBound(var); + if (lb == ub) { + if (first_change) { + // Note that we can save at most one state per fixed var. Also at + // level zero we don't save anything. + rev_int_repository_->SaveState(&info.rev_size); + rev_integer_value_repository_->SaveState(&info.rev_rhs); + first_change = false; + } + info.rev_size--; + std::swap(vars[i], vars[info.rev_size]); + std::swap(coeffs[i], coeffs[info.rev_size]); + info.rev_rhs -= coeff * lb; + } else { + implied_lb += coeff * lb; + max_variations[i] = (ub - lb) * coeff; + max_variation = std::max(max_variation, max_variations[i]); + ++i; } - info.rev_size--; - std::swap(vars[i], vars[info.rev_size]); - std::swap(coeffs[i], coeffs[info.rev_size]); - info.rev_rhs -= coeff * lb; - } else { - implied_lb += coeff * lb; - max_variations_[i] = (ub - lb) * coeff; - max_variation = std::max(max_variation, max_variations_[i]); - ++i; } } const IntegerValue slack = info.rev_rhs - implied_lb; // Negative slack means the constraint is false. if (max_variation <= slack) return true; + id_propagated_something_[id] = true; if (slack < 0) { // Fill integer reason. integer_reason_.clear(); reason_coeffs_.clear(); + const auto coeffs = GetCoeffs(info); for (int i = 0; i < info.initial_size; ++i) { const IntegerVariable var = vars[i]; if (!integer_trail_->VariableLowerBoundIsFromLevelZero(var)) { @@ -794,8 +875,9 @@ bool LinearPropagator::PropagateOneConstraint(int id) { // The lower bound of all the variables except one can be used to update the // upper bound of the last one. int num_pushed = 0; + const auto coeffs = GetCoeffs(info); for (int i = 0; i < info.rev_size; ++i) { - if (max_variations_[i] <= slack) continue; + if (max_variations[i] <= slack) continue; // TODO(user): If the new ub fall into an hole of the variable, we can // actually relax the reason more by computing a better slack. @@ -817,8 +899,8 @@ bool LinearPropagator::PropagateOneConstraint(int id) { literal_reason); reason_coeffs_.clear(); - auto coeffs = GetCoeffs(info); - auto vars = GetVariables(info); + const auto coeffs = GetCoeffs(info); + const auto vars = GetVariables(info); for (int i = 0; i < info.initial_size; ++i) { const IntegerVariable var = vars[i]; if (PositiveVariable(var) == PositiveVariable(i_lit.var)) { @@ -873,8 +955,8 @@ bool LinearPropagator::PropagateOneConstraint(int id) { std::string LinearPropagator::ConstraintDebugString(int id) { std::string result; const ConstraintInfo& info = infos_[id]; - auto coeffs = GetCoeffs(info); - auto vars = GetVariables(info); + const auto coeffs = GetCoeffs(info); + const auto vars = GetVariables(info); IntegerValue implied_lb(0); IntegerValue rhs_correction(0); for (int i = 0; i < info.initial_size; ++i) { @@ -908,8 +990,8 @@ bool LinearPropagator::ReportConflictingCycle() { const ConstraintInfo& info = infos_[id]; enforcement_propagator_->AddEnforcementReason(info.enf_id, &literal_reason_); - auto coeffs = GetCoeffs(info); - auto vars = GetVariables(info); + const auto coeffs = GetCoeffs(info); + const auto vars = GetVariables(info); IntegerValue rhs_correction(0); for (int i = 0; i < info.initial_size; ++i) { if (i >= info.rev_size) { @@ -1020,6 +1102,9 @@ bool LinearPropagator::ReportConflictingCycle() { // // TODO(user): If one of the var coeff is > previous slack we push an id again, // we can stop early with a conflict by propagating the ids in sequence. +// +// TODO(user): Revisit the algo, no point exploring twice the same var, also +// the queue reordering heuristic might not be the best. bool LinearPropagator::DisassembleSubtree(int root_id, int num_pushed) { disassemble_to_reorder_.ClearAndResize(in_queue_.size()); disassemble_reverse_topo_order_.clear(); @@ -1033,7 +1118,7 @@ bool LinearPropagator::DisassembleSubtree(int root_id, int num_pushed) { disassemble_branch_.clear(); { const ConstraintInfo& info = infos_[root_id]; - auto vars = GetVariables(info); + const auto vars = GetVariables(info); for (int i = 0; i < num_pushed; ++i) { disassemble_queue_.push_back({root_id, NegationOf(vars[i])}); } @@ -1041,6 +1126,7 @@ bool LinearPropagator::DisassembleSubtree(int root_id, int num_pushed) { // Note that all var should be unique since there is only one propagated_by_ // for each one. And each time we explore an id, we disassemble the tree. + absl::Span id_to_count = absl::MakeSpan(id_to_propagation_count_); while (!disassemble_queue_.empty()) { const auto [prev_id, var] = disassemble_queue_.back(); if (!disassemble_branch_.empty() && @@ -1053,16 +1139,11 @@ bool LinearPropagator::DisassembleSubtree(int root_id, int num_pushed) { } disassemble_branch_.push_back({prev_id, var}); + time_limit_->AdvanceDeterministicTime( static_cast(var_to_constraint_ids_[var].size()) * 1e-9); for (const int id : var_to_constraint_ids_[var]) { - if (prev_id == root_id) { - // Root id was just propagated, so there is no need to reorder what - // it pushes. - DCHECK_NE(id, root_id); - if (disassemble_to_reorder_[id]) continue; - disassemble_to_reorder_.Set(id); - } else if (id == root_id) { + if (id == root_id) { // TODO(user): Check previous slack vs var coeff? // TODO(user): Make sure there are none or detect cycle not going back // to the root. @@ -1081,16 +1162,16 @@ bool LinearPropagator::DisassembleSubtree(int root_id, int num_pushed) { // variation in slack might be big enough to push a variable twice and // thus push a lower coeff. const ConstraintInfo& info = infos_[id]; - auto coeffs = GetCoeffs(info); - auto vars = GetVariables(info); + const auto coeffs = GetCoeffs(info); + const auto vars = GetVariables(info); IntegerValue root_coeff(0); IntegerValue var_coeff(0); for (int i = 0; i < info.initial_size; ++i) { if (vars[i] == var) var_coeff = coeffs[i]; if (vars[i] == NegationOf(root_var)) root_coeff = coeffs[i]; } - CHECK_NE(root_coeff, 0); - CHECK_NE(var_coeff, 0); + DCHECK_NE(root_coeff, 0); + DCHECK_NE(var_coeff, 0); if (var_coeff >= root_coeff) { return ReportConflictingCycle(); } else { @@ -1099,15 +1180,15 @@ bool LinearPropagator::DisassembleSubtree(int root_id, int num_pushed) { } } - if (id_to_propagation_count_[id] == 0) continue; // Didn't push. disassemble_to_reorder_.Set(id); + if (id_to_count[id] == 0) continue; // Didn't push or was desassembled. // The constraint pushed some variable. Identify which ones will be pushed // further. Disassemble the whole info since we are about to propagate // this constraint again. Any pushed variable must be before the rev_size. const ConstraintInfo& info = infos_[id]; - auto coeffs = GetCoeffs(info); - auto vars = GetVariables(info); + const auto coeffs = GetCoeffs(info); + const auto vars = GetVariables(info); IntegerValue var_coeff(0); disassemble_candidates_.clear(); ++num_explored_in_disassemble_; @@ -1124,7 +1205,7 @@ bool LinearPropagator::DisassembleSubtree(int root_id, int num_pushed) { // We will propagate var again later, so clear all this for now. propagated_by_[next_var] = -1; - id_to_propagation_count_[id]--; + id_to_count[id]--; } } for (const auto [next_var, coeff] : disassemble_candidates_) { @@ -1152,7 +1233,7 @@ bool LinearPropagator::DisassembleSubtree(int root_id, int num_pushed) { tmp_to_reorder_.push_back(id); } - // TODO(user): Reordering can be sloe since require sort and can touch many + // TODO(user): Reordering can be slow since require sort and can touch many // entries. Investigate alternatives. We could probably optimize this a bit // more. if (tmp_to_reorder_.empty()) return true; @@ -1188,12 +1269,28 @@ void LinearPropagator::AddToQueueIfNeeded(int id) { propagation_queue_.Push(id); } -void LinearPropagator::AddWatchedToQueue(IntegerVariable var) { +void LinearPropagator::AddWatchedToQueue(IntegerVariable var, + bool push_delayed_right_away) { if (var >= static_cast(var_to_constraint_ids_.size())) return; time_limit_->AdvanceDeterministicTime( static_cast(var_to_constraint_ids_[var].size()) * 1e-9); + + // If a constraint propagated something and is getting tighter, then it + // will likely propagate again, and we want to propagate it first. for (const int id : var_to_constraint_ids_[var]) { - AddToQueueIfNeeded(id); + if (in_queue_[id]) continue; + if (true || id_propagated_something_[id]) { + id_propagated_something_[id] = false; // reset. + AddToQueueIfNeeded(id); + } else { + tmp_delayed_.push_back(id); + } + } + if (push_delayed_right_away) { + for (const int id : tmp_delayed_) { + AddToQueueIfNeeded(id); + } + tmp_delayed_.clear(); } } diff --git a/ortools/sat/linear_propagation.h b/ortools/sat/linear_propagation.h index 17d7aa6e08..72757ab68d 100644 --- a/ortools/sat/linear_propagation.h +++ b/ortools/sat/linear_propagation.h @@ -66,6 +66,8 @@ class CustomFifoQueue { void SortByPos(absl::Span elements); private: + void FillAndSortTmpPositions(absl::Span elements); + // The queue is stored in [left_, right_) with eventual wrap around % size. // The positions of each element is in pos_[element] and never changes during // normal operation. A position of -1 means that the element is not in the @@ -226,7 +228,8 @@ class LinearPropagator : public PropagatorInterface, ReversibleInterface { void ClearPropagatedBy(); void CanonicalizeConstraint(int id); void AddToQueueIfNeeded(int id); - void AddWatchedToQueue(IntegerVariable var); + void AddWatchedToQueue(IntegerVariable var, + bool push_delayed_right_away = true); void SetPropagatedBy(IntegerVariable var, int id); std::string ConstraintDebugString(int id); @@ -254,9 +257,6 @@ class LinearPropagator : public PropagatorInterface, ReversibleInterface { std::deque infos_; // Buffer of the constraints data. - // - // TODO(user): A lot of constrains have all their coeffs at one, we could - // exploit this. std::vector variables_buffer_; std::vector coeffs_buffer_; std::vector buffer_of_ones_; @@ -302,6 +302,10 @@ class LinearPropagator : public PropagatorInterface, ReversibleInterface { SparseBitset disassemble_to_reorder_; std::vector disassemble_reverse_topo_order_; + // Heuristic to enqueue interesting constraint first. + std::vector id_propagated_something_; + std::vector tmp_delayed_; + // Staging queue. // Initially, we add the constraint to the priority queue, and we extract // them one by one, each time reaching the propagation fixed point. @@ -315,6 +319,9 @@ class LinearPropagator : public PropagatorInterface, ReversibleInterface { SparseBitset id_scanned_at_least_once_; int64_t num_extra_scans_ = 0; + // This is used to update the deterministic time. + int64_t num_terms_for_dtime_update_ = 0; + // Stats. int64_t num_pushes_ = 0; int64_t num_enforcement_pushes_ = 0; diff --git a/ortools/sat/lp_utils.cc b/ortools/sat/lp_utils.cc index 1a5a1629ea..0e1d7c827c 100644 --- a/ortools/sat/lp_utils.cc +++ b/ortools/sat/lp_utils.cc @@ -733,6 +733,7 @@ struct ConstraintScaler { const MPConstraintProto& mp_constraint, CpModelProto* cp_model); + bool keep_names = false; double max_relative_coeff_error = 0.0; double max_absolute_rhs_error = 0.0; double max_scaling_factor = 0.0; @@ -755,7 +756,7 @@ ConstraintProto* ConstraintScaler::AddConstraint( } auto* constraint = cp_model->add_constraints(); - constraint->set_name(mp_constraint.name()); + if (keep_names) constraint->set_name(mp_constraint.name()); auto* arg = constraint->mutable_linear(); // First scale the coefficients of the constraints so that the constraint @@ -959,10 +960,11 @@ bool ConvertMPModelProtoToCpModelProto(const SatParameters& params, // Add the variables. const int num_variables = mp_model.variable_size(); + const bool keep_names = !params.ignore_names(); for (int i = 0; i < num_variables; ++i) { const MPVariableProto& mp_var = mp_model.variable(i); IntegerVariableProto* cp_var = cp_model->add_variables(); - cp_var->set_name(mp_var.name()); + if (keep_names) cp_var->set_name(mp_var.name()); // Deal with the corner case of a domain far away from zero. // @@ -1024,6 +1026,7 @@ bool ConvertMPModelProtoToCpModelProto(const SatParameters& params, << params.mip_max_activity_exponent(); scaler.wanted_precision = kWantedPrecision; scaler.scaling_target = kScalingTarget; + scaler.keep_names = keep_names; // Add the constraints. We scale each of them individually. for (const MPConstraintProto& mp_constraint : mp_model.constraint()) { diff --git a/ortools/sat/optimization.cc b/ortools/sat/optimization.cc index 72f0eaace0..25e4db15b9 100644 --- a/ortools/sat/optimization.cc +++ b/ortools/sat/optimization.cc @@ -439,6 +439,7 @@ CoreBasedOptimizer::CoreBasedOptimizer( std::function feasible_solution_observer, Model* model) : parameters_(model->GetOrCreate()), sat_solver_(model->GetOrCreate()), + clauses_(model->GetOrCreate()), time_limit_(model->GetOrCreate()), implications_(model->GetOrCreate()), integer_trail_(model->GetOrCreate()), @@ -666,9 +667,8 @@ bool CoreBasedOptimizer::CoverOptimization() { } SatSolver::Status CoreBasedOptimizer::OptimizeWithSatEncoding( - const std::vector& literals, - const std::vector& vars, - const std::vector& coefficients, Coefficient offset) { + absl::Span literals, absl::Span vars, + absl::Span coefficients, Coefficient offset) { // Create one initial nodes per variables with cost. // TODO(user): We could create EncodingNode out of IntegerVariable. // @@ -758,9 +758,10 @@ SatSolver::Status CoreBasedOptimizer::OptimizeWithSatEncoding( const int num_bools = sat_solver_->NumVariables(); const int num_fixed = sat_solver_->NumFixedVariables(); model_->GetOrCreate()->UpdateInnerObjectiveBounds( - absl::StrFormat("bool_core (num_cores=%d [%s] a=%u d=%d fixed=%d/%d)", - iter, previous_core_info, encoder.nodes().size(), - max_depth, num_fixed, num_bools), + absl::StrFormat( + "bool_core (num_cores=%d [%s] a=%u d=%d fixed=%d/%d clauses=%s)", + iter, previous_core_info, encoder.nodes().size(), max_depth, + num_fixed, num_bools, FormatCounter(clauses_->num_clauses())), new_obj_lb, integer_trail_->LevelZeroUpperBound(objective_var_)); } diff --git a/ortools/sat/optimization.h b/ortools/sat/optimization.h index 5820783906..4482a3ebca 100644 --- a/ortools/sat/optimization.h +++ b/ortools/sat/optimization.h @@ -114,9 +114,9 @@ class CoreBasedOptimizer { // - Support resuming for interleaved search. // - Implement all core heurisitics. SatSolver::Status OptimizeWithSatEncoding( - const std::vector& literals, - const std::vector& vars, - const std::vector& coefficients, Coefficient offset); + absl::Span literals, + absl::Span vars, + absl::Span coefficients, Coefficient offset); private: CoreBasedOptimizer(const CoreBasedOptimizer&) = delete; @@ -168,6 +168,7 @@ class CoreBasedOptimizer { SatParameters* parameters_; SatSolver* sat_solver_; + ClauseManager* clauses_; TimeLimit* time_limit_; BinaryImplicationGraph* implications_; IntegerTrail* integer_trail_; diff --git a/ortools/sat/precedences.cc b/ortools/sat/precedences.cc index 291cf2fff4..50e01cf5ad 100644 --- a/ortools/sat/precedences.cc +++ b/ortools/sat/precedences.cc @@ -42,6 +42,7 @@ #include "ortools/sat/sat_solver.h" #include "ortools/sat/synchronization.h" #include "ortools/util/bitset.h" +#include "ortools/util/logging.h" #include "ortools/util/strong_integers.h" #include "ortools/util/time_limit.h" @@ -1021,112 +1022,174 @@ bool PrecedencesPropagator::BellmanFordTarjan(Trail* trail) { return true; } -int PrecedencesPropagator::AddGreaterThanAtLeastOneOfConstraintsFromClause( - const absl::Span clause, Model* model) { +void GreaterThanAtLeastOneOfDetector::Add(Literal lit, LinearTerm a, + LinearTerm b, IntegerValue lhs, + IntegerValue rhs) { + Relation r; + r.enforcement = lit; + r.a = a; + r.b = b; + r.lhs = lhs; + r.rhs = rhs; + + // We shall only consider positive variable here. + if (r.a.var != kNoIntegerVariable && !VariableIsPositive(r.a.var)) { + r.a.var = NegationOf(r.a.var); + r.a.coeff = -r.a.coeff; + } + if (r.b.var != kNoIntegerVariable && !VariableIsPositive(r.b.var)) { + r.b.var = NegationOf(r.b.var); + r.b.coeff = -r.b.coeff; + } + + const int index = relations_.size(); + relations_.push_back(std::move(r)); + + if (lit.Index() >= lit_to_relations_.size()) { + lit_to_relations_.resize(lit.Index() + 1); + } + lit_to_relations_[lit.Index()].push_back(index); +} + +bool GreaterThanAtLeastOneOfDetector::AddRelationFromIndices( + IntegerVariable var, absl::Span clause, + absl::Span indices, Model* model) { + std::vector exprs; + std::vector selectors; + absl::flat_hash_set used; + auto* integer_trail = model->GetOrCreate(); + + const IntegerValue var_lb = integer_trail->LevelZeroLowerBound(var); + for (const int index : indices) { + Relation r = relations_[index]; + if (r.a.var != PositiveVariable(var)) std::swap(r.a, r.b); + CHECK_EQ(r.a.var, PositiveVariable(var)); + + if ((r.a.coeff == 1) == VariableIsPositive(var)) { + // a + b >= lhs + if (r.lhs <= kMinIntegerValue) continue; + exprs.push_back(AffineExpression(r.b.var, -r.b.coeff, r.lhs)); + } else { + // -a + b <= rhs. + if (r.rhs >= kMaxIntegerValue) continue; + exprs.push_back(AffineExpression(r.b.var, r.b.coeff, -r.rhs)); + } + + // Ignore this entry if it is always true. + if (var_lb >= integer_trail->LevelZeroUpperBound(exprs.back())) { + exprs.pop_back(); + continue; + } + + // Note that duplicate selector are supported. + selectors.push_back(r.enforcement); + used.insert(r.enforcement); + } + + // The enforcement of the new constraint are simply the literal not used + // above. + std::vector enforcements; + for (const Literal l : clause) { + if (!used.contains(l.Index())) { + enforcements.push_back(l.Negated()); + } + } + + // No point adding a constraint if there is not at least two different + // literals in selectors. + if (used.size() <= 1) return false; + + // Add the constraint. + GreaterThanAtLeastOneOfPropagator* constraint = + new GreaterThanAtLeastOneOfPropagator(var, exprs, selectors, enforcements, + model); + constraint->RegisterWith(model->GetOrCreate()); + model->TakeOwnership(constraint); + return true; +} + +int GreaterThanAtLeastOneOfDetector:: + AddGreaterThanAtLeastOneOfConstraintsFromClause( + const absl::Span clause, Model* model) { CHECK_EQ(model->GetOrCreate()->CurrentDecisionLevel(), 0); if (clause.size() < 2) return 0; - // Collect all arcs impacted by this clause. - std::vector infos; + // Collect all relations impacted by this clause. + std::vector> infos; for (const Literal l : clause) { - if (l.Index() >= literal_to_new_impacted_arcs_.size()) continue; - for (const ArcIndex arc_index : literal_to_new_impacted_arcs_[l.Index()]) { - const ArcInfo& arc = arcs_[arc_index]; - if (arc.presence_literals.size() != 1) continue; - - // TODO(user): Support variable offset. - if (arc.offset_var != kNoIntegerVariable) continue; - infos.push_back(arc); + if (l.Index() >= lit_to_relations_.size()) continue; + for (const int index : lit_to_relations_[l.Index()]) { + const Relation& r = relations_[index]; + if (r.a.var != kNoIntegerVariable && IntTypeAbs(r.a.coeff) == 1) { + infos.push_back({r.a.var, index}); + } + if (r.b.var != kNoIntegerVariable && IntTypeAbs(r.b.coeff) == 1) { + infos.push_back({r.b.var, index}); + } } } if (infos.size() <= 1) return 0; - // Stable sort by head_var so that for a same head_var, the entry are sorted - // by Literal as they appear in clause. - std::stable_sort(infos.begin(), infos.end(), - [](const ArcInfo& a, const ArcInfo& b) { - return a.head_var < b.head_var; - }); + // Stable sort to regroup by var. + std::stable_sort(infos.begin(), infos.end()); - // We process ArcInfo with the same head_var toghether. + // We process the info with same variable together. int num_added_constraints = 0; - auto* solver = model->GetOrCreate(); + std::vector indices; for (int i = 0; i < infos.size();) { const int start = i; - const IntegerVariable head_var = infos[start].head_var; - for (i++; i < infos.size() && infos[i].head_var == head_var; ++i) { - } - const absl::Span arcs(&infos[start], i - start); + const IntegerVariable var = infos[start].first; - // Skip single arcs since it will already be fully propagated. - if (arcs.size() < 2) continue; - - // Heuristic. Look for full or almost full clauses. We could add - // GreaterThanAtLeastOneOf() with more enforcement literals. TODO(user): - // experiments. - if (arcs.size() + 1 < clause.size()) continue; - - std::vector vars; - std::vector offsets; - std::vector selectors; - std::vector enforcements; - - int j = 0; - for (const Literal l : clause) { - bool added = false; - for (; j < arcs.size() && l == arcs[j].presence_literals.front(); ++j) { - added = true; - vars.push_back(arcs[j].tail_var); - offsets.push_back(arcs[j].offset); - - // Note that duplicate selector are supported. - // - // TODO(user): If we support variable offset, we should regroup the arcs - // into one (tail + offset <= head) though, instead of having too - // identical entries. - selectors.push_back(l); - } - if (!added) { - enforcements.push_back(l.Negated()); - } + indices.clear(); + for (; i < infos.size() && infos[i].first == var; ++i) { + indices.push_back(infos[i].second); } - // No point adding a constraint if there is not at least two different - // literals in selectors. - if (enforcements.size() + 1 == clause.size()) continue; + // Skip single relations, we are not interested in these. + if (indices.size() < 2) continue; - ++num_added_constraints; - model->Add(GreaterThanAtLeastOneOf(head_var, vars, offsets, selectors, - enforcements)); - if (!solver->FinishPropagation()) return num_added_constraints; + // Heuristic. Look for full or almost full clauses. + // + // TODO(user): We could add GreaterThanAtLeastOneOf() with more enforcement + // literals. Experiment. + if (indices.size() + 1 < clause.size()) continue; + + if (AddRelationFromIndices(var, clause, indices, model)) { + ++num_added_constraints; + } + if (AddRelationFromIndices(NegationOf(var), clause, indices, model)) { + ++num_added_constraints; + } } return num_added_constraints; } -int PrecedencesPropagator:: +int GreaterThanAtLeastOneOfDetector:: AddGreaterThanAtLeastOneOfConstraintsWithClauseAutoDetection(Model* model) { auto* time_limit = model->GetOrCreate(); auto* solver = model->GetOrCreate(); - // Fill the set of incoming conditional arcs for each variables. - absl::StrongVector> incoming_arcs_; - for (ArcIndex arc_index(0); arc_index < arcs_.size(); ++arc_index) { - const ArcInfo& arc = arcs_[arc_index]; - - // Only keep arc that have a fixed offset and a single presence_literals. - if (arc.offset_var != kNoIntegerVariable) continue; - if (arc.tail_var == arc.head_var) continue; - if (arc.presence_literals.size() != 1) continue; - - if (arc.head_var >= incoming_arcs_.size()) { - incoming_arcs_.resize(arc.head_var.value() + 1); + // Fill the set of interesting relations for each variables. + absl::StrongVector> var_to_relations; + for (int index = 0; index < relations_.size(); ++index) { + const Relation& r = relations_[index]; + if (r.a.var != kNoIntegerVariable && IntTypeAbs(r.a.coeff) == 1) { + if (r.a.var >= var_to_relations.size()) { + var_to_relations.resize(r.a.var + 1); + } + var_to_relations[r.a.var].push_back(index); + } + if (r.b.var != kNoIntegerVariable && IntTypeAbs(r.b.coeff) == 1) { + if (r.b.var >= var_to_relations.size()) { + var_to_relations.resize(r.b.var + 1); + } + var_to_relations[r.b.var].push_back(index); } - incoming_arcs_[arc.head_var].push_back(arc_index); } int num_added_constraints = 0; - for (IntegerVariable target(0); target < incoming_arcs_.size(); ++target) { - if (incoming_arcs_[target].size() <= 1) continue; + for (IntegerVariable target(0); target < var_to_relations.size(); ++target) { + if (var_to_relations[target].size() <= 1) continue; if (time_limit->LimitReached()) return num_added_constraints; // Detect set of incoming arcs for which at least one must be present. @@ -1135,55 +1198,56 @@ int PrecedencesPropagator:: solver->Backtrack(0); if (solver->ModelIsUnsat()) return num_added_constraints; std::vector clause; - for (const ArcIndex arc_index : incoming_arcs_[target]) { - const Literal literal = arcs_[arc_index].presence_literals.front(); + for (const int index : var_to_relations[target]) { + const Literal literal = relations_[index].enforcement; if (solver->Assignment().LiteralIsFalse(literal)) continue; const SatSolver::Status status = solver->EnqueueDecisionAndBacktrackOnConflict(literal.Negated()); if (status == SatSolver::INFEASIBLE) return num_added_constraints; if (status == SatSolver::ASSUMPTIONS_UNSAT) { + // We need to invert it, since a clause is not all false. clause = solver->GetLastIncompatibleDecisions(); + for (Literal& ref : clause) ref = ref.Negated(); break; } } solver->Backtrack(0); + if (clause.size() <= 1) continue; - if (clause.size() > 1) { - // Extract the set of arc for which at least one must be present. - const absl::btree_set clause_set(clause.begin(), clause.end()); - std::vector arcs_in_clause; - for (const ArcIndex arc_index : incoming_arcs_[target]) { - const Literal literal(arcs_[arc_index].presence_literals.front()); - if (clause_set.contains(literal.Negated())) { - arcs_in_clause.push_back(arc_index); - } + // Recover the indices corresponding to this clause. + const absl::btree_set clause_set(clause.begin(), clause.end()); + + std::vector indices; + for (const int index : var_to_relations[target]) { + const Literal literal = relations_[index].enforcement; + if (clause_set.contains(literal)) { + indices.push_back(index); } + } - VLOG(2) << arcs_in_clause.size() << "/" << incoming_arcs_[target].size(); - + // Try both direction. + if (AddRelationFromIndices(target, clause, indices, model)) { + ++num_added_constraints; + } + if (AddRelationFromIndices(NegationOf(target), clause, indices, model)) { ++num_added_constraints; - std::vector vars; - std::vector offsets; - std::vector selectors; - for (const ArcIndex a : arcs_in_clause) { - vars.push_back(arcs_[a].tail_var); - offsets.push_back(arcs_[a].offset); - selectors.push_back(Literal(arcs_[a].presence_literals.front())); - } - model->Add(GreaterThanAtLeastOneOf(target, vars, offsets, selectors, {})); - if (!solver->FinishPropagation()) return num_added_constraints; } } + solver->Backtrack(0); return num_added_constraints; } -int PrecedencesPropagator::AddGreaterThanAtLeastOneOfConstraints(Model* model) { - VLOG(1) << "Detecting GreaterThanAtLeastOneOf() constraints..."; +int GreaterThanAtLeastOneOfDetector::AddGreaterThanAtLeastOneOfConstraints( + Model* model, bool auto_detect_clauses) { auto* time_limit = model->GetOrCreate(); auto* solver = model->GetOrCreate(); auto* clauses = model->GetOrCreate(); + auto* logger = model->GetOrCreate(); + int num_added_constraints = 0; + SOLVER_LOG(logger, "[Precedences] num_relations=", relations_.size(), + " num_clauses=", clauses->AllClausesInCreationOrder().size()); // We have two possible approaches. For now, we prefer the first one except if // there is too many clauses in the problem. @@ -1191,7 +1255,8 @@ int PrecedencesPropagator::AddGreaterThanAtLeastOneOfConstraints(Model* model) { // TODO(user): Do more extensive experiment. Remove the second approach as // it is more time consuming? or identify when it make sense. Note that the // first approach also allows to use "incomplete" at least one between arcs. - if (clauses->AllClausesInCreationOrder().size() < 1e6) { + if (!auto_detect_clauses && + clauses->AllClausesInCreationOrder().size() < 1e6) { // TODO(user): This does not take into account clause of size 2 since they // are stored in the BinaryImplicationGraph instead. Some ideas specific // to size 2: @@ -1229,10 +1294,14 @@ int PrecedencesPropagator::AddGreaterThanAtLeastOneOfConstraints(Model* model) { } if (num_added_constraints > 0) { - SOLVER_LOG(model->GetOrCreate(), "[Precedences] Added ", - num_added_constraints, + SOLVER_LOG(logger, "[Precedences] Added ", num_added_constraints, " GreaterThanAtLeastOneOf() constraints."); } + + // Release the memory, it is not longer needed. + gtl::STLClearObject(&relations_); + gtl::STLClearObject(&lit_to_relations_); + return num_added_constraints; } diff --git a/ortools/sat/precedences.h b/ortools/sat/precedences.h index 6b329fd9df..41245d5395 100644 --- a/ortools/sat/precedences.h +++ b/ortools/sat/precedences.h @@ -234,16 +234,6 @@ class PrecedencesPropagator : public SatPropagator, PropagatorInterface { void ComputePartialPrecedences(const std::vector& vars, std::vector* output); - // Advanced usage. To be called once all the constraints have been added to - // the model. This will loop over all "node" in this class, and if one of its - // optional incoming arcs must be chosen, it will add a corresponding - // GreaterThanAtLeastOneOfConstraint(). Returns the number of added - // constraint. - // - // TODO(user): This can be quite slow, add some kind of deterministic limit - // so that we can use it all the time. - int AddGreaterThanAtLeastOneOfConstraints(Model* model); - // If known, return an offset such that we have a + offset <= b. // Note that this only cover the case where this was conditionned by a single // literal. @@ -262,19 +252,6 @@ class PrecedencesPropagator : public SatPropagator, PropagatorInterface { DEFINE_STRONG_INDEX_TYPE(ArcIndex); DEFINE_STRONG_INDEX_TYPE(OptionalArcIndex); - // Given an existing clause, sees if it can be used to add "greater than at - // least one of" type of constraints. Returns the number of such constraint - // added. - int AddGreaterThanAtLeastOneOfConstraintsFromClause( - absl::Span clause, Model* model); - - // Another approach for AddGreaterThanAtLeastOneOfConstraints(), this one - // might be a bit slow as it relies on the propagation engine to detect - // clauses between incoming arcs presence literals. - // Returns the number of added constraints. - int AddGreaterThanAtLeastOneOfConstraintsWithClauseAutoDetection( - Model* model); - // Information about an individual arc. struct ArcInfo { IntegerVariable tail_var; @@ -432,6 +409,66 @@ class PrecedencesPropagator : public SatPropagator, PropagatorInterface { int64_t num_enforcement_pushes_ = 0; }; +// Similar to AffineExpression, but with a zero constant. +// If coeff is zero, then this is always zero and var is ignored. +struct LinearTerm { + IntegerVariable var = kNoIntegerVariable; + IntegerValue coeff = IntegerValue(0); +}; + +// This collect all enforced linear of size 2 or 1 and detect if at least one of +// a subset touching the same variable must be true. When this is the case +// we add a new propagator to propagate that fact. +// +// TODO(user): Shall we do that on the main thread before the workers are +// spawned? note that the probing version need the model to be loaded though. +class GreaterThanAtLeastOneOfDetector { + public: + // Adds a relation lit => a + b \in [lhs, rhs]. + void Add(Literal lit, LinearTerm a, LinearTerm b, IntegerValue lhs, + IntegerValue rhs); + + // Advanced usage. To be called once all the constraints have been added to + // the model. This will detect GreaterThanAtLeastOneOfConstraint(). + // Returns the number of added constraint. + // + // TODO(user): This can be quite slow, add some kind of deterministic limit + // so that we can use it all the time. + int AddGreaterThanAtLeastOneOfConstraints(Model* model, + bool auto_detect_clauses = false); + + private: + // Given an existing clause, sees if it can be used to add "greater than at + // least one of" type of constraints. Returns the number of such constraint + // added. + int AddGreaterThanAtLeastOneOfConstraintsFromClause( + absl::Span clause, Model* model); + + // Another approach for AddGreaterThanAtLeastOneOfConstraints(), this one + // might be a bit slow as it relies on the propagation engine to detect + // clauses between incoming arcs presence literals. + // Returns the number of added constraints. + int AddGreaterThanAtLeastOneOfConstraintsWithClauseAutoDetection( + Model* model); + + // Once we identified a clause and relevant indices, this build the + // constraint. Returns true if we actually add it. + bool AddRelationFromIndices(IntegerVariable var, + absl::Span clause, + absl::Span indices, Model* model); + + struct Relation { + Literal enforcement; + LinearTerm a; + LinearTerm b; + IntegerValue lhs; + IntegerValue rhs; + }; + + std::vector relations_; + absl::StrongVector> lit_to_relations_; +}; + // ============================================================================= // Implementation of the small API functions below. // ============================================================================= diff --git a/ortools/sat/probing.cc b/ortools/sat/probing.cc index c661ae2ef4..d4d24ef56a 100644 --- a/ortools/sat/probing.cc +++ b/ortools/sat/probing.cc @@ -300,7 +300,7 @@ bool Prober::ProbeBooleanVariables( } bool Prober::ProbeDnf(absl::string_view name, - const std::vector>& dnf) { + absl::Span> dnf) { if (dnf.size() <= 1) return true; // Reset the solver in case it was already used. diff --git a/ortools/sat/probing.h b/ortools/sat/probing.h index 56def373d2..801951896b 100644 --- a/ortools/sat/probing.h +++ b/ortools/sat/probing.h @@ -87,7 +87,7 @@ class Prober { // the conjunction must be true, we might be able to fix literal or improve // integer bounds if all conjunction propagate the same thing. bool ProbeDnf(absl::string_view name, - const std::vector>& dnf); + absl::Span> dnf); // Statistics. // They are reset each time ProbleBooleanVariables() is called. diff --git a/ortools/sat/python/cp_model.py b/ortools/sat/python/cp_model.py index 98deb74acc..ad76a44746 100644 --- a/ortools/sat/python/cp_model.py +++ b/ortools/sat/python/cp_model.py @@ -47,7 +47,6 @@ rather than for solving specific optimization problems. import collections import itertools -import numbers import threading import time from typing import ( @@ -66,6 +65,7 @@ from typing import ( ) import warnings +import numpy as np import pandas as pd from ortools.sat import cp_model_pb2 @@ -119,16 +119,48 @@ PARTIAL_FIXED_SEARCH = sat_parameters_pb2.SatParameters.PARTIAL_FIXED_SEARCH RANDOMIZED_SEARCH = sat_parameters_pb2.SatParameters.RANDOMIZED_SEARCH # Type aliases -# We need to add int to numbers.Integral -IntegralT = Union[numbers.Integral, int] -# We need to add int and float, otherwise type checkers complain. -NumberT = Union[numbers.Integral, int, numbers.Number, float] +IntegralT = Union[int, np.int8, np.uint8, np.int32, np.uint32, np.int64, np.uint64] +IntegralTypes = ( + int, + np.int8, + np.uint8, + np.int32, + np.uint32, + np.int64, + np.uint64, +) +NumberT = Union[ + int, + float, + np.int8, + np.uint8, + np.int32, + np.uint32, + np.int64, + np.uint64, + np.double, +] +NumberTypes = ( + int, + float, + np.int8, + np.uint8, + np.int32, + np.uint32, + np.int64, + np.uint64, + np.double, +) + LiteralT = Union["IntVar", "_NotBooleanVariable", IntegralT, bool] BoolVarT = Union["IntVar", "_NotBooleanVariable"] VariableT = Union["IntVar", IntegralT] + +# We need to add 'IntVar' for pytype. LinearExprT = Union["LinearExpr", "IntVar", IntegralT] -ObjLinearExprT = Union["LinearExpr", "IntVar", NumberT] +ObjLinearExprT = Union["LinearExpr", NumberT] BoundedLinearExprT = Union["BoundedLinearExpression", bool] + ArcT = Tuple[IntegralT, IntegralT, LiteralT] _IndexOrSeries = Union[pd.Index, pd.Series] @@ -229,8 +261,7 @@ class LinearExpr: cls, expressions: Sequence[LinearExprT], coefficients: Sequence[IntegralT], - ) -> LinearExprT: - ... + ) -> LinearExprT: ... @overload @classmethod @@ -238,8 +269,7 @@ class LinearExpr: cls, expressions: Sequence[ObjLinearExprT], coefficients: Sequence[NumberT], - ) -> ObjLinearExprT: - ... + ) -> ObjLinearExprT: ... @classmethod def weighted_sum(cls, expressions, coefficients): @@ -257,8 +287,7 @@ class LinearExpr: cls, expressions: LinearExprT, coefficients: IntegralT, - ) -> LinearExprT: - ... + ) -> LinearExprT: ... @overload @classmethod @@ -266,8 +295,7 @@ class LinearExpr: cls, expressions: ObjLinearExprT, coefficients: NumberT, - ) -> ObjLinearExprT: - ... + ) -> ObjLinearExprT: ... @classmethod def term(cls, expression, coefficient): @@ -311,14 +339,16 @@ class LinearExpr: else: return _WeightedSum(variables, coeffs, offset) - def get_integer_var_value_map(self) -> Tuple[Dict["IntVar", IntegralT], int]: + def get_integer_var_value_map(self) -> Tuple[Dict["IntVar", int], int]: """Scans the expression, and returns (var_coef_map, constant).""" - coeffs = collections.defaultdict(int) + coeffs: Dict["IntVar", int] = collections.defaultdict(int) constant = 0 - to_process: List[Tuple[LinearExprT, IntegralT]] = [(self, 1)] + to_process: List[Tuple[LinearExprT, int]] = [(self, 1)] while to_process: # Flatten to avoid recursion. + expr: LinearExprT + coeff: int expr, coeff = to_process.pop() - if isinstance(expr, numbers.Integral): + if isinstance(expr, IntegralTypes): constant += coeff * int(expr) elif isinstance(expr, _ProductCst): to_process.append((expr.expression(), coeff * expr.coefficient())) @@ -347,14 +377,14 @@ class LinearExpr: self, ) -> Tuple[Dict["IntVar", float], float, bool]: """Scans the expression. Returns (var_coef_map, constant, is_integer).""" - coeffs = {} - constant = 0 - to_process: List[Tuple[LinearExprT, Union[IntegralT, float]]] = [(self, 1)] + coeffs: Dict["IntVar", Union[int, float]] = {} + constant: Union[int, float] = 0 + to_process: List[Tuple[LinearExprT, Union[int, float]]] = [(self, 1)] while to_process: # Flatten to avoid recursion. expr, coeff = to_process.pop() - if isinstance(expr, numbers.Integral): # Keep integrality. + if isinstance(expr, IntegralTypes): # Keep integrality. constant += coeff * int(expr) - elif isinstance(expr, numbers.Number): + elif isinstance(expr, NumberTypes): constant += coeff * float(expr) elif isinstance(expr, _ProductCst): to_process.append((expr.expression(), coeff * expr.coefficient())) @@ -382,10 +412,10 @@ class LinearExpr: coeffs[expr.negated()] = -coeff else: raise TypeError("Unrecognized linear expression: " + str(expr)) - is_integer = isinstance(constant, numbers.Integral) + is_integer = isinstance(constant, IntegralTypes) if is_integer: for coeff in coeffs.values(): - if not isinstance(coeff, numbers.Integral): + if not isinstance(coeff, IntegralTypes): is_integer = False break return coeffs, constant, is_integer @@ -400,12 +430,10 @@ class LinearExpr: ) @overload - def __add__(self, arg: LinearExprT) -> LinearExprT: - ... + def __add__(self, arg: "LinearExpr") -> "LinearExpr": ... @overload - def __add__(self, arg: ObjLinearExprT) -> ObjLinearExprT: - ... + def __add__(self, arg: NumberT) -> "LinearExpr": ... def __add__(self, arg): if cmh.is_zero(arg): @@ -413,53 +441,43 @@ class LinearExpr: return _Sum(self, arg) @overload - def __radd__(self, arg: LinearExprT) -> LinearExprT: - ... + def __radd__(self, arg: "LinearExpr") -> "LinearExpr": ... @overload - def __radd__(self, arg: ObjLinearExprT) -> ObjLinearExprT: - ... + def __radd__(self, arg: NumberT) -> "LinearExpr": ... def __radd__(self, arg): - if cmh.is_zero(arg): - return self - return _Sum(self, arg) + return self.__add__(arg) @overload - def __sub__(self, arg: LinearExprT) -> LinearExprT: - ... + def __sub__(self, arg: "LinearExpr") -> "LinearExpr": ... @overload - def __sub__(self, arg: ObjLinearExprT) -> ObjLinearExprT: - ... + def __sub__(self, arg: NumberT) -> "LinearExpr": ... def __sub__(self, arg): if cmh.is_zero(arg): return self - if isinstance(arg, numbers.Number): + if isinstance(arg, NumberTypes): arg = cmh.assert_is_a_number(arg) return _Sum(self, -arg) else: return _Sum(self, -arg) @overload - def __rsub__(self, arg: LinearExprT) -> LinearExprT: - ... + def __rsub__(self, arg: "LinearExpr") -> "LinearExpr": ... @overload - def __rsub__(self, arg: ObjLinearExprT) -> ObjLinearExprT: - ... + def __rsub__(self, arg: NumberT) -> "LinearExpr": ... def __rsub__(self, arg): return _Sum(-self, arg) @overload - def __mul__(self, arg: LinearExprT) -> LinearExprT: - ... + def __mul__(self, arg: IntegralT) -> Union["LinearExpr", IntegralT]: ... @overload - def __mul__(self, arg: ObjLinearExprT) -> ObjLinearExprT: - ... + def __mul__(self, arg: NumberT) -> Union["LinearExpr", NumberT]: ... def __mul__(self, arg): arg = cmh.assert_is_a_number(arg) @@ -470,20 +488,13 @@ class LinearExpr: return _ProductCst(self, arg) @overload - def __rmul__(self, arg: LinearExprT) -> LinearExprT: - ... + def __rmul__(self, arg: IntegralT) -> Union["LinearExpr", IntegralT]: ... @overload - def __rmul__(self, arg: ObjLinearExprT) -> ObjLinearExprT: - ... + def __rmul__(self, arg: NumberT) -> Union["LinearExpr", NumberT]: ... def __rmul__(self, arg): - arg = cmh.assert_is_a_number(arg) - if cmh.is_one(arg): - return self - elif cmh.is_zero(arg): - return 0 - return _ProductCst(self, arg) + return self.__mul__(arg) def __div__(self, _) -> NoReturn: raise NotImplementedError( @@ -537,7 +548,7 @@ class LinearExpr: "please use CpModel.add_bool_xor" ) - def __neg__(self) -> LinearExprT: + def __neg__(self) -> "LinearExpr": return _ProductCst(self, -1) def __bool__(self) -> NoReturn: @@ -545,31 +556,33 @@ class LinearExpr: "Evaluating a LinearExpr instance as a Boolean is not implemented." ) - def __eq__(self, arg: LinearExprT) -> BoundedLinearExprT: + def __eq__(self, arg: LinearExprT) -> BoundedLinearExprT: # type: ignore[override] if arg is None: return False - if isinstance(arg, numbers.Integral): + if isinstance(arg, IntegralTypes): arg = cmh.assert_is_int64(arg) return BoundedLinearExpression(self, [arg, arg]) - else: + elif isinstance(arg, LinearExpr): return BoundedLinearExpression(self - arg, [0, 0]) + else: + return False - def __ge__(self, arg: LinearExprT) -> BoundedLinearExprT: - if isinstance(arg, numbers.Integral): + def __ge__(self, arg: LinearExprT) -> "BoundedLinearExpression": + if isinstance(arg, IntegralTypes): arg = cmh.assert_is_int64(arg) return BoundedLinearExpression(self, [arg, INT_MAX]) else: return BoundedLinearExpression(self - arg, [0, INT_MAX]) - def __le__(self, arg: LinearExprT) -> BoundedLinearExprT: - if isinstance(arg, numbers.Integral): + def __le__(self, arg: LinearExprT) -> "BoundedLinearExpression": + if isinstance(arg, IntegralTypes): arg = cmh.assert_is_int64(arg) return BoundedLinearExpression(self, [INT_MIN, arg]) else: return BoundedLinearExpression(self - arg, [INT_MIN, 0]) - def __lt__(self, arg: LinearExprT) -> BoundedLinearExprT: - if isinstance(arg, numbers.Integral): + def __lt__(self, arg: LinearExprT) -> "BoundedLinearExpression": + if isinstance(arg, IntegralTypes): arg = cmh.assert_is_int64(arg) if arg == INT_MIN: raise ArithmeticError("< INT_MIN is not supported") @@ -577,8 +590,8 @@ class LinearExpr: else: return BoundedLinearExpression(self - arg, [INT_MIN, -1]) - def __gt__(self, arg: LinearExprT) -> BoundedLinearExprT: - if isinstance(arg, numbers.Integral): + def __gt__(self, arg: LinearExprT) -> "BoundedLinearExpression": + if isinstance(arg, IntegralTypes): arg = cmh.assert_is_int64(arg) if arg == INT_MAX: raise ArithmeticError("> INT_MAX is not supported") @@ -586,10 +599,10 @@ class LinearExpr: else: return BoundedLinearExpression(self - arg, [1, INT_MAX]) - def __ne__(self, arg: LinearExprT) -> BoundedLinearExprT: + def __ne__(self, arg: LinearExprT) -> BoundedLinearExprT: # type: ignore[override] if arg is None: return True - if isinstance(arg, numbers.Integral): + if isinstance(arg, IntegralTypes): arg = cmh.assert_is_int64(arg) if arg == INT_MAX: return BoundedLinearExpression(self, [INT_MIN, INT_MAX - 1]) @@ -599,8 +612,10 @@ class LinearExpr: return BoundedLinearExpression( self, [INT_MIN, arg - 1, arg + 1, INT_MAX] ) - else: + elif isinstance(arg, LinearExpr): return BoundedLinearExpression(self - arg, [INT_MIN, -1, 1, INT_MAX]) + else: + return True # Compatibility with pre PEP8 # pylint: disable=invalid-name @@ -615,8 +630,7 @@ class LinearExpr: cls, expressions: Sequence[LinearExprT], coefficients: Sequence[IntegralT], - ) -> LinearExprT: - ... + ) -> LinearExprT: ... @overload @classmethod @@ -624,8 +638,7 @@ class LinearExpr: cls, expressions: Sequence[ObjLinearExprT], coefficients: Sequence[NumberT], - ) -> ObjLinearExprT: - ... + ) -> ObjLinearExprT: ... @classmethod def WeightedSum(cls, expressions, coefficients): @@ -638,8 +651,7 @@ class LinearExpr: cls, expressions: LinearExprT, coefficients: IntegralT, - ) -> LinearExprT: - ... + ) -> LinearExprT: ... @overload @classmethod @@ -647,8 +659,7 @@ class LinearExpr: cls, expressions: ObjLinearExprT, coefficients: NumberT, - ) -> ObjLinearExprT: - ... + ) -> ObjLinearExprT: ... @classmethod def Term(cls, expression, coefficient): @@ -663,7 +674,7 @@ class _Sum(LinearExpr): def __init__(self, left, right): for x in [left, right]: - if not isinstance(x, (numbers.Number, LinearExpr)): + if not isinstance(x, (NumberTypes, LinearExpr)): raise TypeError("not an linear expression: " + str(x)) self.__left = left self.__right = right @@ -716,7 +727,7 @@ class _SumArray(LinearExpr): self.__expressions = [] self.__constant = constant for x in expressions: - if isinstance(x, numbers.Number): + if isinstance(x, NumberTypes): if cmh.is_zero(x): continue x = cmh.assert_is_a_number(x) @@ -762,7 +773,7 @@ class _WeightedSum(LinearExpr): c = cmh.assert_is_a_number(c) if cmh.is_zero(c): continue - if isinstance(e, numbers.Number): + if isinstance(e, NumberTypes): e = cmh.assert_is_a_number(e) self.__constant += e * c elif isinstance(e, LinearExpr): @@ -829,9 +840,9 @@ class IntVar(LinearExpr): def __init__( self, model: cp_model_pb2.CpModelProto, - domain: Union[int, Domain], + domain: Union[int, sorted_interval_list.Domain], name: Optional[str], - ): + ) -> None: """See CpModel.new_int_var below.""" self.__negation: Optional[_NotBooleanVariable] = None # Python do not support multiple __init__ methods. @@ -841,13 +852,15 @@ class IntVar(LinearExpr): # model is a CpModelProto, domain is a Domain, and name is a string. # case 2: # model is a CpModelProto, domain is an index (int), and name is None. - if isinstance(domain, numbers.Integral) and name is None: + if isinstance(domain, IntegralTypes) and name is None: self.__index: int = int(domain) self.__var: cp_model_pb2.IntegerVariableProto = model.variables[domain] else: self.__index: int = len(model.variables) self.__var: cp_model_pb2.IntegerVariableProto = model.variables.add() - self.__var.domain.extend(cast(Domain, domain).flattened_intervals()) + self.__var.domain.extend( + cast(sorted_interval_list.Domain, domain).flattened_intervals() + ) self.__var.name = name @property @@ -974,7 +987,7 @@ class BoundedLinearExpression: model.add(x + 2 * y -1 >= z) """ - def __init__(self, expr: LinearExprT, bounds: Sequence[int]): + def __init__(self, expr: LinearExprT, bounds: Sequence[int]) -> None: self.__expr: LinearExprT = expr self.__bounds: Sequence[int] = bounds @@ -1056,7 +1069,7 @@ class Constraint: def __init__( self, cp_model: "CpModel", - ): + ) -> None: self.__index: int = len(cp_model.proto.constraints) self.__cp_model: "CpModel" = cp_model self.__constraint: cp_model_pb2.ConstraintProto = ( @@ -1064,12 +1077,10 @@ class Constraint: ) @overload - def only_enforce_if(self, boolvar: Iterable[LiteralT]) -> "Constraint": - ... + def only_enforce_if(self, boolvar: Iterable[LiteralT]) -> "Constraint": ... @overload - def only_enforce_if(self, *boolvar: LiteralT) -> "Constraint": - ... + def only_enforce_if(self, *boolvar: LiteralT) -> "Constraint": ... def only_enforce_if(self, *boolvar) -> "Constraint": """Adds an enforcement literal to the constraint. @@ -1090,12 +1101,12 @@ class Constraint: """ for lit in expand_generator_or_tuple(boolvar): if (cmh.is_boolean(lit) and lit) or ( - isinstance(lit, numbers.Integral) and lit == 1 + isinstance(lit, IntegralTypes) and lit == 1 ): # Always true. Do nothing. pass elif (cmh.is_boolean(lit) and not lit) or ( - isinstance(lit, numbers.Integral) and lit == 0 + isinstance(lit, IntegralTypes) and lit == 0 ): self.__constraint.enforcement_literal.append( self.__cp_model.new_constant(0).index @@ -1174,7 +1185,7 @@ class IntervalVar: end: Optional[cp_model_pb2.LinearExpressionProto], is_present_index: Optional[int], name: Optional[str], - ): + ) -> None: self.__model: cp_model_pb2.CpModelProto = model # As with the IntVar::__init__ method, we hack the __init__ method to # support two use cases: @@ -1275,7 +1286,7 @@ def object_is_a_true_literal(literal: LiteralT) -> bool: if isinstance(literal, _NotBooleanVariable): proto = literal.negated().proto return len(proto.domain) == 2 and proto.domain[0] == 0 and proto.domain[1] == 0 - if isinstance(literal, numbers.Integral): + if isinstance(literal, IntegralTypes): return int(literal) == 1 return False @@ -1288,7 +1299,7 @@ def object_is_a_false_literal(literal: LiteralT) -> bool: if isinstance(literal, _NotBooleanVariable): proto = literal.negated().proto return len(proto.domain) == 2 and proto.domain[0] == 1 and proto.domain[1] == 1 - if isinstance(literal, numbers.Integral): + if isinstance(literal, IntegralTypes): return int(literal) == 0 return False @@ -1302,9 +1313,9 @@ class CpModel: * ```add``` create new constraints and add them to the model. """ - def __init__(self): + def __init__(self) -> None: self.__model: cp_model_pb2.CpModelProto = cp_model_pb2.CpModelProto() - self.__constant_map = {} + self.__constant_map: Dict[IntegralT, int] = {} # Naming. @property @@ -1337,9 +1348,11 @@ class CpModel: a variable whose domain is [lb, ub]. """ - return IntVar(self.__model, Domain(lb, ub), name) + return IntVar(self.__model, sorted_interval_list.Domain(lb, ub), name) - def new_int_var_from_domain(self, domain: Domain, name: str) -> IntVar: + def new_int_var_from_domain( + self, domain: sorted_interval_list.Domain, name: str + ) -> IntVar: """Create an integer variable from a domain. A domain is a set of integers specified by a collection of intervals. @@ -1357,7 +1370,7 @@ class CpModel: def new_bool_var(self, name: str) -> IntVar: """Creates a 0-1 variable with the given name.""" - return IntVar(self.__model, Domain(0, 1), name) + return IntVar(self.__model, sorted_interval_list.Domain(0, 1), name) def new_constant(self, value: IntegralT) -> IntVar: """Declares a constant integer.""" @@ -1397,8 +1410,8 @@ class CpModel: if not name.isidentifier(): raise ValueError("name={} is not a valid identifier".format(name)) if ( - isinstance(lower_bounds, numbers.Integral) - and isinstance(upper_bounds, numbers.Integral) + isinstance(lower_bounds, IntegralTypes) + and isinstance(upper_bounds, IntegralTypes) and lower_bounds > upper_bounds ): raise ValueError( @@ -1419,7 +1432,9 @@ class CpModel: IntVar( model=self.__model, name=f"{name}[{i}]", - domain=Domain(lower_bounds[i], upper_bounds[i]), + domain=sorted_interval_list.Domain( + lower_bounds[i], upper_bounds[i] + ), ) for i in index ], @@ -1453,10 +1468,12 @@ class CpModel: self, linear_expr: LinearExprT, lb: IntegralT, ub: IntegralT ) -> Constraint: """Adds the constraint: `lb <= linear_expr <= ub`.""" - return self.add_linear_expression_in_domain(linear_expr, Domain(lb, ub)) + return self.add_linear_expression_in_domain( + linear_expr, sorted_interval_list.Domain(lb, ub) + ) def add_linear_expression_in_domain( - self, linear_expr: LinearExprT, domain: Domain + self, linear_expr: LinearExprT, domain: sorted_interval_list.Domain ) -> Constraint: """Adds the constraint: `linear_expr` in `domain`.""" if isinstance(linear_expr, LinearExpr): @@ -1476,7 +1493,7 @@ class CpModel: ] ) return ct - if isinstance(linear_expr, numbers.Integral): + if isinstance(linear_expr, IntegralTypes): if not domain.contains(int(linear_expr)): return self.add_bool_or([]) # Evaluate to false. else: @@ -1489,7 +1506,13 @@ class CpModel: + ")" ) - def add(self, ct: Union[BoundedLinearExpression, bool]) -> Constraint: + @overload + def add(self, ct: BoundedLinearExpression) -> Constraint: ... + + @overload + def add(self, ct: Union[bool, np.bool_]) -> Constraint: ... + + def add(self, ct): """Adds a `BoundedLinearExpression` to the model. Args: @@ -1500,7 +1523,8 @@ class CpModel: """ if isinstance(ct, BoundedLinearExpression): return self.add_linear_expression_in_domain( - ct.expression(), Domain.from_flat_intervals(ct.bounds()) + ct.expression(), + sorted_interval_list.Domain.from_flat_intervals(ct.bounds()), ) if ct and cmh.is_boolean(ct): return self.add_bool_or([True]) @@ -1511,12 +1535,10 @@ class CpModel: # General Integer Constraints. @overload - def add_all_different(self, expressions: Iterable[LinearExprT]) -> Constraint: - ... + def add_all_different(self, expressions: Iterable[LinearExprT]) -> Constraint: ... @overload - def add_all_different(self, *expressions: LinearExprT) -> Constraint: - ... + def add_all_different(self, *expressions: LinearExprT) -> Constraint: ... def add_all_different(self, *expressions): """Adds AllDifferent(expressions). @@ -1554,8 +1576,9 @@ class CpModel: if not variables: raise ValueError("add_element expects a non-empty variables array") - if isinstance(index, numbers.Integral): - return self.add(list(variables)[int(index)] == target) + if isinstance(index, IntegralTypes): + variable: VariableT = list(variables)[int(index)] + return self.add(variable == target) ct = Constraint(self) model_ct = self.__model.constraints[ct.index] @@ -2001,12 +2024,10 @@ class CpModel: return ct @overload - def add_bool_or(self, literals: Iterable[LiteralT]) -> Constraint: - ... + def add_bool_or(self, literals: Iterable[LiteralT]) -> Constraint: ... @overload - def add_bool_or(self, *literals: LiteralT) -> Constraint: - ... + def add_bool_or(self, *literals: LiteralT) -> Constraint: ... def add_bool_or(self, *literals): """Adds `Or(literals) == true`: sum(literals) >= 1.""" @@ -2021,24 +2042,20 @@ class CpModel: return ct @overload - def add_at_least_one(self, literals: Iterable[LiteralT]) -> Constraint: - ... + def add_at_least_one(self, literals: Iterable[LiteralT]) -> Constraint: ... @overload - def add_at_least_one(self, *literals: LiteralT) -> Constraint: - ... + def add_at_least_one(self, *literals: LiteralT) -> Constraint: ... def add_at_least_one(self, *literals): """Same as `add_bool_or`: `sum(literals) >= 1`.""" return self.add_bool_or(*literals) @overload - def add_at_most_one(self, literals: Iterable[LiteralT]) -> Constraint: - ... + def add_at_most_one(self, literals: Iterable[LiteralT]) -> Constraint: ... @overload - def add_at_most_one(self, *literals: LiteralT) -> Constraint: - ... + def add_at_most_one(self, *literals: LiteralT) -> Constraint: ... def add_at_most_one(self, *literals): """Adds `AtMostOne(literals)`: `sum(literals) <= 1`.""" @@ -2053,12 +2070,10 @@ class CpModel: return ct @overload - def add_exactly_one(self, literals: Iterable[LiteralT]) -> Constraint: - ... + def add_exactly_one(self, literals: Iterable[LiteralT]) -> Constraint: ... @overload - def add_exactly_one(self, *literals: LiteralT) -> Constraint: - ... + def add_exactly_one(self, *literals: LiteralT) -> Constraint: ... def add_exactly_one(self, *literals): """Adds `ExactlyOne(literals)`: `sum(literals) == 1`.""" @@ -2073,12 +2088,10 @@ class CpModel: return ct @overload - def add_bool_and(self, literals: Iterable[LiteralT]) -> Constraint: - ... + def add_bool_and(self, literals: Iterable[LiteralT]) -> Constraint: ... @overload - def add_bool_and(self, *literals: LiteralT) -> Constraint: - ... + def add_bool_and(self, *literals: LiteralT) -> Constraint: ... def add_bool_and(self, *literals): """Adds `And(literals) == true`.""" @@ -2093,12 +2106,10 @@ class CpModel: return ct @overload - def add_bool_xor(self, literals: Iterable[LiteralT]) -> Constraint: - ... + def add_bool_xor(self, literals: Iterable[LiteralT]) -> Constraint: ... @overload - def add_bool_xor(self, *literals: LiteralT) -> Constraint: - ... + def add_bool_xor(self, *literals: LiteralT) -> Constraint: ... def add_bool_xor(self, *literals): """Adds `XOr(literals) == true`. @@ -2725,7 +2736,7 @@ class CpModel: and arg.coefficient() == -1 ): return -arg.expression().index - 1 - if isinstance(arg, numbers.Integral): + if isinstance(arg, IntegralTypes): arg = cmh.assert_is_int64(arg) return self.get_or_make_index_from_constant(arg) raise TypeError("NotSupported: model.get_or_make_index(" + str(arg) + ")") @@ -2738,7 +2749,7 @@ class CpModel: if isinstance(arg, _NotBooleanVariable): self.assert_is_boolean_variable(arg.negated()) return arg.index - if isinstance(arg, numbers.Integral): + if isinstance(arg, IntegralTypes): arg = cmh.assert_is_zero_or_one(arg) return self.get_or_make_index_from_constant(arg) if cmh.is_boolean(arg): @@ -2774,7 +2785,7 @@ class CpModel: cp_model_pb2.LinearExpressionProto() ) mult = -1 if negate else 1 - if isinstance(linear_expr, numbers.Integral): + if isinstance(linear_expr, IntegralTypes): result.offset = int(linear_expr) * mult return result @@ -2826,7 +2837,7 @@ class CpModel: for v, c in coeffs_map.items(): self.__model.floating_point_objective.coeffs.append(c) self.__model.floating_point_objective.vars.append(v.index) - elif isinstance(obj, numbers.Integral): + elif isinstance(obj, IntegralTypes): self.__model.objective.offset = int(obj) self.__model.objective.scaling_factor = 1 else: @@ -2962,6 +2973,7 @@ class CpModel: AddAutomaton = add_automaton AddInverse = add_inverse AddReservoirConstraint = add_reservoir_constraint + AddReservoirConstraintWithActive = add_reservoir_constraint_with_active AddImplication = add_implication AddBoolOr = add_bool_or AddAtLeastOne = add_at_least_one @@ -2977,11 +2989,11 @@ class CpModel: AddMultiplicationEquality = add_multiplication_equality NewIntervalVar = new_interval_var NewIntervalVarSeries = new_interval_var_series - NewFixedSizedIntervalVar = new_fixed_size_interval_var + NewFixedSizeIntervalVar = new_fixed_size_interval_var NewOptionalIntervalVar = new_optional_interval_var NewOptionalIntervalVarSeries = new_optional_interval_var_series - NewOptionalFixedSizedIntervalVar = new_optional_fixed_size_interval_var - NewOptionalFixedSizedIntervalVarSeries = new_optional_fixed_size_interval_var_series + NewOptionalFixedSizeIntervalVar = new_optional_fixed_size_interval_var + NewOptionalFixedSizeIntervalVarSeries = new_optional_fixed_size_interval_var_series AddNoOverlap = add_no_overlap AddNoOverlap2D = add_no_overlap_2d AddCumulative = add_cumulative @@ -3009,22 +3021,20 @@ class CpModel: @overload def expand_generator_or_tuple( args: Union[Tuple[LiteralT, ...], Iterable[LiteralT]] -) -> Union[Iterable[LiteralT], LiteralT]: - ... +) -> Union[Iterable[LiteralT], LiteralT]: ... @overload def expand_generator_or_tuple( args: Union[Tuple[LinearExprT, ...], Iterable[LinearExprT]] -) -> Union[Iterable[LinearExprT], LinearExprT]: - ... +) -> Union[Iterable[LinearExprT], LinearExprT]: ... def expand_generator_or_tuple(args): if hasattr(args, "__len__"): # Tuple if len(args) != 1: return args - if isinstance(args[0], (numbers.Number, LinearExpr)): + if isinstance(args[0], (NumberTypes, LinearExpr)): return args # Generator return args[0] @@ -3034,7 +3044,7 @@ def evaluate_linear_expr( expression: LinearExprT, solution: cp_model_pb2.CpSolverResponse ) -> int: """Evaluate a linear expression against a solution.""" - if isinstance(expression, numbers.Integral): + if isinstance(expression, IntegralTypes): return int(expression) if not isinstance(expression, LinearExpr): raise TypeError("Cannot interpret %s as a linear expression." % expression) @@ -3043,7 +3053,7 @@ def evaluate_linear_expr( to_process = [(expression, 1)] while to_process: expr, coeff = to_process.pop() - if isinstance(expr, numbers.Integral): + if isinstance(expr, IntegralTypes): value += int(expr) * coeff elif isinstance(expr, _ProductCst): to_process.append((expr.expression(), coeff * expr.coefficient())) @@ -3072,7 +3082,7 @@ def evaluate_boolean_expression( literal: LiteralT, solution: cp_model_pb2.CpSolverResponse ) -> bool: """Evaluate a boolean expression against a solution.""" - if isinstance(literal, numbers.Integral): + if isinstance(literal, IntegralTypes): return bool(literal) elif isinstance(literal, IntVar) or isinstance(literal, _NotBooleanVariable): index: int = cast(Union[IntVar, _NotBooleanVariable], literal).index @@ -3095,7 +3105,7 @@ class CpSolver: about the solve procedure. """ - def __init__(self): + def __init__(self) -> None: self.__solution: Optional[cp_model_pb2.CpSolverResponse] = None self.parameters: sat_parameters_pb2.SatParameters = ( sat_parameters_pb2.SatParameters() @@ -3390,7 +3400,7 @@ class CpSolverSolutionCallback(swig_helper.SolutionCallback): `CpSolver` class. """ - def __init__(self): + def __init__(self) -> None: swig_helper.SolutionCallback.__init__(self) def OnSolutionCallback(self) -> None: @@ -3411,7 +3421,7 @@ class CpSolverSolutionCallback(swig_helper.SolutionCallback): """ if not self.has_response(): raise RuntimeError("solve() has not been called.") - if isinstance(lit, numbers.Integral): + if isinstance(lit, IntegralTypes): return bool(lit) if isinstance(lit, IntVar) or isinstance(lit, _NotBooleanVariable): return self.SolutionBooleanValue( @@ -3441,7 +3451,7 @@ class CpSolverSolutionCallback(swig_helper.SolutionCallback): to_process = [(expression, 1)] while to_process: expr, coeff = to_process.pop() - if isinstance(expr, numbers.Integral): + if isinstance(expr, IntegralTypes): value += int(expr) * coeff elif isinstance(expr, _ProductCst): to_process.append((expr.expression(), coeff * expr.coefficient())) @@ -3563,7 +3573,7 @@ class CpSolverSolutionCallback(swig_helper.SolutionCallback): class ObjectiveSolutionPrinter(CpSolverSolutionCallback): """Display the objective value and time of intermediate solutions.""" - def __init__(self): + def __init__(self) -> None: CpSolverSolutionCallback.__init__(self) self.__solution_count = 0 self.__start_time = time.time() @@ -3586,7 +3596,7 @@ class ObjectiveSolutionPrinter(CpSolverSolutionCallback): class VarArrayAndObjectiveSolutionPrinter(CpSolverSolutionCallback): """Print intermediate solutions (objective, variable values, time).""" - def __init__(self, variables): + def __init__(self, variables: Sequence[IntVar]) -> None: CpSolverSolutionCallback.__init__(self) self.__variables: Sequence[IntVar] = variables self.__solution_count: int = 0 @@ -3614,7 +3624,7 @@ class VarArrayAndObjectiveSolutionPrinter(CpSolverSolutionCallback): class VarArraySolutionPrinter(CpSolverSolutionCallback): """Print intermediate solutions (variable values, time).""" - def __init__(self, variables: Sequence[IntVar]): + def __init__(self, variables: Sequence[IntVar]) -> None: CpSolverSolutionCallback.__init__(self) self.__variables: Sequence[IntVar] = variables self.__solution_count: int = 0 @@ -3681,7 +3691,7 @@ def _convert_to_integral_series_and_validate_index( TypeError: If the type of `value_or_series` is not recognized. ValueError: If the index does not match. """ - if isinstance(value_or_series, numbers.Integral): + if isinstance(value_or_series, IntegralTypes): result = pd.Series(data=value_or_series, index=index) elif isinstance(value_or_series, pd.Series): if value_or_series.index.equals(index): @@ -3709,7 +3719,7 @@ def _convert_to_linear_expr_series_and_validate_index( TypeError: If the type of `value_or_series` is not recognized. ValueError: If the index does not match. """ - if isinstance(value_or_series, numbers.Integral): + if isinstance(value_or_series, IntegralTypes): result = pd.Series(data=value_or_series, index=index) elif isinstance(value_or_series, pd.Series): if value_or_series.index.equals(index): @@ -3737,7 +3747,7 @@ def _convert_to_literal_series_and_validate_index( TypeError: If the type of `value_or_series` is not recognized. ValueError: If the index does not match. """ - if isinstance(value_or_series, numbers.Integral): + if isinstance(value_or_series, IntegralTypes): result = pd.Series(data=value_or_series, index=index) elif isinstance(value_or_series, pd.Series): if value_or_series.index.equals(index): diff --git a/ortools/sat/python/cp_model_helper.py b/ortools/sat/python/cp_model_helper.py index 662e1cbd38..76b698ad31 100644 --- a/ortools/sat/python/cp_model_helper.py +++ b/ortools/sat/python/cp_model_helper.py @@ -37,7 +37,7 @@ def is_zero(x: Any) -> bool: """Checks if the x is 0 or 0.0.""" if isinstance(x, numbers.Integral): return int(x) == 0 - if isinstance(x, numbers.Number): + if isinstance(x, numbers.Real): return float(x) == 0.0 return False @@ -46,7 +46,7 @@ def is_one(x: Any) -> bool: """Checks if x is 1 or 1.0.""" if isinstance(x, numbers.Integral): return int(x) == 1 - if isinstance(x, numbers.Number): + if isinstance(x, numbers.Real): return float(x) == 1.0 return False @@ -55,7 +55,7 @@ def is_minus_one(x: Any) -> bool: """Checks if x is -1 or -1.0 .""" if isinstance(x, numbers.Integral): return int(x) == -1 - if isinstance(x, numbers.Number): + if isinstance(x, numbers.Real): return float(x) == -1.0 return False @@ -89,7 +89,7 @@ def assert_is_a_number(x: Any) -> Union[int, float]: """Asserts that x is a number and returns it casted to an int or a float.""" if isinstance(x, numbers.Integral): return int(x) - if isinstance(x, numbers.Number): + if isinstance(x, numbers.Real): return float(x) raise TypeError("Not a number: %s" % x) diff --git a/ortools/sat/python/cp_model_helper_test.py b/ortools/sat/python/cp_model_helper_test.py index 35f9347eb9..40fe7b2c25 100644 --- a/ortools/sat/python/cp_model_helper_test.py +++ b/ortools/sat/python/cp_model_helper_test.py @@ -20,6 +20,7 @@ from ortools.sat.python import cp_model_helper class CpModelHelperTest(absltest.TestCase): + def test_is_boolean(self): print("test_is_boolean") self.assertTrue(cp_model_helper.is_boolean(True)) @@ -34,9 +35,7 @@ class CpModelHelperTest(absltest.TestCase): self.assertRaises(TypeError, cp_model_helper.assert_is_int64, "Hello") self.assertRaises(TypeError, cp_model_helper.assert_is_int64, 1.2) self.assertRaises(OverflowError, cp_model_helper.assert_is_int64, 2**63) - self.assertRaises( - OverflowError, cp_model_helper.assert_is_int64, -(2**63) - 1 - ) + self.assertRaises(OverflowError, cp_model_helper.assert_is_int64, -(2**63) - 1) cp_model_helper.assert_is_int64(123) cp_model_helper.assert_is_int64(2**63 - 1) cp_model_helper.assert_is_int64(-(2**63)) diff --git a/ortools/sat/python/cp_model_test.py b/ortools/sat/python/cp_model_test.py index fc2562f33d..f128bf5a9a 100644 --- a/ortools/sat/python/cp_model_test.py +++ b/ortools/sat/python/cp_model_test.py @@ -111,6 +111,7 @@ class LogToString: class CpModelTest(absltest.TestCase): + def testCreateIntegerVariable(self): print("testCreateIntegerVariable") model = cp_model.CpModel() diff --git a/ortools/sat/python/swig_helper_test.py b/ortools/sat/python/swig_helper_test.py index f41364180d..adb9011f95 100644 --- a/ortools/sat/python/swig_helper_test.py +++ b/ortools/sat/python/swig_helper_test.py @@ -22,6 +22,7 @@ from ortools.sat.python import swig_helper class Callback(swig_helper.SolutionCallback): + def __init__(self): swig_helper.SolutionCallback.__init__(self) self.__solution_count = 0 @@ -35,6 +36,7 @@ class Callback(swig_helper.SolutionCallback): class SwigHelperTest(absltest.TestCase): + def testVariableDomain(self): model_string = """ variables { domain: [ -10, 10 ] } diff --git a/ortools/sat/rins.cc b/ortools/sat/rins.cc index e9576ee1b2..edff8f5048 100644 --- a/ortools/sat/rins.cc +++ b/ortools/sat/rins.cc @@ -104,8 +104,8 @@ struct VarWeight { bool operator<(const VarWeight& o) const { return weight < o.weight; } }; -void FillRinsNeighborhood(const std::vector& solution, - const std::vector& relaxation_values, +void FillRinsNeighborhood(absl::Span solution, + absl::Span relaxation_values, double difficulty, absl::BitGenRef random, ReducedDomainNeighborhood& reduced_domains) { std::vector var_lp_gap_pairs; diff --git a/ortools/sat/routing_cuts.cc b/ortools/sat/routing_cuts.cc index 4c1497c0eb..237d04f725 100644 --- a/ortools/sat/routing_cuts.cc +++ b/ortools/sat/routing_cuts.cc @@ -89,7 +89,7 @@ class OutgoingCutHelper { // Given a subset of nodes, it is easy to identify the best subset A of edge // to consider. bool TryBlossomSubsetCut(std::string name, - const std::vector& symmetrized_edges, + absl::Span symmetrized_edges, absl::Span subset); private: @@ -271,7 +271,7 @@ bool OutgoingCutHelper::TrySubsetCut(std::string name, } bool OutgoingCutHelper::TryBlossomSubsetCut( - std::string name, const std::vector& symmetrized_edges, + std::string name, absl::Span symmetrized_edges, absl::Span subset) { DCHECK_GE(subset.size(), 1); DCHECK_LT(subset.size(), num_nodes_); @@ -715,7 +715,7 @@ namespace { // Returns for each literal its integer view, or the view of its negation. std::vector GetAssociatedVariables( - const std::vector& literals, Model* model) { + absl::Span literals, Model* model) { auto* encoder = model->GetOrCreate(); std::vector result; for (const Literal l : literals) { @@ -792,8 +792,8 @@ CutGenerator CreateCVRPCutGenerator(int num_nodes, std::vector tails, // This is really similar to SeparateSubtourInequalities, see the reference // there. void SeparateFlowInequalities( - int num_nodes, const std::vector& tails, const std::vector& heads, - const std::vector& arc_capacities, + int num_nodes, absl::Span tails, absl::Span heads, + absl::Span arc_capacities, std::function& in_subset, IntegerValue* min_incoming_flow, IntegerValue* min_outgoing_flow)> diff --git a/ortools/sat/samples/bin_packing_sat.py b/ortools/sat/samples/bin_packing_sat.py index 680f1949aa..9ac4f9e807 100644 --- a/ortools/sat/samples/bin_packing_sat.py +++ b/ortools/sat/samples/bin_packing_sat.py @@ -121,10 +121,13 @@ def main() -> None: for b in active_bins: print(f"Bin {b}") - items_in_bin = x_values.xs(b, level="bin").loc[lambda x: x].index - for item in items_in_bin: + items_in_active_bin = x_values.xs(b, level="bin").loc[lambda x: x].index + for item in items_in_active_bin: print(f" Item {item} - weight {items.loc[item].weight}") - print(f" Packed items weight: {items.loc[items_in_bin].sum().to_string()}") + print( + " Packed items weight:" + f" {items.loc[items_in_active_bin].sum().to_string()}" + ) print() print(f"Total packed weight: {items.weight.sum()}") diff --git a/ortools/sat/samples/schedule_requests_sat.py b/ortools/sat/samples/schedule_requests_sat.py index f87789c64c..4518a75eda 100644 --- a/ortools/sat/samples/schedule_requests_sat.py +++ b/ortools/sat/samples/schedule_requests_sat.py @@ -15,6 +15,8 @@ # [START program] """Nurse scheduling problem with shift requests.""" # [START import] +from typing import Union + from ortools.sat.python import cp_model # [END import] @@ -80,7 +82,7 @@ def main() -> None: else: max_shifts_per_nurse = min_shifts_per_nurse + 1 for n in all_nurses: - num_shifts_worked = 0 + num_shifts_worked: Union[cp_model.LinearExpr, int] = 0 for d in all_days: for s in all_shifts: num_shifts_worked += shifts[(n, d, s)] diff --git a/ortools/sat/samples/solution_hinting_sample_sat.go b/ortools/sat/samples/solution_hinting_sample_sat.go index 1d67fdc13f..59b2766c2b 100644 --- a/ortools/sat/samples/solution_hinting_sample_sat.go +++ b/ortools/sat/samples/solution_hinting_sample_sat.go @@ -32,10 +32,10 @@ func solutionHintingSampleSat() error { model.AddNotEqual(x, y) - model.Maximize(cpmodel.NewLinearExpr().AddWeightedSum([]cpmodel.LinearArgument{x, y, z}, []int64_t{1, 2, 3})) + model.Maximize(cpmodel.NewLinearExpr().AddWeightedSum([]cpmodel.LinearArgument{x, y, z}, []int64{1, 2, 3})) // Solution hinting: x <- 1, y <- 2 - hint := &cpmodel.Hint{Ints: map[cpmodel.IntVar]int64_t{x: 7}} + hint := &cpmodel.Hint{Ints: map[cpmodel.IntVar]int64{x: 7}} model.SetHint(hint) m, err := model.Model() diff --git a/ortools/sat/samples/step_function_sample_sat.go b/ortools/sat/samples/step_function_sample_sat.go index a3dfb25daf..3545973734 100644 --- a/ortools/sat/samples/step_function_sample_sat.go +++ b/ortools/sat/samples/step_function_sample_sat.go @@ -45,7 +45,7 @@ func stepFunctionSampleSat() error { // expr == 0 on [5, 6] U [8, 10] b0 := model.NewBoolVar() - d0 := cpmodel.FromValues([]int64_t{5, 6, 8, 9, 10}) + d0 := cpmodel.FromValues([]int64{5, 6, 8, 9, 10}) model.AddLinearConstraintForDomain(x, d0).OnlyEnforceIf(b0) model.AddEquality(expr, cpmodel.NewConstant(0)).OnlyEnforceIf(b0) diff --git a/ortools/sat/sat_parameters.proto b/ortools/sat/sat_parameters.proto index 81dda8ca2e..a856518443 100644 --- a/ortools/sat/sat_parameters.proto +++ b/ortools/sat/sat_parameters.proto @@ -23,7 +23,7 @@ option csharp_namespace = "Google.OrTools.Sat"; // Contains the definitions for all the sat algorithm parameters and their // default values. // -// NEXT TAG: 280 +// NEXT TAG: 281 message SatParameters { // In some context, like in a portfolio of search, it makes sense to name a // given parameters set for logging purpose. @@ -464,6 +464,13 @@ message SatParameters { // possible precedences between event and encoding the constraint. optional bool expand_reservoir_constraints = 182 [default = true]; + // If true, replace target = max(x, y) by linear constraint with the + // introduction of a new boolean b such that b => target == x and not(b) => + // target == y. + // + // This is mainly for experimenting compared to a custom lin_max propagator. + optional int32 max_lin_max_size_for_expansion = 280 [default = 0]; + // If true, it disable all constraint expansion. // This should only be used to test the presolve of expanded constraints. optional bool disable_constraint_expansion = 181 [default = false]; @@ -1217,8 +1224,10 @@ message SatParameters { // breaking during search. optional int32 symmetry_level = 183 [default = 2]; - // Experimental. Use new code to propagate linear constraint. - optional bool new_linear_propagation = 224 [default = false]; + // The new linear propagation code treat all constraints at once and use + // an adaptation of Bellman-Ford-Tarjan to propagate constraint in a smarter + // order and potentially detect propagation cycle earlier. + optional bool new_linear_propagation = 224 [default = true]; // Linear constraints that are not pseudo-Boolean and that are longer than // this size will be split into sqrt(size) intermediate sums in order to have