diff --git a/ortools/sat/cp_model_expand.cc b/ortools/sat/cp_model_expand.cc index 292e90c2b6..df20e1879f 100644 --- a/ortools/sat/cp_model_expand.cc +++ b/ortools/sat/cp_model_expand.cc @@ -1692,9 +1692,7 @@ void ExpandCpModel(PresolveContext* context) { bool skip = false; switch (ct->constraint_case()) { case ConstraintProto::ConstraintCase::kReservoir: - if (context->params().expand_reservoir_constraints()) { - ExpandReservoir(ct, context); - } + ExpandReservoir(ct, context); break; case ConstraintProto::ConstraintCase::kIntMod: ExpandIntMod(ct, context); @@ -1709,17 +1707,13 @@ void ExpandCpModel(PresolveContext* context) { ExpandLinMin(ct, context); break; case ConstraintProto::ConstraintCase::kElement: - if (context->params().expand_element_constraints()) { - ExpandElement(ct, context); - } + ExpandElement(ct, context); break; case ConstraintProto::ConstraintCase::kInverse: ExpandInverse(ct, context); break; case ConstraintProto::ConstraintCase::kAutomaton: - if (context->params().expand_automaton_constraints()) { - ExpandAutomaton(ct, context); - } + ExpandAutomaton(ct, context); break; case ConstraintProto::ConstraintCase::kTable: if (ct->table().negated()) { diff --git a/ortools/sat/cp_model_loader.cc b/ortools/sat/cp_model_loader.cc index 929bce2ddc..5145f016d4 100644 --- a/ortools/sat/cp_model_loader.cc +++ b/ortools/sat/cp_model_loader.cc @@ -1219,338 +1219,6 @@ void LoadCumulativeConstraint(const ConstraintProto& ct, Model* m) { m->Add(Cumulative(intervals, demands, capacity)); } -void LoadReservoirConstraint(const ConstraintProto& ct, Model* m) { - auto* mapping = m->GetOrCreate(); - auto* encoder = m->GetOrCreate(); - std::vector times; - std::vector deltas; - std::vector presences; - const int size = ct.reservoir().times().size(); - for (int i = 0; i < size; ++i) { - times.push_back(mapping->Integer(ct.reservoir().times(i))); - deltas.push_back(IntegerValue(ct.reservoir().demands(i))); - if (!ct.reservoir().actives().empty()) { - presences.push_back(mapping->Literal(ct.reservoir().actives(i))); - } else { - presences.push_back(encoder->GetTrueLiteral()); - } - } - AddReservoirConstraint(times, deltas, presences, ct.reservoir().min_level(), - ct.reservoir().max_level(), m); -} - -// If a variable is constant and its value appear in no other variable domains, -// then the literal encoding the index and the one encoding the target at this -// value are equivalent. -bool DetectEquivalencesInElementConstraint(const ConstraintProto& ct, - Model* m) { - auto* mapping = m->GetOrCreate(); - IntegerEncoder* encoder = m->GetOrCreate(); - IntegerTrail* integer_trail = m->GetOrCreate(); - - const IntegerVariable index = mapping->Integer(ct.element().index()); - const IntegerVariable target = mapping->Integer(ct.element().target()); - const std::vector vars = - mapping->Integers(ct.element().vars()); - CHECK(!m->Get(IsFixed(index))); - CHECK(!m->Get(IsFixed(target))); - - Domain union_of_non_constant_domains; - std::map constant_to_num; - for (const auto literal_value : m->Add(FullyEncodeVariable(index))) { - const int i = literal_value.value.value(); - if (m->Get(IsFixed(vars[i]))) { - const IntegerValue value(m->Get(Value(vars[i]))); - constant_to_num[value]++; - } else { - union_of_non_constant_domains = union_of_non_constant_domains.UnionWith( - integer_trail->InitialVariableDomain(vars[i])); - } - } - - // Bump the number if the constant appear in union_of_non_constant_domains. - for (const auto entry : constant_to_num) { - if (union_of_non_constant_domains.Contains(entry.first.value())) { - constant_to_num[entry.first]++; - } - } - - // Use the literal from the index encoding to encode the target at the - // "unique" values. - bool is_one_to_one_mapping = true; - for (const auto literal_value : m->Add(FullyEncodeVariable(index))) { - const int i = literal_value.value.value(); - if (!m->Get(IsFixed(vars[i]))) { - is_one_to_one_mapping = false; - continue; - } - - const IntegerValue value(m->Get(Value(vars[i]))); - if (constant_to_num[value] == 1) { - const Literal r = literal_value.literal; - encoder->AssociateToIntegerEqualValue(r, target, value); - } else { - is_one_to_one_mapping = false; - } - } - - return is_one_to_one_mapping; -} - -// TODO(user): Be more efficient when the element().vars() are constants. -// Ideally we should avoid creating them as integer variable since we don't -// use them. -void LoadElementConstraintBounds(const ConstraintProto& ct, Model* m) { - auto* mapping = m->GetOrCreate(); - const IntegerVariable index = mapping->Integer(ct.element().index()); - const IntegerVariable target = mapping->Integer(ct.element().target()); - const std::vector vars = - mapping->Integers(ct.element().vars()); - CHECK(!m->Get(IsFixed(index))); - - // We always fully encode the index on an element constraint. - const auto encoding = m->Add(FullyEncodeVariable((index))); - std::vector selectors; - std::vector possible_vars; - for (const auto literal_value : encoding) { - const int i = literal_value.value.value(); - CHECK_GE(i, 0); - CHECK_LT(i, vars.size()); - possible_vars.push_back(vars[i]); - selectors.push_back(literal_value.literal); - const Literal r = literal_value.literal; - - if (vars[i] == target) continue; - if (m->Get(IsFixed(target))) { - const int64_t value = m->Get(Value(target)); - m->Add(ImpliesInInterval(r, vars[i], value, value)); - } else if (m->Get(IsFixed(vars[i]))) { - const int64_t value = m->Get(Value(vars[i])); - m->Add(ImpliesInInterval(r, target, value, value)); - } else { - m->Add(ConditionalLowerOrEqualWithOffset(vars[i], target, 0, r)); - m->Add(ConditionalLowerOrEqualWithOffset(target, vars[i], 0, r)); - } - } - - if (!m->Get(IsFixed(target))) { - m->Add(PartialIsOneOfVar(target, possible_vars, selectors)); - } -} - -// Arc-Consistent encoding of the element constraint as SAT clauses. -// The constraint enforces vars[index] == target. -// -// The AC propagation can be decomposed in three rules: -// Rule 1: dom(index) == i => dom(vars[i]) == dom(target). -// Rule 2: dom(target) \subseteq \Union_{i \in dom(index)} dom(vars[i]). -// Rule 3: dom(index) \subseteq { i | |dom(vars[i]) \inter dom(target)| > 0 }. -// -// We encode this in a way similar to the table constraint, except that the -// set of admissible tuples is not explicit. -// First, we add Booleans selected[i][value] <=> (index == i /\ vars[i] == -// value). Rules 1 and 2 are enforced by target == value <=> \Or_{i} -// selected[i][value]. Rule 3 is enforced by index == i <=> \Or_{value} -// selected[i][value]. -void LoadElementConstraintAC(const ConstraintProto& ct, Model* m) { - auto* mapping = m->GetOrCreate(); - const IntegerVariable index = mapping->Integer(ct.element().index()); - const IntegerVariable target = mapping->Integer(ct.element().target()); - const std::vector vars = - mapping->Integers(ct.element().vars()); - CHECK(!m->Get(IsFixed(index))); - CHECK(!m->Get(IsFixed(target))); - - absl::flat_hash_map target_map; - const auto target_encoding = m->Add(FullyEncodeVariable(target)); - for (const auto literal_value : target_encoding) { - target_map[literal_value.value] = literal_value.literal; - } - - // For i \in index and value in vars[i], make (index == i /\ vars[i] == value) - // literals and store them by value in vectors. - absl::flat_hash_map> value_to_literals; - const auto index_encoding = m->Add(FullyEncodeVariable(index)); - IntegerTrail* integer_trail = m->GetOrCreate(); - for (const auto literal_value : index_encoding) { - const int i = literal_value.value.value(); - const Literal i_lit = literal_value.literal; - - // Special case where vars[i] == value /\ i_lit is actually i_lit. - if (m->Get(IsFixed(vars[i]))) { - value_to_literals[integer_trail->LowerBound(vars[i])].push_back(i_lit); - continue; - } - - const auto var_encoding = m->Add(FullyEncodeVariable(vars[i])); - std::vector var_selected_literals; - for (const auto var_literal_value : var_encoding) { - const IntegerValue value = var_literal_value.value; - const Literal var_is_value = var_literal_value.literal; - - if (!gtl::ContainsKey(target_map, value)) { - // No need to add to value_to_literals, selected[i][value] is always - // false. - m->Add(Implication(i_lit, var_is_value.Negated())); - continue; - } - - const Literal var_is_value_and_selected = - Literal(m->Add(NewBooleanVariable()), true); - m->Add(ReifiedBoolAnd({i_lit, var_is_value}, var_is_value_and_selected)); - value_to_literals[value].push_back(var_is_value_and_selected); - var_selected_literals.push_back(var_is_value_and_selected); - } - // index == i <=> \Or_{value} selected[i][value]. - m->Add(ReifiedBoolOr(var_selected_literals, i_lit)); - } - - // target == value <=> \Or_{i \in index} (vars[i] == value /\ index == i). - for (const auto& entry : target_map) { - const IntegerValue value = entry.first; - const Literal target_is_value = entry.second; - - if (!gtl::ContainsKey(value_to_literals, value)) { - m->Add(ClauseConstraint({target_is_value.Negated()})); - } else { - m->Add(ReifiedBoolOr(value_to_literals[value], target_is_value)); - } - } -} - -namespace { - -// This Boolean encoding is enough for consistency, but does not propagate as -// much as LoadElementConstraintAC(). However, setting any of the non-propagated -// Booleans to its "wrong" value will result directly in a conflict, so the -// solver will easily learn an AC encoding... -// -// The advantage is that this does not introduce extra BooleanVariables. -void LoadElementConstraintHalfAC(const ConstraintProto& ct, Model* m) { - auto* mapping = m->GetOrCreate(); - const IntegerVariable index = mapping->Integer(ct.element().index()); - const IntegerVariable target = mapping->Integer(ct.element().target()); - const std::vector vars = - mapping->Integers(ct.element().vars()); - CHECK(!m->Get(IsFixed(index))); - CHECK(!m->Get(IsFixed(target))); - - m->Add(FullyEncodeVariable(target)); - for (const auto value_literal : m->Add(FullyEncodeVariable(index))) { - const int i = value_literal.value.value(); - m->Add(FullyEncodeVariable(vars[i])); - LoadEquivalenceAC({value_literal.literal}, IntegerValue(1), vars[i], - IntegerValue(-1), target, IntegerValue(0), m); - } -} - -void LoadBooleanElement(const ConstraintProto& ct, Model* m) { - auto* mapping = m->GetOrCreate(); - const IntegerVariable index = mapping->Integer(ct.element().index()); - const std::vector literals = mapping->Literals(ct.element().vars()); - const Literal target = mapping->Literal(ct.element().target()); - - if (m->Get(IsFixed(index))) { - m->Add(Equality(target, literals[m->Get(Value(index))])); - return; - } - - std::vector all_true; - std::vector all_false; - for (const auto value_literal : m->Add(FullyEncodeVariable(index))) { - const Literal a_lit = literals[value_literal.value.value()]; - const Literal i_lit = value_literal.literal; - m->Add(ClauseConstraint({i_lit.Negated(), a_lit.Negated(), target})); - m->Add(ClauseConstraint({i_lit.Negated(), a_lit, target.Negated()})); - all_true.push_back(a_lit.Negated()); - all_false.push_back(a_lit); - } - all_true.push_back(target); - all_false.push_back(target.Negated()); - m->Add(ClauseConstraint(all_true)); - m->Add(ClauseConstraint(all_false)); - // TODO(user): Investigate filtering this with active literals. -} - -} // namespace - -void LoadElementConstraint(const ConstraintProto& ct, Model* m) { - auto* mapping = m->GetOrCreate(); - const IntegerVariable index = mapping->Integer(ct.element().index()); - - bool boolean_array = true; - for (const int ref : ct.element().vars()) { - if (!mapping->IsBoolean(ref)) { - boolean_array = false; - break; - } - } - if (boolean_array && !mapping->IsBoolean(ct.element().target())) { - // Should have been reduced but presolve. - VLOG(1) << "Fix boolean_element not propagated on target"; - boolean_array = false; - } - - // TODO(user): Move this to presolve. Leads to a larger discussion on - // adding full encoding to model during presolve. - if (boolean_array) { - LoadBooleanElement(ct, m); - return; - } - - const IntegerVariable target = mapping->Integer(ct.element().target()); - const std::vector vars = - mapping->Integers(ct.element().vars()); - - // Retrict the domain of index in case there was no presolve. - if (!m->GetOrCreate()->UpdateInitialDomain( - index, Domain(0, vars.size() - 1))) { - return; - } - - // This returns true if there is nothing else to do after the equivalences - // of the form (index literal <=> target_literal) have been added. - if (!m->Get(IsFixed(index)) && !m->Get(IsFixed(target)) && - DetectEquivalencesInElementConstraint(ct, m)) { - return; - } - - // Special case when index is fixed. - if (m->Get(IsFixed(index))) { - m->Add(Equality(target, vars[m->Get(Value(index))])); - return; - } - - // Special case when target is fixed. - if (m->Get(IsFixed(target))) { - return LoadElementConstraintBounds(ct, m); - } - - IntegerEncoder* encoder = m->GetOrCreate(); - const bool target_is_AC = encoder->VariableIsFullyEncoded(target); - - int num_AC_variables = 0; - const int num_vars = ct.element().vars().size(); - for (const int v : ct.element().vars()) { - IntegerVariable variable = mapping->Integer(v); - const bool is_full = - m->Get(IsFixed(variable)) || encoder->VariableIsFullyEncoded(variable); - if (is_full) num_AC_variables++; - } - - const SatParameters& params = *m->GetOrCreate(); - if (params.boolean_encoding_level() > 0 && - (target_is_AC || num_AC_variables >= num_vars - 1)) { - if (params.boolean_encoding_level() > 1) { - LoadElementConstraintAC(ct, m); - } else { - LoadElementConstraintHalfAC(ct, m); - } - } else { - LoadElementConstraintBounds(ct, m); - } -} - void LoadTableConstraint(const ConstraintProto& ct, Model* m) { auto* mapping = m->GetOrCreate(); const std::vector vars = @@ -1572,26 +1240,6 @@ void LoadTableConstraint(const ConstraintProto& ct, Model* m) { } } -void LoadAutomatonConstraint(const ConstraintProto& ct, Model* m) { - auto* mapping = m->GetOrCreate(); - const std::vector vars = - mapping->Integers(ct.automaton().vars()); - - const int num_transitions = ct.automaton().transition_tail_size(); - std::vector> transitions; - transitions.reserve(num_transitions); - for (int i = 0; i < num_transitions; ++i) { - transitions.push_back({ct.automaton().transition_tail(i), - ct.automaton().transition_label(i), - ct.automaton().transition_head(i)}); - } - - const int64_t starting_state = ct.automaton().starting_state(); - const std::vector final_states = - ValuesFromProto(ct.automaton().final_states()); - m->Add(TransitionConstraint(vars, transitions, starting_state, final_states)); -} - // From vector of n IntegerVariables, returns an n x n matrix of Literal // such that matrix[i][j] is the Literal corresponding to vars[i] == j. std::vector> GetSquareMatrixFromIntegerVariables( @@ -1701,18 +1349,9 @@ bool LoadConstraint(const ConstraintProto& ct, Model* m) { case ConstraintProto::ConstraintProto::kCumulative: LoadCumulativeConstraint(ct, m); return true; - case ConstraintProto::ConstraintProto::kReservoir: - LoadReservoirConstraint(ct, m); - return true; - case ConstraintProto::ConstraintProto::kElement: - LoadElementConstraint(ct, m); - return true; case ConstraintProto::ConstraintProto::kTable: LoadTableConstraint(ct, m); return true; - case ConstraintProto::ConstraintProto::kAutomaton: - LoadAutomatonConstraint(ct, m); - return true; case ConstraintProto::ConstraintProto::kCircuit: LoadCircuitConstraint(ct, m); return true; diff --git a/ortools/sat/cp_model_loader.h b/ortools/sat/cp_model_loader.h index 18b7bc41d5..e25066ac17 100644 --- a/ortools/sat/cp_model_loader.h +++ b/ortools/sat/cp_model_loader.h @@ -105,16 +105,10 @@ void LoadIntMaxConstraint(const ConstraintProto& ct, Model* m); void LoadNoOverlapConstraint(const ConstraintProto& ct, Model* m); void LoadNoOverlap2dConstraint(const ConstraintProto& ct, Model* m); void LoadCumulativeConstraint(const ConstraintProto& ct, Model* m); -void LoadReservoirConstraint(const ConstraintProto& ct, Model* m); -void LoadElementConstraintBounds(const ConstraintProto& ct, Model* m); -void LoadElementConstraintAC(const ConstraintProto& ct, Model* m); -void LoadElementConstraint(const ConstraintProto& ct, Model* m); void LoadTableConstraint(const ConstraintProto& ct, Model* m); -void LoadAutomatonConstraint(const ConstraintProto& ct, Model* m); void LoadCircuitConstraint(const ConstraintProto& ct, Model* m); void LoadRoutesConstraint(const ConstraintProto& ct, Model* m); void LoadCircuitCoveringConstraint(const ConstraintProto& ct, Model* m); -void LoadInverseConstraint(const ConstraintProto& ct, Model* m); } // namespace sat } // namespace operations_research diff --git a/ortools/sat/sat_parameters.proto b/ortools/sat/sat_parameters.proto index 73fac30121..9c6d886451 100644 --- a/ortools/sat/sat_parameters.proto +++ b/ortools/sat/sat_parameters.proto @@ -463,13 +463,6 @@ message SatParameters { optional bool cp_model_use_sat_presolve = 93 [default = true]; optional bool use_sat_inprocessing = 163 [default = false]; - // If true, the element constraints are expanded into many - // linear constraints of the form (index == i) => (element[i] == target). - optional bool expand_element_constraints = 140 [default = true]; - - // If true, the automaton constraints are expanded. - optional bool expand_automaton_constraints = 143 [default = true]; - // If true, the positive table constraints are expanded. // Note that currently, negative table constraints are always expanded. optional bool expand_table_constraints = 158 [default = true]; @@ -478,10 +471,6 @@ message SatParameters { // Permutations (#Variables = #Values) are always expanded. optional bool expand_alldiff_constraints = 170 [default = false]; - // If true, expand the reservoir constraints by creating booleans for all - // possible precedences between event and encoding the constraint. - optional bool expand_reservoir_constraints = 182 [default = true]; - // 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]; diff --git a/ortools/sat/table.cc b/ortools/sat/table.cc index ccde496054..a9b718c68c 100644 --- a/ortools/sat/table.cc +++ b/ortools/sat/table.cc @@ -591,170 +591,5 @@ std::function LiteralTableConstraint( }; } -std::function TransitionConstraint( - const std::vector& vars, - const std::vector>& automaton, int64_t initial_state, - const std::vector& final_states) { - return [=](Model* model) { - IntegerTrail* integer_trail = model->GetOrCreate(); - const int n = vars.size(); - CHECK_GT(n, 0) << "No variables in TransitionConstraint()."; - - // Test precondition. - { - std::set> unique_transition_checker; - for (const std::vector& transition : automaton) { - CHECK_EQ(transition.size(), 3); - const std::pair p{transition[0], transition[1]}; - CHECK(!gtl::ContainsKey(unique_transition_checker, p)) - << "Duplicate outgoing transitions with value " << transition[1] - << " from state " << transition[0] << "."; - unique_transition_checker.insert(p); - } - } - - // Construct a table with the possible values of each vars. - std::vector> possible_values(n); - for (int time = 0; time < n; ++time) { - const auto domain = integer_trail->InitialVariableDomain(vars[time]); - for (const std::vector& transition : automaton) { - // TODO(user): quadratic algo, improve! - if (domain.Contains(transition[1])) { - possible_values[time].insert(transition[1]); - } - } - } - - // Compute the set of reachable state at each time point. - std::vector> reachable_states(n + 1); - reachable_states[0].insert(initial_state); - reachable_states[n] = {final_states.begin(), final_states.end()}; - - // Forward. - // - // TODO(user): filter using the domain of vars[time] that may not contain - // all the possible transitions. - for (int time = 0; time + 1 < n; ++time) { - for (const std::vector& transition : automaton) { - if (!gtl::ContainsKey(reachable_states[time], transition[0])) continue; - if (!gtl::ContainsKey(possible_values[time], transition[1])) continue; - reachable_states[time + 1].insert(transition[2]); - } - } - - // Backward. - for (int time = n - 1; time > 0; --time) { - std::set new_set; - for (const std::vector& transition : automaton) { - if (!gtl::ContainsKey(reachable_states[time], transition[0])) continue; - if (!gtl::ContainsKey(possible_values[time], transition[1])) continue; - if (!gtl::ContainsKey(reachable_states[time + 1], transition[2])) - continue; - new_set.insert(transition[0]); - } - reachable_states[time].swap(new_set); - } - - // We will model at each time step the current automaton state using Boolean - // variables. We will have n+1 time step. At time zero, we start in the - // initial state, and at time n we should be in one of the final states. We - // don't need to create Booleans at at time when there is just one possible - // state (like at time zero). - absl::flat_hash_map encoding; - absl::flat_hash_map in_encoding; - absl::flat_hash_map out_encoding; - 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 - // given time. - std::vector tuple_literals; - std::vector in_states; - std::vector transition_values; - std::vector out_states; - for (const std::vector& transition : automaton) { - if (!gtl::ContainsKey(reachable_states[time], transition[0])) continue; - if (!gtl::ContainsKey(possible_values[time], transition[1])) continue; - if (!gtl::ContainsKey(reachable_states[time + 1], transition[2])) - 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 - // Boolean variable instead of creating a new one! - tuple_literals.push_back( - Literal(model->Add(NewBooleanVariable()), true)); - in_states.push_back(IntegerValue(transition[0])); - - transition_values.push_back(IntegerValue(transition[1])); - - // On the last step we don't need to distinguish the output states, so - // we use zero. - out_states.push_back(time + 1 == n ? IntegerValue(0) - : IntegerValue(transition[2])); - } - - // Fully instantiate vars[time]. - // Tricky: because we started adding constraints that can propagate, the - // possible values returned by encoding might not contains all the value - // computed in transition_values. - { - std::vector s = transition_values; - gtl::STLSortAndRemoveDuplicates(&s); - - encoding.clear(); - if (s.size() > 1) { - std::vector values; - values.reserve(s.size()); - for (IntegerValue v : s) values.push_back(v.value()); - integer_trail->UpdateInitialDomain(vars[time], - Domain::FromValues(values)); - model->Add(FullyEncodeVariable(vars[time])); - encoding = GetEncoding(vars[time], model); - } else { - // Fix vars[time] to its unique possible value. - CHECK_EQ(s.size(), 1); - const int64_t unique_value = s.begin()->value(); - model->Add(LowerOrEqual(vars[time], unique_value)); - model->Add(GreaterOrEqual(vars[time], unique_value)); - } - } - - // For each possible out states, create one Boolean variable. - { - std::vector s = out_states; - gtl::STLSortAndRemoveDuplicates(&s); - - out_encoding.clear(); - if (s.size() == 2) { - const BooleanVariable var = model->Add(NewBooleanVariable()); - out_encoding[s.front()] = Literal(var, true); - out_encoding[s.back()] = Literal(var, false); - } else if (s.size() > 1) { - for (const IntegerValue state : s) { - const Literal l = Literal(model->Add(NewBooleanVariable()), true); - out_encoding[state] = l; - } - } - } - - // Now we link everything together. - // - // Note that we do not need the ExactlyOneConstraint(tuple_literals) - // because it is already implicitely encoded since we have exactly one - // transition value. - if (!in_encoding.empty()) { - ProcessOneColumn(tuple_literals, in_states, in_encoding, {}, model); - } - if (!encoding.empty()) { - ProcessOneColumn(tuple_literals, transition_values, encoding, {}, - model); - } - if (!out_encoding.empty()) { - ProcessOneColumn(tuple_literals, out_states, out_encoding, {}, model); - } - in_encoding = out_encoding; - } - }; -} - } // namespace sat } // namespace operations_research diff --git a/ortools/sat/table.h b/ortools/sat/table.h index e81e7d2490..c408266f02 100644 --- a/ortools/sat/table.h +++ b/ortools/sat/table.h @@ -49,23 +49,6 @@ std::function LiteralTableConstraint( const std::vector>& literal_tuples, const std::vector& line_literals); -// Given an automaton defined by a set of 3-tuples: -// (state, transition_with_value_as_label, next_state) -// this accepts the sequences of vars.size() variables that are recognized by -// this automaton. That is: -// - We start from the initial state. -// - For each variable, we move along the transition labeled by this variable -// value. Moreover, the variable must take a value that correspond to a -// feasible transition. -// - We only accept sequences that ends in one of the final states. -// -// We CHECK that there is only one possible transition for a state/value pair. -// See the test for some examples. -std::function TransitionConstraint( - const std::vector& vars, - const std::vector>& automaton, int64_t initial_state, - const std::vector& final_states); - } // namespace sat } // namespace operations_research