From ee241f30b5715174502d549615b73e5d078c99a1 Mon Sep 17 00:00:00 2001 From: Laurent Perron Date: Fri, 25 Oct 2024 13:15:18 +0200 Subject: [PATCH] [CP-SAT] supports affine expression in automaton --- ortools/flatzinc/cp_model_fz_solver.cc | 10 +- .../java/com/google/ortools/sat/CpModel.java | 50 +- ortools/sat/BUILD.bazel | 3 + ortools/sat/cp_model.cc | 32 +- ortools/sat/cp_model.h | 14 + ortools/sat/cp_model.proto | 9 +- ortools/sat/cp_model_checker.cc | 40 +- ortools/sat/cp_model_expand.cc | 82 +-- ortools/sat/cp_model_expand.h | 8 +- ortools/sat/cp_model_expand_test.cc | 24 +- ortools/sat/cp_model_postsolve.cc | 21 +- ortools/sat/cp_model_presolve.cc | 552 ++++++++++++++---- ortools/sat/cp_model_presolve.h | 9 +- ortools/sat/cp_model_table.cc | 52 ++ ortools/sat/cp_model_table.h | 6 + ortools/sat/cp_model_utils.cc | 24 +- ortools/sat/csharp/Constraints.cs | 8 +- ortools/sat/csharp/CpModel.cs | 53 +- ortools/sat/java/CpModelTest.java | 30 + .../sat/linear_programming_constraint_test.cc | 1 + ortools/sat/presolve_context.cc | 153 ++++- ortools/sat/presolve_context.h | 14 +- ortools/sat/python/cp_model.py | 37 +- ortools/sat/python/cp_model_test.py | 2 +- ortools/sat/table_test.cc | 8 +- 25 files changed, 957 insertions(+), 285 deletions(-) diff --git a/ortools/flatzinc/cp_model_fz_solver.cc b/ortools/flatzinc/cp_model_fz_solver.cc index 456ad64fef0..fcce8d4e5e5 100644 --- a/ortools/flatzinc/cp_model_fz_solver.cc +++ b/ortools/flatzinc/cp_model_fz_solver.cc @@ -749,7 +749,15 @@ void CpModelProtoWithMapping::FillConstraint(const fz::Constraint& fz_ct, arg->add_values(value); } else if (fz_ct.type == "ortools_regular") { auto* arg = ct->mutable_automaton(); - for (const int var : LookupVars(fz_ct.arguments[0])) arg->add_vars(var); + for (const VarOrValue v : LookupVarsOrValues(fz_ct.arguments[0])) { + LinearExpressionProto* expr = arg->add_exprs(); + if (v.var != kNoVar) { + expr->add_vars(v.var); + expr->add_coeffs(1); + } else { + expr->set_offset(v.value); + } + } int count = 0; const int num_states = fz_ct.arguments[1].Value(); diff --git a/ortools/java/com/google/ortools/sat/CpModel.java b/ortools/java/com/google/ortools/sat/CpModel.java index 78e54140b05..72f86014e95 100644 --- a/ortools/java/com/google/ortools/sat/CpModel.java +++ b/ortools/java/com/google/ortools/sat/CpModel.java @@ -509,11 +509,11 @@ public TableConstraint addForbiddenAssignments(IterableAn automaton constraint takes a list of variables (of size n), an initial state, a set of - * final states, and a set of transitions that will be added incrementally directly on the + *

An automaton constraint takes a list of affine expressions (of size n), an initial state, a + * set of final states, and a set of transitions that will be added incrementally directly on the * returned AutomatonConstraint instance. A transition is a triplet ('tail', 'transition', * 'head'), where 'tail' and 'head' are states, and 'transition' is the label of an arc from - * 'head' to 'tail', corresponding to the value of one variable in the list of variables. + * 'head' to 'tail', corresponding to the value of one expression in the list of expressions. * *

This automaton will be unrolled into a flow with n + 1 phases. Each phase contains the * possible states of the automaton. The first state contains the initial state. The last phase @@ -521,26 +521,48 @@ public TableConstraint addForbiddenAssignments(IterableBetween two consecutive phases i and i + 1, the automaton creates a set of arcs. For each * transition (tail, label, head), it will add an arc from the state 'tail' of phase i and the - * state 'head' of phase i + 1. This arc labeled by the value 'label' of the variables - * 'variables[i]'. That is, this arc can only be selected if 'variables[i]' is assigned the value - * 'label'. + * state 'head' of phase i + 1. This arc labeled by the value 'label' of the expression + * 'expressions[i]'. That is, this arc can only be selected if 'expressions[i]' is assigned the + * value 'label'. * - *

A feasible solution of this constraint is an assignment of variables such that, starting - * from the initial state in phase 0, there is a path labeled by the values of the variables that - * ends in one of the final states in the final phase. + *

A feasible solution of this constraint is an assignment of expressions such that, starting + * from the initial state in phase 0, there is a path labeled by the values of the expressions + * that ends in one of the final states in the final phase. * - * @param transitionVariables a non empty list of variables whose values correspond to the labels - * of the arcs traversed by the automaton + * @param transitionExpressions a non empty list of affine expressions (a * var + b) whose values + * correspond to the labels of the arcs traversed by the automaton * @param startingState the initial state of the automaton * @param finalStates a non empty list of admissible final states * @return an instance of the Constraint class */ public AutomatonConstraint addAutomaton( - IntVar[] transitionVariables, long startingState, long[] finalStates) { + LinearArgument[] transitionExpressions, long startingState, long[] finalStates) { AutomatonConstraint ct = new AutomatonConstraint(modelBuilder); AutomatonConstraintProto.Builder automaton = ct.getBuilder().getAutomatonBuilder(); - for (IntVar var : transitionVariables) { - automaton.addVars(var.getIndex()); + for (LinearArgument expr : transitionExpressions) { + automaton.addExprs( + getLinearExpressionProtoBuilderFromLinearArgument(expr, /* negate= */ false)); + } + automaton.setStartingState(startingState); + for (long c : finalStates) { + automaton.addFinalStates(c); + } + return ct; + } + + /** + * Adds an automaton constraint. + * + * @see addAutomaton(LinearArgument[] transitionExpressions, long startingState, long[] + * finalStates) + */ + public AutomatonConstraint addAutomaton(Iterable transitionExpressions, + long startingState, long[] finalStates) { + AutomatonConstraint ct = new AutomatonConstraint(modelBuilder); + AutomatonConstraintProto.Builder automaton = ct.getBuilder().getAutomatonBuilder(); + for (LinearArgument expr : transitionExpressions) { + automaton.addExprs( + getLinearExpressionProtoBuilderFromLinearArgument(expr, /* negate= */ false)); } automaton.setStartingState(startingState); for (long c : finalStates) { diff --git a/ortools/sat/BUILD.bazel b/ortools/sat/BUILD.bazel index 851f3f2bbe3..e5faa5bdbe1 100644 --- a/ortools/sat/BUILD.bazel +++ b/ortools/sat/BUILD.bazel @@ -757,6 +757,7 @@ cc_library( hdrs = ["presolve_context.h"], deps = [ ":cp_model_cc_proto", + ":cp_model_checker", ":cp_model_loader", ":cp_model_mapping", ":cp_model_utils", @@ -820,6 +821,7 @@ cc_library( ":presolve_context", "//ortools/base:stl_util", "@com_google_absl//absl/container:flat_hash_map", + "@com_google_absl//absl/container:flat_hash_set", "@com_google_absl//absl/container:inlined_vector", "@com_google_absl//absl/log:check", "@com_google_absl//absl/types:span", @@ -980,6 +982,7 @@ cc_library( "//ortools/port:proto_utils", "//ortools/util:logging", "//ortools/util:sorted_interval_list", + "@com_google_absl//absl/algorithm:container", "@com_google_absl//absl/container:btree", "@com_google_absl//absl/container:flat_hash_map", "@com_google_absl//absl/container:flat_hash_set", diff --git a/ortools/sat/cp_model.cc b/ortools/sat/cp_model.cc index 1b92b5a482e..bdee3f4537d 100644 --- a/ortools/sat/cp_model.cc +++ b/ortools/sat/cp_model.cc @@ -1056,12 +1056,42 @@ ReservoirConstraint CpModelBuilder::AddReservoirConstraint(int64_t min_level, return ReservoirConstraint(proto, this); } +AutomatonConstraint CpModelBuilder::AddAutomaton( + absl::Span transition_expressions, int starting_state, + absl::Span final_states) { + ConstraintProto* const proto = cp_model_.add_constraints(); + for (const LinearExpr& expr : transition_expressions) { + *proto->mutable_automaton()->add_exprs() = LinearExprToProto(expr); + } + proto->mutable_automaton()->set_starting_state(starting_state); + for (const int final_state : final_states) { + proto->mutable_automaton()->add_final_states(final_state); + } + return AutomatonConstraint(proto); +} + AutomatonConstraint CpModelBuilder::AddAutomaton( absl::Span transition_variables, int starting_state, absl::Span final_states) { ConstraintProto* const proto = cp_model_.add_constraints(); for (const IntVar& var : transition_variables) { - proto->mutable_automaton()->add_vars(var.index_); + LinearExpressionProto* expr = proto->mutable_automaton()->add_exprs(); + expr->add_vars(var.index_); + expr->add_coeffs(1); + } + proto->mutable_automaton()->set_starting_state(starting_state); + for (const int final_state : final_states) { + proto->mutable_automaton()->add_final_states(final_state); + } + return AutomatonConstraint(proto); +} + +AutomatonConstraint CpModelBuilder::AddAutomaton( + std::initializer_list transition_expressions, + int starting_state, absl::Span final_states) { + ConstraintProto* const proto = cp_model_.add_constraints(); + for (const LinearExpr& expr : transition_expressions) { + *proto->mutable_automaton()->add_exprs() = LinearExprToProto(expr); } proto->mutable_automaton()->set_starting_state(starting_state); for (const int final_state : final_states) { diff --git a/ortools/sat/cp_model.h b/ortools/sat/cp_model.h index 3cffecba2d5..eab648c1051 100644 --- a/ortools/sat/cp_model.h +++ b/ortools/sat/cp_model.h @@ -1001,10 +1001,24 @@ class CpModelBuilder { * It returns an AutomatonConstraint that allows adding transition * incrementally after construction. */ + AutomatonConstraint AddAutomaton( + absl::Span transition_expressions, int starting_state, + absl::Span final_states); + + /** + * An automaton constraint. + */ AutomatonConstraint AddAutomaton( absl::Span transition_variables, int starting_state, absl::Span final_states); + /** + * An automaton constraint. + */ + AutomatonConstraint AddAutomaton( + std::initializer_list transition_expressions, + int starting_state, absl::Span final_states); + /// Adds target == min(vars). Constraint AddMinEquality(const LinearExpr& target, absl::Span vars); diff --git a/ortools/sat/cp_model.proto b/ortools/sat/cp_model.proto index f3e5f12ef32..faa9cb2788f 100644 --- a/ortools/sat/cp_model.proto +++ b/ortools/sat/cp_model.proto @@ -268,7 +268,7 @@ message InverseConstraintProto { repeated int32 f_inverse = 2; } -// This constraint forces a sequence of variables to be accepted by an +// This constraint forces a sequence of expressions to be accepted by an // automaton. message AutomatonConstraintProto { // A state is identified by a non-negative number. It is preferable to keep @@ -284,9 +284,12 @@ message AutomatonConstraintProto { repeated int64 transition_head = 5; repeated int64 transition_label = 6; - // The sequence of variables. The automaton is ran for vars_size() "steps" and - // the value of vars[i] corresponds to the transition label at step i. + // Legacy field. repeated int32 vars = 7; + // The sequence of affine expressions (a * var + b). The automaton is ran for + // exprs_size() "steps" and the value of exprs[i] corresponds to the + // transition label at step i. + repeated LinearExpressionProto exprs = 8; } // A list of variables, without any semantics. diff --git a/ortools/sat/cp_model_checker.cc b/ortools/sat/cp_model_checker.cc index 8b6d3e84e3d..6b3766f7a5a 100644 --- a/ortools/sat/cp_model_checker.cc +++ b/ortools/sat/cp_model_checker.cc @@ -498,18 +498,24 @@ std::string ValidateTableConstraint(const ConstraintProto& ct) { } std::string ValidateAutomatonConstraint(const ConstraintProto& ct) { - const int num_transistions = ct.automaton().transition_tail().size(); - if (num_transistions != ct.automaton().transition_head().size() || - num_transistions != ct.automaton().transition_label().size()) { + const AutomatonConstraintProto& automaton = ct.automaton(); + if (!automaton.vars().empty() && !automaton.exprs().empty()) { + return absl::StrCat( + "Inconsistent automaton with both legacy and new format defined: ", + ProtobufShortDebugString(ct)); + } + const int num_transistions = automaton.transition_tail().size(); + if (num_transistions != automaton.transition_head().size() || + num_transistions != automaton.transition_label().size()) { return absl::StrCat( "The transitions repeated fields must have the same size: ", ProtobufShortDebugString(ct)); } absl::flat_hash_map, int64_t> tail_label_to_head; for (int i = 0; i < num_transistions; ++i) { - const int64_t tail = ct.automaton().transition_tail(i); - const int64_t head = ct.automaton().transition_head(i); - const int64_t label = ct.automaton().transition_label(i); + const int64_t tail = automaton.transition_tail(i); + const int64_t head = automaton.transition_head(i); + const int64_t label = automaton.transition_label(i); if (label <= std::numeric_limits::min() + 1 || label == std::numeric_limits::max()) { return absl::StrCat("labels in the automaton constraint are too big: ", @@ -1489,20 +1495,24 @@ class ConstraintChecker { bool AutomatonConstraintIsFeasible(const ConstraintProto& ct) { // Build the transition table {tail, label} -> head. + const AutomatonConstraintProto& automaton = ct.automaton(); absl::flat_hash_map, int64_t> transition_map; - const int num_transitions = ct.automaton().transition_tail().size(); + const int num_transitions = automaton.transition_tail().size(); for (int i = 0; i < num_transitions; ++i) { - transition_map[{ct.automaton().transition_tail(i), - ct.automaton().transition_label(i)}] = - ct.automaton().transition_head(i); + transition_map[{automaton.transition_tail(i), + automaton.transition_label(i)}] = + automaton.transition_head(i); } // Walk the automaton. - int64_t current_state = ct.automaton().starting_state(); - const int num_steps = ct.automaton().vars_size(); + int64_t current_state = automaton.starting_state(); + const int num_steps = + std::max(automaton.vars_size(), automaton.exprs_size()); for (int i = 0; i < num_steps; ++i) { - const std::pair key = {current_state, - Value(ct.automaton().vars(i))}; + const std::pair key = { + current_state, automaton.vars().empty() + ? LinearExpressionValue(automaton.exprs(i)) + : Value(automaton.vars(i))}; if (!transition_map.contains(key)) { return false; } @@ -1510,7 +1520,7 @@ class ConstraintChecker { } // Check we are now in a final state. - for (const int64_t final : ct.automaton().final_states()) { + for (const int64_t final : automaton.final_states()) { if (current_state == final) return true; } return false; diff --git a/ortools/sat/cp_model_expand.cc b/ortools/sat/cp_model_expand.cc index 9c4cc52875c..e6e18421cd1 100644 --- a/ortools/sat/cp_model_expand.cc +++ b/ortools/sat/cp_model_expand.cc @@ -22,6 +22,7 @@ #include #include +#include "absl/algorithm/container.h" #include "absl/container/btree_map.h" #include "absl/container/flat_hash_map.h" #include "absl/container/flat_hash_set.h" @@ -46,58 +47,6 @@ namespace operations_research { namespace sat { - -// TODO(user): Note that if we have duplicate variables controlling different -// time point, this might not reach the fixed point. Fix? it is not that -// important as the expansion take care of this case anyway. -void PropagateAutomaton(const AutomatonConstraintProto& proto, - const PresolveContext& context, - std::vector>* states, - std::vector>* labels) { - const int n = proto.vars_size(); - const absl::flat_hash_set final_states( - {proto.final_states().begin(), proto.final_states().end()}); - - labels->clear(); - labels->resize(n); - states->clear(); - states->resize(n + 1); - (*states)[0].insert(proto.starting_state()); - - // Forward pass. - for (int time = 0; time < n; ++time) { - for (int t = 0; t < proto.transition_tail_size(); ++t) { - const int64_t tail = proto.transition_tail(t); - const int64_t label = proto.transition_label(t); - const int64_t head = proto.transition_head(t); - if (!(*states)[time].contains(tail)) continue; - if (!context.DomainContains(proto.vars(time), label)) continue; - if (time == n - 1 && !final_states.contains(head)) continue; - (*labels)[time].insert(label); - (*states)[time + 1].insert(head); - } - } - - // Backward pass. - for (int time = n - 1; time >= 0; --time) { - absl::flat_hash_set new_states; - absl::flat_hash_set new_labels; - for (int t = 0; t < proto.transition_tail_size(); ++t) { - const int64_t tail = proto.transition_tail(t); - const int64_t label = proto.transition_label(t); - const int64_t head = proto.transition_head(t); - - if (!(*states)[time].contains(tail)) continue; - if (!(*labels)[time].contains(label)) continue; - if (!(*states)[time + 1].contains(head)) continue; - new_labels.insert(label); - new_states.insert(tail); - } - (*labels)[time].swap(new_labels); - (*states)[time].swap(new_states); - } -} - namespace { // Different encoding that support general demands. This is usually a pretty bad @@ -1030,7 +979,7 @@ void AddImplyInReachableValues(int literal, void ExpandAutomaton(ConstraintProto* ct, PresolveContext* context) { AutomatonConstraintProto& proto = *ct->mutable_automaton(); - if (proto.vars_size() == 0) { + if (proto.exprs_size() == 0) { const int64_t initial_state = proto.starting_state(); for (const int64_t final_state : proto.final_states()) { if (initial_state == final_state) { @@ -1060,8 +1009,7 @@ void ExpandAutomaton(ConstraintProto* ct, PresolveContext* context) { absl::flat_hash_map out_encoding; bool removed_values = false; - const int n = proto.vars_size(); - const std::vector vars = {proto.vars().begin(), proto.vars().end()}; + const int n = proto.exprs_size(); for (int time = 0; time < n; ++time) { // All these vector have the same size. We will use them to enforce a // local table constraint representing one step of the automaton at the @@ -1076,7 +1024,7 @@ void ExpandAutomaton(ConstraintProto* ct, PresolveContext* context) { if (!reachable_states[time].contains(tail)) continue; if (!reachable_states[time + 1].contains(head)) continue; - if (!context->DomainContains(vars[time], label)) continue; + if (!context->DomainContains(proto.exprs(time), label)) continue; // TODO(user): if this transition correspond to just one in-state or // one-out state or one variable value, we could reuse the corresponding @@ -1092,7 +1040,8 @@ void ExpandAutomaton(ConstraintProto* ct, PresolveContext* context) { // Deal with single tuple. const int num_tuples = in_states.size(); if (num_tuples == 1) { - if (!context->IntersectDomainWith(vars[time], Domain(labels.front()))) { + if (!context->IntersectDomainWith(proto.exprs(time), + Domain(labels.front()))) { VLOG(1) << "Infeasible automaton."; return; } @@ -1115,20 +1064,23 @@ void ExpandAutomaton(ConstraintProto* ct, PresolveContext* context) { // Fully encode vars[time]. { std::vector transitions = labels; + const LinearExpressionProto& expr = proto.exprs(time); gtl::STLSortAndRemoveDuplicates(&transitions); encoding.clear(); - if (!context->IntersectDomainWith( - vars[time], Domain::FromValues(transitions), &removed_values)) { + if (!context->IntersectDomainWith(expr, Domain::FromValues(transitions), + &removed_values)) { VLOG(1) << "Infeasible automaton."; return; } // Fully encode the variable. // We can leave the encoding empty for fixed vars. - if (!context->IsFixed(vars[time])) { - for (const int64_t v : context->DomainOf(vars[time]).Values()) { - encoding[v] = context->GetOrCreateVarValueEncoding(vars[time], v); + if (!context->IsFixed(expr)) { + const int var = expr.vars(0); + for (const int64_t v : context->DomainOf(var).Values()) { + encoding[AffineExpressionValueAt(expr, v)] = + context->GetOrCreateVarValueEncoding(var, v); } } } @@ -1234,7 +1186,11 @@ void ExpandAutomaton(ConstraintProto* ct, PresolveContext* context) { in_to_label[in_states[i]].push_back(labels[i]); in_to_out[in_states[i]].push_back(out_states[i]); } - for (const auto [in_value, in_literal] : in_encoding) { + // Sort the pairs to make the order deterministic. + std::vector> in_to_label_pairs( + in_encoding.begin(), in_encoding.end()); + absl::c_sort(in_to_label_pairs); + for (const auto [in_value, in_literal] : in_to_label_pairs) { AddImplyInReachableValues(in_literal, in_to_label[in_value], encoding, context); AddImplyInReachableValues(in_literal, in_to_out[in_value], out_encoding, diff --git a/ortools/sat/cp_model_expand.h b/ortools/sat/cp_model_expand.h index e8428a39b9a..c63ea637487 100644 --- a/ortools/sat/cp_model_expand.h +++ b/ortools/sat/cp_model_expand.h @@ -35,15 +35,9 @@ void ExpandCpModel(PresolveContext* context); // presolve. We do that at the end, because the presolve is allowed to simplify // such constraints by updating the rhs. Also the extra variable we create are // only linked by a few constraints to the rest of the model and should not be -// presolvable. +// pre-solvable. void FinalExpansionForLinearConstraint(PresolveContext* context); -// Fills and propagates the set of reachable states/labels. -void PropagateAutomaton(const AutomatonConstraintProto& proto, - const PresolveContext& context, - std::vector>* states, - std::vector>* labels); - } // namespace sat } // namespace operations_research diff --git a/ortools/sat/cp_model_expand_test.cc b/ortools/sat/cp_model_expand_test.cc index 95fedc47029..5cfb1e64205 100644 --- a/ortools/sat/cp_model_expand_test.cc +++ b/ortools/sat/cp_model_expand_test.cc @@ -686,9 +686,9 @@ TEST(AutomatonExpandTest, Bug1753_1) { transition_head: 1 transition_label: 1 transition_label: 2 - vars: 0 - vars: 1 - vars: 2 + exprs { vars: 0 coeffs: 1 } + exprs { vars: 1 coeffs: 1 } + exprs { vars: 2 coeffs: 1 } } } )pb"); @@ -756,7 +756,12 @@ TEST(AutomatonExpandTest, EverythingZero) { transition_tail: 1, transition_head: 1, transition_label: 0, - vars: [ 0, 1, 2, 3, 4, 5 ], + exprs { vars: 0 coeffs: 1 } + exprs { vars: 1 coeffs: 1 } + exprs { vars: 2 coeffs: 1 } + exprs { vars: 3 coeffs: 1 } + exprs { vars: 4 coeffs: 1 } + exprs { vars: 5 coeffs: 1 } } } )pb"); @@ -842,7 +847,16 @@ TEST(AutomatonExpandTest, LoopingAutomatonMultipleFinalStatesNegatedVariables) { transition_tail: [ 1, 1, 2, 3, 3, 4 ], transition_head: [ 1, 2, 3, 2, 4, 4 ], transition_label: [ 0, 1, 2, 1, 0, 0 ], - vars: [ 0, -2, 2, 3, 4, 5, 6, 7, 8, 9 ], + exprs { vars: 0 coeffs: 1 } + exprs { vars: 1 coeffs: -1 } + exprs { vars: 2 coeffs: 1 } + exprs { vars: 3 coeffs: 1 } + exprs { vars: 4 coeffs: 1 } + exprs { vars: 5 coeffs: 1 } + exprs { vars: 6 coeffs: 1 } + exprs { vars: 7 coeffs: 1 } + exprs { vars: 8 coeffs: 1 } + exprs { vars: 9 coeffs: 1 } } } )pb"); diff --git a/ortools/sat/cp_model_postsolve.cc b/ortools/sat/cp_model_postsolve.cc index bd046fd1125..5f329a9625d 100644 --- a/ortools/sat/cp_model_postsolve.cc +++ b/ortools/sat/cp_model_postsolve.cc @@ -170,6 +170,7 @@ void PostsolveLinear(const ConstraintProto& ct, std::vector* domains) { Domain term = (*domains)[free_vars[i]].MultiplicationBy(-free_coeffs[i]); rhs_domains.push_back(term.AdditionWith(rhs_domains.back())); } + std::vector values(free_vars.size()); for (int i = free_vars.size() - 1; i >= 0; --i) { // Choose a value for free_vars[i] that fall into rhs_domains[i] - // fixed_activity. This will crash if the intersection is empty, but it @@ -184,12 +185,28 @@ void PostsolveLinear(const ConstraintProto& ct, std::vector* domains) { // TODO(user): I am not 100% that the algo here might cover all the presolve // case, so if this fail, it might indicate an issue here and not in the // presolve/solver code. + if (domain.IsEmpty()) { + LOG(INFO) << "Empty domain while trying to assign " << var; + for (int i = 0; i < size; ++i) { + const int var = ct.linear().vars(i); + LOG(INFO) << var << " " << (*domains)[var]; + } + LOG(FATAL) << "Couldn't postsolve the constraint: " + << ProtobufShortDebugString(ct); + } + CHECK(!domain.IsEmpty()) << ProtobufShortDebugString(ct); const int64_t value = domain.SmallestValue(); - (*domains)[var] = Domain(value); - + values[i] = value; fixed_activity += coeff * value; } + + // We assign that afterwards for better debugging if we run into the domains + // empty above. + for (int i = 0; i < free_vars.size(); ++i) { + (*domains)[free_vars[i]] = Domain(values[i]); + } + DCHECK(initial_rhs.Contains(fixed_activity)); } diff --git a/ortools/sat/cp_model_presolve.cc b/ortools/sat/cp_model_presolve.cc index cf1cdc0c050..5310777a840 100644 --- a/ortools/sat/cp_model_presolve.cc +++ b/ortools/sat/cp_model_presolve.cc @@ -5906,6 +5906,7 @@ bool CpModelPresolver::PresolveNoOverlap2D(int /*c*/, ConstraintProto* ct) { return RemoveConstraint(ct); } } + RunPropagatorsForConstraint(*ct); return new_size < initial_num_boxes; } @@ -6419,6 +6420,7 @@ bool CpModelPresolver::PresolveCumulative(ConstraintProto* ct) { } } + RunPropagatorsForConstraint(*ct); return changed; } @@ -6479,6 +6481,7 @@ bool CpModelPresolver::PresolveRoutes(ConstraintProto* ct) { return true; } + RunPropagatorsForConstraint(*ct); return false; } @@ -6675,105 +6678,53 @@ bool CpModelPresolver::PresolveCircuit(ConstraintProto* ct) { context_->UpdateRuleStats("circuit: removed false arcs."); return true; } + RunPropagatorsForConstraint(*ct); return false; } bool CpModelPresolver::PresolveAutomaton(ConstraintProto* ct) { if (context_->ModelIsUnsat()) return false; if (HasEnforcementLiteral(*ct)) return false; - AutomatonConstraintProto& proto = *ct->mutable_automaton(); - if (proto.vars_size() == 0 || proto.transition_label_size() == 0) { - return false; - } - bool all_have_same_affine_relation = true; - std::vector affine_relations; - for (int v = 0; v < proto.vars_size(); ++v) { - const int var = ct->automaton().vars(v); - const AffineRelation::Relation r = context_->GetAffineRelation(var); - affine_relations.push_back(r); - if (r.representative == var) { - all_have_same_affine_relation = false; - break; - } - if (v > 0 && (r.coeff != affine_relations[v - 1].coeff || - r.offset != affine_relations[v - 1].offset)) { - all_have_same_affine_relation = false; - break; - } + AutomatonConstraintProto* proto = ct->mutable_automaton(); + if (proto->exprs_size() == 0 || proto->transition_label_size() == 0) { + return false; } - if (all_have_same_affine_relation) { // Unscale labels. - for (int v = 0; v < proto.vars_size(); ++v) { - proto.set_vars(v, affine_relations[v].representative); - } - const AffineRelation::Relation rep = affine_relations.front(); - int new_size = 0; - for (int t = 0; t < proto.transition_tail_size(); ++t) { - const int64_t label = proto.transition_label(t); - int64_t inverse_label = (label - rep.offset) / rep.coeff; - if (inverse_label * rep.coeff + rep.offset == label) { - if (new_size != t) { - proto.set_transition_tail(new_size, proto.transition_tail(t)); - proto.set_transition_head(new_size, proto.transition_head(t)); - } - proto.set_transition_label(new_size, inverse_label); - new_size++; - } - } - if (new_size < proto.transition_tail_size()) { - proto.mutable_transition_tail()->Truncate(new_size); - proto.mutable_transition_label()->Truncate(new_size); - proto.mutable_transition_head()->Truncate(new_size); - context_->UpdateRuleStats("automaton: remove invalid transitions"); - } - context_->UpdateRuleStats("automaton: unscale all affine labels"); - return true; + bool changed = false; + for (int i = 0; i < proto->exprs_size(); ++i) { + changed |= CanonicalizeLinearExpression(*ct, proto->mutable_exprs(i)); } std::vector> reachable_states; std::vector> reachable_labels; - PropagateAutomaton(proto, *context_, &reachable_states, &reachable_labels); + PropagateAutomaton(*proto, *context_, &reachable_states, &reachable_labels); // Filter domains and compute the union of all relevant labels. - bool removed_values = false; - Domain hull; for (int time = 0; time < reachable_labels.size(); ++time) { - if (!context_->IntersectDomainWith( - proto.vars(time), - Domain::FromValues( - {reachable_labels[time].begin(), reachable_labels[time].end()}), - &removed_values)) { - return false; - } - hull = hull.UnionWith(context_->DomainOf(proto.vars(time))); - } - if (removed_values) { - context_->UpdateRuleStats("automaton: reduced variable domains"); - } - - // Only keep relevant transitions. - int new_size = 0; - for (int t = 0; t < proto.transition_tail_size(); ++t) { - const int64_t label = proto.transition_label(t); - if (hull.Contains(label)) { - if (new_size != t) { - proto.set_transition_tail(new_size, proto.transition_tail(t)); - proto.set_transition_label(new_size, label); - proto.set_transition_head(new_size, proto.transition_head(t)); + const LinearExpressionProto& expr = proto->exprs(time); + if (context_->IsFixed(expr)) { + if (!reachable_labels[time].contains(context_->FixedValue(expr))) { + return MarkConstraintAsFalse(ct); + } + } else { + std::vector unscaled_reachable_labels; + for (const int64_t label : reachable_labels[time]) { + unscaled_reachable_labels.push_back(GetInnerVarValue(expr, label)); + } + bool removed_values = false; + if (!context_->IntersectDomainWith( + expr.vars(0), Domain::FromValues(unscaled_reachable_labels), + &removed_values)) { + return true; + } + if (removed_values) { + context_->UpdateRuleStats("automaton: reduce variable domain"); } - new_size++; } } - if (new_size < proto.transition_tail_size()) { - proto.mutable_transition_tail()->Truncate(new_size); - proto.mutable_transition_label()->Truncate(new_size); - proto.mutable_transition_head()->Truncate(new_size); - context_->UpdateRuleStats("automaton: remove invalid transitions"); - return false; - } - return false; + return changed; } bool CpModelPresolver::PresolveReservoir(ConstraintProto* ct) { @@ -6950,6 +6901,7 @@ bool CpModelPresolver::PresolveReservoir(ConstraintProto* ct) { } } + RunPropagatorsForConstraint(*ct); return changed; } @@ -6991,6 +6943,87 @@ void CpModelPresolver::ConvertToBoolAnd() { } } +void CpModelPresolver::RunPropagatorsForConstraint(const ConstraintProto& ct) { + Model model; + + // Enable as many propagators as possible. We do not care if some propagator + // is a bit slow or if the explanation is too big: anything that improves our + // bounds is an improvement. + SatParameters local_params; + local_params.set_use_try_edge_reasoning_in_no_overlap_2d(true); + local_params.set_exploit_all_precedences(true); + local_params.set_use_hard_precedences_in_cumulative(true); + local_params.set_max_num_intervals_for_timetable_edge_finding(1000); + local_params.set_use_overload_checker_in_cumulative(true); + local_params.set_use_strong_propagation_in_disjunctive(true); + local_params.set_use_timetable_edge_finding_in_cumulative(true); + local_params.set_max_pairs_pairwise_reasoning_in_no_overlap_2d(50000); + local_params.set_use_timetabling_in_no_overlap_2d(true); + local_params.set_use_energetic_reasoning_in_no_overlap_2d(true); + local_params.set_use_area_energetic_reasoning_in_no_overlap_2d(true); + local_params.set_use_conservative_scale_overload_checker(true); + local_params.set_use_dual_scheduling_heuristics(true); + + std::vector variable_mapping; + CreateValidModelWithSingleConstraint(ct, context_, &variable_mapping, + &tmp_model_); + if (!LoadModelForPresolve(tmp_model_, std::move(local_params), context_, + &model, "single constraint")) { + return; + } + + auto* mapping = model.GetOrCreate(); + auto* integer_trail = model.GetOrCreate(); + auto* implication_graph = model.GetOrCreate(); + auto* trail = model.GetOrCreate(); + + int num_equiv = 0; + int num_changed_bounds = 0; + int num_fixed_bools = 0; + for (int var = 0; var < variable_mapping.size(); ++var) { + const int proto_var = variable_mapping[var]; + if (mapping->IsBoolean(var)) { + const Literal l = mapping->Literal(var); + if (trail->Assignment().LiteralIsFalse(l)) { + (void)context_->SetLiteralToFalse(proto_var); + ++num_fixed_bools; + continue; + } else if (trail->Assignment().LiteralIsTrue(l)) { + (void)context_->SetLiteralToTrue(proto_var); + ++num_fixed_bools; + continue; + } + // Add Boolean equivalence relations. + const Literal r = implication_graph->RepresentativeOf(l); + if (r != l) { + ++num_equiv; + const int r_var = + mapping->GetProtoVariableFromBooleanVariable(r.Variable()); + if (r_var < 0) continue; + context_->StoreBooleanEqualityRelation( + proto_var, r.IsPositive() ? r_var : NegatedRef(r_var)); + } + } else { + // Restrict variable domain. + bool changed = false; + if (!context_->IntersectDomainWith( + proto_var, + integer_trail->InitialVariableDomain(mapping->Integer(var)), + &changed)) { + return; + } + if (changed) ++num_changed_bounds; + } + } + if (num_changed_bounds > 0) { + context_->UpdateRuleStats("propagators: changed bounds", + num_changed_bounds); + } + if (num_fixed_bools > 0) { + context_->UpdateRuleStats("propagators: fixed booleans", num_fixed_bools); + } +} + // TODO(user): It might make sense to run this in parallel. The same apply for // other expansive and self-contains steps like symmetry detection, etc... void CpModelPresolver::Probe() { @@ -8858,6 +8891,308 @@ bool CpModelPresolver::ProcessEncodingFromLinear( return true; } +struct ColumnHashForDuplicateDetection { + explicit ColumnHashForDuplicateDetection( + CompactVectorVector>* _column) + : column(_column) {} + std::size_t operator()(int c) const { return absl::HashOf((*column)[c]); } + + CompactVectorVector>* column; +}; + +struct ColumnEqForDuplicateDetection { + explicit ColumnEqForDuplicateDetection( + CompactVectorVector>* _column) + : column(_column) {} + bool operator()(int a, int b) const { + if (a == b) return true; + + // We use absl::span<> comparison. + return (*column)[a] == (*column)[b]; + } + + CompactVectorVector>* column; +}; + +// Note that our symmetry-detector will also identify full permutation group +// for these columns, but it is better to handle that even before. We can +// also detect variable with different domains but with indentical columns. +void CpModelPresolver::DetectDuplicateColumns() { + if (time_limit_->LimitReached()) return; + if (context_->ModelIsUnsat()) return; + PresolveTimer timer(__FUNCTION__, logger_, time_limit_); + + const int num_vars = context_->working_model->variables().size(); + const int num_constraints = context_->working_model->constraints().size(); + + // Our current implementation require almost a full copy. + // First construct a transpose var to columns (constraint_index, coeff). + std::vector flat_vars; + std::vector> flat_terms; + CompactVectorVector> var_to_columns; + + // We will only support columns that include: + // - objective + // - linear (non-enforced part) + // - at_most_one/exactly_one/clauses (but with positive variable only). + // + // TODO(user): deal with enforcement_literal, especially bool_and. It is a bit + // annoying to have to deal with all kind of constraints. Maybe convert + // bool_and to at_most_one first? We already do that in other places. Note + // however that an at most one of size 2 means at most 2 columns can be + // identical. If we have a bool and with many term on the left, all column + // could be indentical, but we have to linearize the constraint first. + std::vector appear_in_amo(num_vars, false); + std::vector appear_in_bool_constraint(num_vars, false); + for (int c = 0; c < num_constraints; ++c) { + const ConstraintProto& ct = context_->working_model->constraints(c); + absl::Span literals; + + bool is_amo = false; + if (ct.constraint_case() == ConstraintProto::kAtMostOne) { + is_amo = true; + literals = ct.at_most_one().literals(); + } else if (ct.constraint_case() == ConstraintProto::kExactlyOne) { + is_amo = true; // That works here. + literals = ct.exactly_one().literals(); + } else if (ct.constraint_case() == ConstraintProto::kBoolOr) { + literals = ct.bool_or().literals(); + } + + if (!literals.empty()) { + for (const int lit : literals) { + // It is okay to ignore terms (the columns will not be full). + if (!RefIsPositive(lit)) continue; + if (is_amo) appear_in_amo[lit] = true; + appear_in_bool_constraint[lit] = true; + flat_vars.push_back(lit); + flat_terms.push_back({c, 1}); + } + continue; + } + + if (ct.constraint_case() == ConstraintProto::kLinear) { + const int num_terms = ct.linear().vars().size(); + for (int i = 0; i < num_terms; ++i) { + const int var = ct.linear().vars(i); + const int64_t coeff = ct.linear().coeffs(i); + flat_vars.push_back(var); + flat_terms.push_back({c, coeff}); + } + continue; + } + } + + // Use kObjectiveConstraint (-1) for the objective. + // + // TODO(user): deal with equivalent column with different objective value. + // It might not be easy to presolve, but we can at least have a single + // variable = sum of var appearing only in objective. And we can transfer the + // min cost. + if (context_->working_model->has_objective()) { + context_->WriteObjectiveToProto(); + const int num_terms = context_->working_model->objective().vars().size(); + for (int i = 0; i < num_terms; ++i) { + const int var = context_->working_model->objective().vars(i); + const int64_t coeff = context_->working_model->objective().coeffs(i); + flat_vars.push_back(var); + flat_terms.push_back({kObjectiveConstraint, coeff}); + } + } + + // Now construct the graph. + var_to_columns.ResetFromFlatMapping(flat_vars, flat_terms); + + // Find duplicate columns using an hash map. + // We only consider "full" columns. + // var -> var_representative using columns hash/comparison. + absl::flat_hash_map + duplicates( + /*capacity=*/num_vars, + ColumnHashForDuplicateDetection(&var_to_columns), + ColumnEqForDuplicateDetection(&var_to_columns)); + std::vector flat_duplicates; + std::vector flat_representatives; + for (int var = 0; var < var_to_columns.size(); ++var) { + const int size_seen = var_to_columns[var].size(); + if (size_seen == 0) continue; + if (size_seen != context_->VarToConstraints(var).size()) continue; + + // TODO(user): If we have duplicate columns appearing in Boolean constraint + // we can only easily substitute if the sum of columns is a Boolean (i.e. if + // it appear in an at most one or exactly one). Otherwise we will need to + // transform such constraint to linear, do that? + if (appear_in_bool_constraint[var] && !appear_in_amo[var]) { + context_->UpdateRuleStats( + "TODO duplicate: duplicate columns in Boolean constraints"); + continue; + } + + const auto [it, inserted] = duplicates.insert({var, var}); + if (!inserted) { + flat_duplicates.push_back(var); + flat_representatives.push_back(it->second); + } + } + + // Process duplicates. + int num_equivalent_classes = 0; + CompactVectorVector rep_to_dups; + rep_to_dups.ResetFromFlatMapping(flat_representatives, flat_duplicates); + std::vector> definition; + std::vector var_to_remove; + std::vector var_to_rep(num_vars, -1); + for (int var = 0; var < rep_to_dups.size(); ++var) { + if (rep_to_dups[var].empty()) continue; + + // Since columns are the same, we can introduce a new variable = sum all + // columns. Note that we shouldn't have any overflow here by the + // precondition on our variable domains. + // + // In the corner case where there is a lot of holes in the domain, and the + // sum domain is too complex, we skip. Hopefully this should be rare. + definition.clear(); + definition.push_back({var, 1}); + Domain domain = context_->DomainOf(var); + for (const int other_var : rep_to_dups[var]) { + definition.push_back({other_var, 1}); + domain = domain.AdditionWith(context_->DomainOf(other_var)); + if (domain.NumIntervals() > 100) break; + } + if (domain.NumIntervals() > 100) { + context_->UpdateRuleStats( + "TODO duplicate: domain of the sum is too complex"); + continue; + } + if (appear_in_amo[var]) { + domain = domain.IntersectionWith(Domain(0, 1)); + } + const int new_var = context_->NewIntVarWithDefinition( + domain, definition, /*append_constraint_to_mapping_model=*/true); + CHECK_NE(new_var, -1); + + var_to_remove.push_back(var); + CHECK_EQ(var_to_rep[var], -1); + var_to_rep[var] = new_var; + for (const int other_var : rep_to_dups[var]) { + var_to_remove.push_back(other_var); + CHECK_EQ(var_to_rep[other_var], -1); + var_to_rep[other_var] = new_var; + } + + // Deal with objective right away. + const int64_t obj_coeff = context_->ObjectiveCoeff(var); + if (obj_coeff != 0) { + context_->RemoveVariableFromObjective(var); + for (const int other_var : rep_to_dups[var]) { + CHECK_EQ(context_->ObjectiveCoeff(other_var), obj_coeff); + context_->RemoveVariableFromObjective(other_var); + } + context_->AddToObjective(new_var, obj_coeff); + } + + num_equivalent_classes++; + } + + // Lets rescan the model, and remove all variables, replacing them by + // the sum. We do that in one O(model size) pass. + if (!var_to_remove.empty()) { + absl::flat_hash_set seen; + std::vector> new_terms; + for (int c = 0; c < num_constraints; ++c) { + ConstraintProto* mutable_ct = + context_->working_model->mutable_constraints(c); + + seen.clear(); + new_terms.clear(); + + // Deal with bool case. + // TODO(user): maybe converting to linear + single code is better? + BoolArgumentProto* mutable_arg = nullptr; + if (mutable_ct->constraint_case() == ConstraintProto::kAtMostOne) { + mutable_arg = mutable_ct->mutable_at_most_one(); + } else if (mutable_ct->constraint_case() == + ConstraintProto::kExactlyOne) { + mutable_arg = mutable_ct->mutable_exactly_one(); + } else if (mutable_ct->constraint_case() == ConstraintProto::kBoolOr) { + mutable_arg = mutable_ct->mutable_bool_or(); + } + if (mutable_arg != nullptr) { + int new_size = 0; + const int num_terms = mutable_arg->literals().size(); + for (int i = 0; i < num_terms; ++i) { + const int lit = mutable_arg->literals(i); + const int rep = var_to_rep[PositiveRef(lit)]; + if (rep != -1) { + CHECK(RefIsPositive(lit)); + const auto [_, inserted] = seen.insert(rep); + if (inserted) new_terms.push_back({rep, 1}); + continue; + } + mutable_arg->set_literals(new_size, lit); + ++new_size; + } + if (new_size == num_terms) continue; // skip. + + // TODO(user): clear amo/exo of size 1. + mutable_arg->mutable_literals()->Truncate(new_size); + for (const auto [var, coeff] : new_terms) { + mutable_arg->add_literals(var); + } + context_->UpdateConstraintVariableUsage(c); + continue; + } + + // Deal with linear case. + if (mutable_ct->constraint_case() == ConstraintProto::kLinear) { + int new_size = 0; + LinearConstraintProto* mutable_linear = mutable_ct->mutable_linear(); + const int num_terms = mutable_linear->vars().size(); + for (int i = 0; i < num_terms; ++i) { + const int var = mutable_linear->vars(i); + const int64_t coeff = mutable_linear->coeffs(i); + const int rep = var_to_rep[var]; + if (rep != -1) { + const auto [_, inserted] = seen.insert(rep); + if (inserted) new_terms.push_back({rep, coeff}); + continue; + } + mutable_linear->set_vars(new_size, var); + mutable_linear->set_coeffs(new_size, coeff); + ++new_size; + } + if (new_size == num_terms) continue; // skip. + + mutable_linear->mutable_vars()->Truncate(new_size); + mutable_linear->mutable_coeffs()->Truncate(new_size); + for (const auto [var, coeff] : new_terms) { + mutable_linear->add_vars(var); + mutable_linear->add_coeffs(coeff); + } + context_->UpdateConstraintVariableUsage(c); + continue; + } + } + } + + // We removed all occurrence of "var_to_remove" so we can remove them now. + // Note that since we introduce a new variable per equivalence class, we + // remove one less for each equivalent class. + const int num_var_reduction = var_to_remove.size() - num_equivalent_classes; + for (const int var : var_to_remove) { + CHECK(context_->VarToConstraints(var).empty()); + context_->MarkVariableAsRemoved(var); + } + if (num_var_reduction > 0) { + context_->UpdateRuleStats("duplicate: removed duplicated column", + num_var_reduction); + } + + timer.AddCounter("num_equiv_classes", num_equivalent_classes); + timer.AddCounter("num_removed_vars", num_var_reduction); +} + void CpModelPresolver::DetectDuplicateConstraints() { if (time_limit_->LimitReached()) return; if (context_->ModelIsUnsat()) return; @@ -9896,36 +10231,11 @@ bool CpModelPresolver::RemoveCommonPart( } } - // TODO(user): use exactly one for the defining constraint here. - if (max_activity == min_activity + 1) { - context_->UpdateRuleStats("linear matrix: boolean common part"); - } - // Create new variable. std::sort(common_part.begin(), common_part.end()); new_var = context_->NewIntVarWithDefinition( Domain(min_activity, max_activity), common_part); - - // Create new linear constraint sum common_part = new_var - auto* new_linear = - context_->working_model->add_constraints()->mutable_linear(); - for (const auto [var, coeff] : common_part) { - new_linear->add_vars(var); - new_linear->add_coeffs(coeff); - } - new_linear->add_vars(new_var); - new_linear->add_coeffs(-1); - new_linear->add_domain(0); - new_linear->add_domain(0); - if (PossibleIntegerOverflow(*context_->working_model, new_linear->vars(), - new_linear->coeffs())) { - context_->UpdateRuleStats( - "TODO linear matrix: possible overflow in common part!"); - context_->working_model->mutable_constraints()->RemoveLast(); - return false; - } - - context_->UpdateNewConstraintsVariableUsage(); + if (new_var == -1) return false; } // Replace in each constraint the common part by gcd * multiple * new_var ! @@ -11996,6 +12306,9 @@ bool ModelCopy::ImportAndSimplifyConstraints( case ConstraintProto::kTable: if (!CopyTable(ct)) return CreateUnsatModel(c, ct); break; + case ConstraintProto::kAutomaton: + if (!CopyAutomaton(ct)) return CreateUnsatModel(c, ct); + break; case ConstraintProto::kAtMostOne: if (!CopyAtMostOne(ct)) return CreateUnsatModel(c, ct); break; @@ -12389,6 +12702,31 @@ bool ModelCopy::CopyElement(const ConstraintProto& ct) { return true; } +bool ModelCopy::CopyAutomaton(const ConstraintProto& ct) { + ConstraintProto* new_ct = context_->working_model->add_constraints(); + *new_ct = ct; + if (new_ct->automaton().vars().empty()) return true; + + auto fill_expr = [this](int var, LinearExpressionProto* expr) mutable { + if (context_->IsFixed(var)) { + expr->set_offset(context_->FixedValue(var)); + } else { + DCHECK(RefIsPositive(var)); + expr->mutable_vars()->Reserve(1); + expr->mutable_coeffs()->Reserve(1); + expr->add_vars(var); + expr->add_coeffs(1); + } + }; + + for (const int var : ct.automaton().vars()) { + fill_expr(var, new_ct->mutable_automaton()->add_exprs()); + } + new_ct->mutable_automaton()->clear_vars(); + + return true; +} + bool ModelCopy::CopyTable(const ConstraintProto& ct) { ConstraintProto* new_ct = context_->working_model->add_constraints(); if (ct.table().vars().empty() && !ct.table().exprs().empty()) { @@ -13074,6 +13412,10 @@ CpSolverStatus CpModelPresolver::Presolve() { if (context_->params().symmetry_level() > 0 && !context_->ModelIsUnsat() && !time_limit_->LimitReached() && !context_->keep_all_feasible_solutions) { + // Both kind of duplications might introduce a lot of symmetries and we + // want to do that before we even compute them. + DetectDuplicateColumns(); + DetectDuplicateConstraints(); DetectAndExploitSymmetriesInPresolve(context_); } diff --git a/ortools/sat/cp_model_presolve.h b/ortools/sat/cp_model_presolve.h index 1b1148c8d98..253a2893c0e 100644 --- a/ortools/sat/cp_model_presolve.h +++ b/ortools/sat/cp_model_presolve.h @@ -86,8 +86,9 @@ class CpModelPresolver { // Executes presolve method for the given constraint. Public for testing only. bool PresolveOneConstraint(int c); - // Public for testing only. + // Visible for testing. void RemoveEmptyConstraints(); + void DetectDuplicateColumns(); private: // A simple helper that logs the rules applied so far and return INFEASIBLE. @@ -310,6 +311,8 @@ class CpModelPresolver { // efficient than the two watcher literal scheme for clauses. Investigate! void MergeClauses(); + void RunPropagatorsForConstraint(const ConstraintProto& ct); + // Boths function are responsible for dealing with affine relations. // The second one returns false on UNSAT. void EncodeAllAffineRelations(); @@ -338,6 +341,9 @@ class CpModelPresolver { absl::flat_hash_set temp_set_; ConstraintProto temp_ct_; + // Used by RunPropagatorsForConstraint(). + CpModelProto tmp_model_; + // Use by TryToReduceCoefficientsOfLinearConstraint(). struct RdEntry { int64_t magnitude; @@ -436,6 +442,7 @@ class ModelCopy { bool CopyLinear(const ConstraintProto& ct); bool CopyLinearExpression(const LinearExpressionProto& expr, LinearExpressionProto* dst); + bool CopyAutomaton(const ConstraintProto& ct); bool CopyTable(const ConstraintProto& ct); // If we "copy" an interval for a first time, we make sure to create the diff --git a/ortools/sat/cp_model_table.cc b/ortools/sat/cp_model_table.cc index ee574610e2b..f018b6790c2 100644 --- a/ortools/sat/cp_model_table.cc +++ b/ortools/sat/cp_model_table.cc @@ -20,6 +20,7 @@ #include #include "absl/container/flat_hash_map.h" +#include "absl/container/flat_hash_set.h" #include "absl/container/inlined_vector.h" #include "absl/log/check.h" #include "absl/types/span.h" @@ -319,5 +320,56 @@ std::vector>> FullyCompressTuples( return output; } +// TODO(user): Note that if we have duplicate variables controlling different +// time point, this might not reach the fixed point. Fix? it is not that +// important as the expansion take care of this case anyway. +void PropagateAutomaton(const AutomatonConstraintProto& proto, + const PresolveContext& context, + std::vector>* states, + std::vector>* labels) { + const int n = proto.exprs_size(); + const absl::flat_hash_set final_states( + {proto.final_states().begin(), proto.final_states().end()}); + + labels->clear(); + labels->resize(n); + states->clear(); + states->resize(n + 1); + (*states)[0].insert(proto.starting_state()); + + // Forward pass. + for (int time = 0; time < n; ++time) { + for (int t = 0; t < proto.transition_tail_size(); ++t) { + const int64_t tail = proto.transition_tail(t); + const int64_t label = proto.transition_label(t); + const int64_t head = proto.transition_head(t); + if (!(*states)[time].contains(tail)) continue; + if (!context.DomainContains(proto.exprs(time), label)) continue; + if (time == n - 1 && !final_states.contains(head)) continue; + (*labels)[time].insert(label); + (*states)[time + 1].insert(head); + } + } + + // Backward pass. + for (int time = n - 1; time >= 0; --time) { + absl::flat_hash_set new_states; + absl::flat_hash_set new_labels; + for (int t = 0; t < proto.transition_tail_size(); ++t) { + const int64_t tail = proto.transition_tail(t); + const int64_t label = proto.transition_label(t); + const int64_t head = proto.transition_head(t); + + if (!(*states)[time].contains(tail)) continue; + if (!(*labels)[time].contains(label)) continue; + if (!(*states)[time + 1].contains(head)) continue; + new_labels.insert(label); + new_states.insert(tail); + } + (*labels)[time].swap(new_labels); + (*states)[time].swap(new_states); + } +} + } // namespace sat } // namespace operations_research diff --git a/ortools/sat/cp_model_table.h b/ortools/sat/cp_model_table.h index 30cc46c4317..efa1e7ccb0b 100644 --- a/ortools/sat/cp_model_table.h +++ b/ortools/sat/cp_model_table.h @@ -67,6 +67,12 @@ std::vector>> FullyCompressTuples( absl::Span domain_sizes, std::vector>* tuples); +// Fills and propagates the set of reachable states/labels. +void PropagateAutomaton(const AutomatonConstraintProto& proto, + const PresolveContext& context, + std::vector>* states, + std::vector>* labels); + } // namespace sat } // namespace operations_research diff --git a/ortools/sat/cp_model_utils.cc b/ortools/sat/cp_model_utils.cc index cdfee30103e..dfbe47bf240 100644 --- a/ortools/sat/cp_model_utils.cc +++ b/ortools/sat/cp_model_utils.cc @@ -187,7 +187,13 @@ void GetReferencesUsedByConstraint(const ConstraintProto& ct, } break; case ConstraintProto::ConstraintCase::kAutomaton: - AddIndices(ct.automaton().vars(), variables); + if (!ct.automaton().vars().empty()) { + AddIndices(ct.automaton().vars(), variables); + } else { + for (const LinearExpressionProto& expr : ct.automaton().exprs()) { + AddIndices(expr.vars(), variables); + } + } break; case ConstraintProto::ConstraintCase::kInterval: AddIndices(ct.interval().start().vars(), variables); @@ -374,7 +380,13 @@ void ApplyToAllVariableIndices(const std::function& f, } break; case ConstraintProto::ConstraintCase::kAutomaton: - APPLY_TO_REPEATED_FIELD(automaton, vars); + if (!ct->automaton().vars().empty()) { + APPLY_TO_REPEATED_FIELD(automaton, vars); + } else { + for (int i = 0; i < ct->automaton().exprs_size(); ++i) { + APPLY_TO_REPEATED_FIELD(automaton, exprs(i)->mutable_vars); + } + } break; case ConstraintProto::ConstraintCase::kInterval: APPLY_TO_REPEATED_FIELD(interval, start()->mutable_vars); @@ -792,7 +804,13 @@ uint64_t FingerprintModel(const CpModelProto& model, uint64_t seed) { fp = FingerprintRepeatedField(ct.automaton().transition_tail(), fp); fp = FingerprintRepeatedField(ct.automaton().transition_head(), fp); fp = FingerprintRepeatedField(ct.automaton().transition_label(), fp); - fp = FingerprintRepeatedField(ct.automaton().vars(), fp); + if (!ct.automaton().vars().empty()) { + fp = FingerprintRepeatedField(ct.automaton().vars(), fp); + } else { + for (const LinearExpressionProto& expr : ct.automaton().exprs()) { + fp = FingerprintExpression(expr, fp); + } + } break; case ConstraintProto::ConstraintCase::kInterval: fp = FingerprintExpression(ct.interval().start(), fp); diff --git a/ortools/sat/csharp/Constraints.cs b/ortools/sat/csharp/Constraints.cs index b708babf04f..eccadbeb5b6 100644 --- a/ortools/sat/csharp/Constraints.cs +++ b/ortools/sat/csharp/Constraints.cs @@ -173,7 +173,7 @@ public TableConstraint AddTuple(IEnumerable tuple) table.Values.Add(value); count++; } - if (count != table.Exprs.Count) + if (count != table.Vars.Count) { throw new ArgumentException("addTuple", "tuple does not have the same length as the variables"); } @@ -199,7 +199,7 @@ public TableConstraint AddTuple(IEnumerable tuple) table.Values.Add(value); count++; } - if (count != table.Exprs.Count) + if (count != table.Vars.Count) { throw new ArgumentException("addTuple", "tuple does not have the same length as the variables"); } @@ -219,7 +219,7 @@ public TableConstraint AddTuples(int[,] tuples) { TableConstraintProto table = Proto.Table; - if (tuples.GetLength(1) != table.Exprs.Count) + if (tuples.GetLength(1) != table.Vars.Count) { throw new ArgumentException("addTuples", "tuples does not have the same length as the variables"); } @@ -247,7 +247,7 @@ public TableConstraint AddTuples(long[,] tuples) { TableConstraintProto table = Proto.Table; - if (tuples.GetLength(1) != table.Exprs.Count) + if (tuples.GetLength(1) != table.Vars.Count) { throw new ArgumentException("addTuples", "tuples does not have the same length as the variables"); } diff --git a/ortools/sat/csharp/CpModel.cs b/ortools/sat/csharp/CpModel.cs index ce7041c5833..3370abd4b09 100644 --- a/ortools/sat/csharp/CpModel.cs +++ b/ortools/sat/csharp/CpModel.cs @@ -387,48 +387,49 @@ public TableConstraint AddForbiddenAssignments(IEnumerable exprs) * * * - * An automaton constraint takes a list of variables (of size n), an initial state, a set of - * final states, and a set of transitions that will be added incrementally directly on the - * returned AutomatonConstraint instance. A transition is a triplet (tail, transition, - * head), where tail and head are states, and transition is the label of an arc from - * head to tail, corresponding to the value of one variable in the list of variables. + * An automaton constraint takes a list of affine expressions (of size n), an initial + * state, a set of final states, and a set of transitions that will be added incrementally + * directly on the returned AutomatonConstraint instance. A transition is a triplet + * (tail, transition, head), where tail and head are states, + * and transition is the label of an arc from head to tail, corresponding + * to the value of one expression in the list of expressions. * * This automaton will be unrolled into a flow with n + 1 phases. Each phase contains the * possible states of the automaton. The first state contains the initial state. The last phase * contains the final states. * - * Between two consecutive phases i and i + 1, the automaton creates a set of arcs. For each - * transition (tail, label, head), it will add an arc from the state tail of phase i and - * the state head of phase i + 1. This arc labeled by the value label of the variables - * variables[i]. That is, this arc can only be selected variables[i]a is assigned the value - * label. + * Between two consecutive phases i and i + 1, the automaton creates a set of arcs. For + * each transition (tail, label, head), it will add an arc from the state + * tail of phase i and the state head of phase i + 1. This arc labeled by the + * value label of the expression expressions[i]. That is, this arc can only be + * selected expressions[i]a is assigned the value label. * - * A feasible solution of this constraint is an assignment of variables such that, starting - * from the initial state in phase 0, there is a path labeled by the values of the variables that - * ends in one of the final states in the final phase. + * A feasible solution of this constraint is an assignment of expression such that, + * starting from the initial state in phase 0, there is a path labeled by the values of the + * expressions that ends in one of the final states in the final phase. * * - * a non empty list of variables whose values correspond to the labels - * of the arcs traversed by the automaton - * the initial state of the automaton - * a non empty list of admissible final states - * an instance of the AutomatonConstraint class + * a non empty list of affine expressions (a * var + b) whose values + * correspond to the labels of the arcs traversed by the automaton the initial state of the automaton + * a non empty list of admissible final states an instance of the + * AutomatonConstraint class */ - public AutomatonConstraint AddAutomaton(IEnumerable vars, long starting_state, + public AutomatonConstraint AddAutomaton(IEnumerable expressions, long starting_state, IEnumerable final_states) { - AutomatonConstraintProto aut = new AutomatonConstraintProto(); - aut.Vars.TrySetCapacity(vars); - foreach (IntVar var in vars) + AutomatonConstraintProto automaton = new AutomatonConstraintProto(); + automaton.Vars.TrySetCapacity(expressions); + foreach (LinearExpr expr in exprs) { - aut.Vars.Add(var.Index); + automaton.Exprs.Add(GetLinearExpressionProto(expr)); } - aut.StartingState = starting_state; - aut.FinalStates.AddRange(final_states); + automaton.StartingState = starting_state; + automaton.FinalStates.AddRange(final_states); AutomatonConstraint ct = new AutomatonConstraint(model_); - ct.Proto.Automaton = aut; + ct.Proto.Automaton = automaton; return ct; } diff --git a/ortools/sat/java/CpModelTest.java b/ortools/sat/java/CpModelTest.java index fdc4454ff2d..35384b3afdf 100644 --- a/ortools/sat/java/CpModelTest.java +++ b/ortools/sat/java/CpModelTest.java @@ -520,7 +520,37 @@ public void testCpModelAddAutomaton() throws Exception { automaton.addTransition(1, 2, 2); assertThat(model.model().getConstraintsCount()).isEqualTo(1); assertThat(model.model().getConstraints(0).hasAutomaton()).isTrue(); + assertThat(model.model().getConstraints(0).getAutomaton().getExprsCount()).isEqualTo(3); + assertThat(model.model().getConstraints(0).getAutomaton().getTransitionTailCount()) + .isEqualTo(3); + assertThat(model.model().getConstraints(0).getAutomaton().getTransitionHeadCount()) + .isEqualTo(3); + assertThat(model.model().getConstraints(0).getAutomaton().getTransitionLabelCount()) + .isEqualTo(3); + assertThat(model.model().getConstraints(0).getAutomaton().getStartingState()).isEqualTo(0); + + assertThat(model.model().getConstraints(0).getAutomaton().getFinalStatesCount()).isEqualTo(2); + } + + @Test + public void testCpModelAddAutomatonLinearArgument() throws Exception { + System.out.println("testCpModelAddAutomaton"); + final CpModel model = new CpModel(); + assertNotNull(model); + + final IntVar x1 = model.newIntVar(0, 5, "x1"); + final IntVar x2 = model.newIntVar(0, 5, "x2"); + final IntVar x3 = model.newIntVar(0, 5, "x3"); + + AutomatonConstraint automaton = model.addAutomaton( + new LinearArgument[] {x1, x2, LinearExpr.constant(1), LinearExpr.affine(x3, -1, 2)}, 0, + new long[] {1, 2}); + automaton.addTransition(0, 1, 0); + automaton.addTransition(1, 1, 1); + automaton.addTransition(1, 2, 2); + assertThat(model.model().getConstraintsCount()).isEqualTo(1); assertThat(model.model().getConstraints(0).hasAutomaton()).isTrue(); + assertThat(model.model().getConstraints(0).getAutomaton().getExprsCount()).isEqualTo(4); assertThat(model.model().getConstraints(0).getAutomaton().getTransitionTailCount()) .isEqualTo(3); assertThat(model.model().getConstraints(0).getAutomaton().getTransitionHeadCount()) diff --git a/ortools/sat/linear_programming_constraint_test.cc b/ortools/sat/linear_programming_constraint_test.cc index 73ec064503d..2808ee4f3d6 100644 --- a/ortools/sat/linear_programming_constraint_test.cc +++ b/ortools/sat/linear_programming_constraint_test.cc @@ -136,6 +136,7 @@ LPProblem GeneratePermutationProblem(int size) { int CountSolutionsOfLPProblemUsingSAT(const LPProblem& problem) { Model model; + model.GetOrCreate()->set_add_lp_constraints_lazily(false); std::vector cp_variables; const int num_cp_vars = problem.num_integer_vars(); diff --git a/ortools/sat/presolve_context.cc b/ortools/sat/presolve_context.cc index 31e43a8280d..76b228604a0 100644 --- a/ortools/sat/presolve_context.cc +++ b/ortools/sat/presolve_context.cc @@ -40,6 +40,7 @@ #include "ortools/base/stl_util.h" #include "ortools/port/proto_utils.h" #include "ortools/sat/cp_model.pb.h" +#include "ortools/sat/cp_model_checker.h" #include "ortools/sat/cp_model_loader.h" #include "ortools/sat/cp_model_mapping.h" #include "ortools/sat/cp_model_utils.h" @@ -57,7 +58,7 @@ #include "ortools/util/time_limit.h" ABSL_FLAG(bool, cp_model_debug_postsolve, false, - "DEBUG ONLY. When set to true, the mappin_model.proto will contains " + "DEBUG ONLY. When set to true, the mapping_model.proto will contains " "file:line of the code that created that constraint. This is helpful " "for debugging postsolve"); @@ -80,10 +81,41 @@ int PresolveContext::NewIntVar(const Domain& domain) { } int PresolveContext::NewIntVarWithDefinition( - const Domain& domain, - absl::Span> definition) { + const Domain& domain, absl::Span> definition, + bool append_constraint_to_mapping_model) { + if (domain.Size() == 1) { + UpdateRuleStats("TODO new_var_definition : use boolean equation"); + } + const int new_var = NewIntVar(domain); + // Create new linear constraint new_var = definition. + // TODO(user): When we encounter overflow (rare), we still create a variable. + auto* new_linear = append_constraint_to_mapping_model + ? mapping_model->add_constraints()->mutable_linear() + : working_model->add_constraints()->mutable_linear(); + for (const auto [var, coeff] : definition) { + new_linear->add_vars(var); + new_linear->add_coeffs(coeff); + } + new_linear->add_vars(new_var); + new_linear->add_coeffs(-1); + new_linear->add_domain(0); + new_linear->add_domain(0); + if (PossibleIntegerOverflow(*working_model, new_linear->vars(), + new_linear->coeffs())) { + UpdateRuleStats("TODO new_var_definition : possible overflow."); + if (append_constraint_to_mapping_model) { + mapping_model->mutable_constraints()->RemoveLast(); + } else { + working_model->mutable_constraints()->RemoveLast(); + } + return -1; + } + if (!append_constraint_to_mapping_model) { + UpdateNewConstraintsVariableUsage(); + } + // We only fill the hint of the new variable if all the variable involved // in its definition have a value. if (hint_is_loaded_) { @@ -2387,12 +2419,17 @@ bool LoadModelForProbing(PresolveContext* context, Model* local_model) { // Update the domain in the current CpModelProto. context->WriteVariableDomainsToProto(); const CpModelProto& model_proto = *(context->working_model); - // Adapt some of the parameters during this probing phase. - auto* local_param = local_model->GetOrCreate(); - *local_param = context->params(); - local_param->set_use_implied_bounds(false); + SatParameters local_params = context->params(); + local_params.set_use_implied_bounds(false); + return LoadModelForPresolve(model_proto, std::move(local_params), context, + local_model, "probing"); +} +bool LoadModelForPresolve(const CpModelProto& model_proto, SatParameters params, + PresolveContext* context, Model* local_model, + absl::string_view name_for_logging) { + *local_model->GetOrCreate() = std::move(params); local_model->GetOrCreate()->MergeWithGlobalTimeLimit( context->time_limit()); local_model->Register(context->random()); @@ -2408,15 +2445,16 @@ bool LoadModelForProbing(PresolveContext* context, Model* local_model) { ExtractEncoding(model_proto, local_model); auto* sat_solver = local_model->GetOrCreate(); if (sat_solver->ModelIsUnsat()) { - return context->NotifyThatModelIsUnsat("Initial loading for probing"); + return context->NotifyThatModelIsUnsat( + absl::StrCat("Initial loading for ", name_for_logging)); } for (const ConstraintProto& ct : model_proto.constraints()) { if (mapping->ConstraintIsAlreadyLoaded(&ct)) continue; CHECK(LoadConstraint(ct, local_model)); if (sat_solver->ModelIsUnsat()) { return context->NotifyThatModelIsUnsat( - absl::StrCat("after loading constraint during probing ", - ProtobufShortDebugString(ct))); + absl::StrCat("after loading constraint during ", name_for_logging, + " ", ProtobufShortDebugString(ct))); } } encoder->AddAllImplicationsBetweenAssociatedLiterals(); @@ -2429,11 +2467,11 @@ bool LoadModelForProbing(PresolveContext* context, Model* local_model) { return true; } -template +template bool CanonicalizeLinearExpressionInternal( absl::Span enforcements, ProtoWithVarsAndCoeffs* proto, int64_t* offset, std::vector>* tmp_terms, - PresolveContext* context) { + PresolveContextT* context) { // First regroup the terms on the same variables and sum the fixed ones. // // TODO(user): Add a quick pass to skip most of the work below if the @@ -2526,6 +2564,29 @@ bool CanonicalizeLinearExpressionInternal( return remapped || proto->vars().size() < old_size; } +namespace { +bool CanonicalizeLinearExpressionNoContext(absl::Span enforcements, + LinearConstraintProto* proto) { + struct DummyContext { + bool IsFixed(int /*var*/) const { return false; } + int64_t FixedValue(int /*var*/) const { return 0; } + AffineRelation::Relation GetAffineRelation(int var) const { + return {var, 1, 0}; + } + void UpdateRuleStats(absl::string_view /*rule*/) const {} + } dummy_context; + int64_t offset = 0; + std::vector> tmp_terms; + const bool result = CanonicalizeLinearExpressionInternal( + enforcements, proto, &offset, &tmp_terms, &dummy_context); + if (offset != 0) { + FillDomainInProto(ReadDomainFromProto(*proto).AdditionWith(Domain(-offset)), + proto); + } + return result; +} +} // namespace + bool PresolveContext::CanonicalizeLinearConstraint(ConstraintProto* ct) { int64_t offset = 0; const bool result = CanonicalizeLinearExpressionInternal( @@ -2569,5 +2630,73 @@ ConstraintProto* PresolveContext::NewMappingConstraint( return new_ct; } +void CreateValidModelWithSingleConstraint(const ConstraintProto& ct, + const PresolveContext* context, + std::vector* variable_mapping, + CpModelProto* mini_model) { + mini_model->Clear(); + + *mini_model->add_constraints() = ct; + + absl::flat_hash_map inverse_interval_map; + for (const int i : UsedIntervals(ct)) { + auto [it, inserted] = + inverse_interval_map.insert({i, mini_model->constraints_size()}); + if (inserted) { + *mini_model->add_constraints() = context->working_model->constraints(i); + + // Now add end = start + size for the interval. This is not strictly + // necessary but it makes the presolve more powerful. + ConstraintProto* linear = mini_model->add_constraints(); + *linear->mutable_enforcement_literal() = ct.enforcement_literal(); + LinearConstraintProto* mutable_linear = linear->mutable_linear(); + const IntervalConstraintProto& itv = + context->working_model->constraints(i).interval(); + + mutable_linear->add_domain(0); + mutable_linear->add_domain(0); + AddLinearExpressionToLinearConstraint(itv.start(), 1, mutable_linear); + AddLinearExpressionToLinearConstraint(itv.size(), 1, mutable_linear); + AddLinearExpressionToLinearConstraint(itv.end(), -1, mutable_linear); + CanonicalizeLinearExpressionNoContext(ct.enforcement_literal(), + mutable_linear); + } + } + + absl::flat_hash_map inverse_variable_map; + for (const ConstraintProto& cur_ct : mini_model->constraints()) { + for (const int v : UsedVariables(cur_ct)) { + auto [it, inserted] = + inverse_variable_map.insert({v, mini_model->variables_size()}); + if (inserted) { + FillDomainInProto(context->DomainOf(v), mini_model->add_variables()); + } + } + } + + variable_mapping->resize(inverse_variable_map.size()); + for (const auto& [k, v] : inverse_variable_map) { + (*variable_mapping)[v] = k; + } + const auto mapping_function = [&inverse_variable_map](int* i) { + const bool is_positive = RefIsPositive(*i); + const int positive_ref = is_positive ? *i : NegatedRef(*i); + + const auto it = inverse_variable_map.find(positive_ref); + DCHECK(it != inverse_variable_map.end()); + *i = is_positive ? it->second : NegatedRef(it->second); + }; + const auto interval_mapping_function = [&inverse_interval_map](int* i) { + const auto it = inverse_interval_map.find(*i); + DCHECK(it != inverse_interval_map.end()); + *i = it->second; + }; + for (ConstraintProto& ct : *mini_model->mutable_constraints()) { + ApplyToAllVariableIndices(mapping_function, &ct); + ApplyToAllLiteralIndices(mapping_function, &ct); + ApplyToAllIntervalIndices(interval_mapping_function, &ct); + } +} + } // namespace sat } // namespace operations_research diff --git a/ortools/sat/presolve_context.h b/ortools/sat/presolve_context.h index a2adcd2db55..9fbc8b8e520 100644 --- a/ortools/sat/presolve_context.h +++ b/ortools/sat/presolve_context.h @@ -102,9 +102,13 @@ class PresolveContext { // This should replace NewIntVar() eventually in order to be able to crush // primal solution or just update the hint. + // + // By default this also create the linking constraint new_var = definition. + // Returns -1 if we couldn't create the definition due to overflow. int NewIntVarWithDefinition( const Domain& domain, - absl::Span> definition); + absl::Span> definition, + bool append_constraint_to_mapping_model = false); // Create a new bool var. // Its hint value will be the same as the value of the given clause. @@ -773,6 +777,14 @@ class PresolveContext { // that will be used for probing. Returns false if UNSAT. bool LoadModelForProbing(PresolveContext* context, Model* local_model); +bool LoadModelForPresolve(const CpModelProto& model_proto, SatParameters params, + PresolveContext* context, Model* local_model, + absl::string_view name_for_logging); + +void CreateValidModelWithSingleConstraint(const ConstraintProto& ct, + const PresolveContext* context, + std::vector* variable_mapping, + CpModelProto* mini_model); } // namespace sat } // namespace operations_research diff --git a/ortools/sat/python/cp_model.py b/ortools/sat/python/cp_model.py index 786aef5b9e8..15c81cc958a 100644 --- a/ortools/sat/python/cp_model.py +++ b/ortools/sat/python/cp_model.py @@ -1770,18 +1770,20 @@ def add_forbidden_assignments( def add_automaton( self, - transition_variables: Sequence[VariableT], + transition_expressions: Sequence[LinearExprT], starting_state: IntegralT, final_states: Sequence[IntegralT], transition_triples: Sequence[Tuple[IntegralT, IntegralT, IntegralT]], ) -> Constraint: """Adds an automaton constraint. - An automaton constraint takes a list of variables (of size *n*), an initial - state, a set of final states, and a set of transitions. A transition is a - triplet (*tail*, *transition*, *head*), where *tail* and *head* are states, - and *transition* is the label of an arc from *head* to *tail*, - corresponding to the value of one variable in the list of variables. + An automaton constraint takes a list of affine expressions (a * var + b) (of + size *n*), an initial state, a set of final states, and a set of + transitions. A transition is a triplet (*tail*, *transition*, *head*), where + *tail* and *head* are states, and *transition* is the label of an arc from + *head* to *tail*, corresponding to the value of one expression in the list + of + expressions. This automaton will be unrolled into a flow with *n* + 1 phases. Each phase contains the possible states of the automaton. The first state contains the @@ -1790,18 +1792,19 @@ def add_automaton( Between two consecutive phases *i* and *i* + 1, the automaton creates a set of arcs. For each transition (*tail*, *transition*, *head*), it will add an arc from the state *tail* of phase *i* and the state *head* of phase - *i* + 1. This arc is labeled by the value *transition* of the variables - `variables[i]`. That is, this arc can only be selected if `variables[i]` + *i* + 1. This arc is labeled by the value *transition* of the expression + `expressions[i]`. That is, this arc can only be selected if `expressions[i]` is assigned the value *transition*. - A feasible solution of this constraint is an assignment of variables such + A feasible solution of this constraint is an assignment of expressions such that, starting from the initial state in phase 0, there is a path labeled by - the values of the variables that ends in one of the final states in the + the values of the expressions that ends in one of the final states in the final phase. Args: - transition_variables: A non-empty list of variables whose values - correspond to the labels of the arcs traversed by the automaton. + transition_expressions: A non-empty list of affine expressions (a * var + + b) whose values correspond to the labels of the arcs traversed by the + automaton. starting_state: The initial state of the automaton. final_states: A non-empty list of admissible final states. transition_triples: A list of transitions for the automaton, in the @@ -1811,13 +1814,13 @@ def add_automaton( An instance of the `Constraint` class. Raises: - ValueError: if `transition_variables`, `final_states`, or + ValueError: if `transition_expressions`, `final_states`, or `transition_triples` are empty. """ - if not transition_variables: + if not transition_expressions: raise ValueError( - "add_automaton expects a non-empty transition_variables array" + "add_automaton expects a non-empty transition_expressions array" ) if not final_states: raise ValueError("add_automaton expects some final states") @@ -1827,8 +1830,8 @@ def add_automaton( ct = Constraint(self) model_ct = self.__model.constraints[ct.index] - model_ct.automaton.vars.extend( - [self.get_or_make_index(x) for x in transition_variables] + model_ct.automaton.exprs.extend( + [self.parse_linear_expression(e) for e in transition_expressions] ) model_ct.automaton.starting_state = starting_state for v in final_states: diff --git a/ortools/sat/python/cp_model_test.py b/ortools/sat/python/cp_model_test.py index 61e1aea2f5f..35b2376660c 100644 --- a/ortools/sat/python/cp_model_test.py +++ b/ortools/sat/python/cp_model_test.py @@ -723,7 +723,7 @@ def testAutomaton(self) -> None: model.add_automaton(x, 0, [2, 3], [(0, 0, 0), (0, 1, 1), (1, 2, 2), (2, 3, 3)]) self.assertLen(model.proto.variables, 5) self.assertLen(model.proto.constraints, 1) - self.assertLen(model.proto.constraints[0].automaton.vars, 5) + self.assertLen(model.proto.constraints[0].automaton.exprs, 5) self.assertLen(model.proto.constraints[0].automaton.transition_tail, 4) self.assertLen(model.proto.constraints[0].automaton.transition_head, 4) self.assertLen(model.proto.constraints[0].automaton.transition_label, 4) diff --git a/ortools/sat/table_test.cc b/ortools/sat/table_test.cc index 04555f6524b..fbdeb692e39 100644 --- a/ortools/sat/table_test.cc +++ b/ortools/sat/table_test.cc @@ -355,10 +355,10 @@ TEST(AutomatonTest, TestAutomaton) { transition_label: 1 transition_label: 1 transition_label: 0 - vars: 0 - vars: 1 - vars: 2 - vars: 3 + exprs { vars: 0 coeffs: 1 } + exprs { vars: 1 coeffs: 1 } + exprs { vars: 2 coeffs: 1 } + exprs { vars: 3 coeffs: 1 } } } )pb");