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

[CP-SAT] remove dead code

Browse Source
This commit is contained in:
Laurent Perron
2021-10-21 13:37:15 +02:00
parent 61a8fefb64
commit 4482483be3
6 changed files with 3 additions and 569 deletions
Download Patch File Download Diff File Expand all files Collapse all files

12
ortools/sat/cp_model_expand.cc
View File

@@ -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()) {

361
ortools/sat/cp_model_loader.cc
View File

@@ -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<CpModelMapping>();
auto* encoder = m->GetOrCreate<IntegerEncoder>();
std::vector<AffineExpression> times;
std::vector<IntegerValue> deltas;
std::vector<Literal> 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<CpModelMapping>();
IntegerEncoder* encoder = m->GetOrCreate<IntegerEncoder>();
IntegerTrail* integer_trail = m->GetOrCreate<IntegerTrail>();
const IntegerVariable index = mapping->Integer(ct.element().index());
const IntegerVariable target = mapping->Integer(ct.element().target());
const std::vector<IntegerVariable> vars =
mapping->Integers(ct.element().vars());
CHECK(!m->Get(IsFixed(index)));
CHECK(!m->Get(IsFixed(target)));
Domain union_of_non_constant_domains;
std::map<IntegerValue, int> 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<CpModelMapping>();
const IntegerVariable index = mapping->Integer(ct.element().index());
const IntegerVariable target = mapping->Integer(ct.element().target());
const std::vector<IntegerVariable> 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<Literal> selectors;
std::vector<IntegerVariable> 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<CpModelMapping>();
const IntegerVariable index = mapping->Integer(ct.element().index());
const IntegerVariable target = mapping->Integer(ct.element().target());
const std::vector<IntegerVariable> vars =
mapping->Integers(ct.element().vars());
CHECK(!m->Get(IsFixed(index)));
CHECK(!m->Get(IsFixed(target)));
absl::flat_hash_map<IntegerValue, Literal> 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<IntegerValue, std::vector<Literal>> value_to_literals;
const auto index_encoding = m->Add(FullyEncodeVariable(index));
IntegerTrail* integer_trail = m->GetOrCreate<IntegerTrail>();
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<Literal> 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<CpModelMapping>();
const IntegerVariable index = mapping->Integer(ct.element().index());
const IntegerVariable target = mapping->Integer(ct.element().target());
const std::vector<IntegerVariable> 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<CpModelMapping>();
const IntegerVariable index = mapping->Integer(ct.element().index());
const std::vector<Literal> 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<Literal> all_true;
std::vector<Literal> 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<CpModelMapping>();
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<IntegerVariable> vars =
mapping->Integers(ct.element().vars());
// Retrict the domain of index in case there was no presolve.
if (!m->GetOrCreate<IntegerTrail>()->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<IntegerEncoder>();
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<SatParameters>();
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<CpModelMapping>();
const std::vector<IntegerVariable> vars =
@@ -1572,26 +1240,6 @@ void LoadTableConstraint(const ConstraintProto& ct, Model* m) {
}
}
void LoadAutomatonConstraint(const ConstraintProto& ct, Model* m) {
auto* mapping = m->GetOrCreate<CpModelMapping>();
const std::vector<IntegerVariable> vars =
mapping->Integers(ct.automaton().vars());
const int num_transitions = ct.automaton().transition_tail_size();
std::vector<std::vector<int64_t>> 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<int64_t> 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<std::vector<Literal>> 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;

6
ortools/sat/cp_model_loader.h
View File

@@ -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

11
ortools/sat/sat_parameters.proto
View File

@@ -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];

165
ortools/sat/table.cc
View File

@@ -591,170 +591,5 @@ std::function<void(Model*)> LiteralTableConstraint(
};
}
std::function<void(Model*)> TransitionConstraint(
const std::vector<IntegerVariable>& vars,
const std::vector<std::vector<int64_t>>& automaton, int64_t initial_state,
const std::vector<int64_t>& final_states) {
return [=](Model* model) {
IntegerTrail* integer_trail = model->GetOrCreate<IntegerTrail>();
const int n = vars.size();
CHECK_GT(n, 0) << "No variables in TransitionConstraint().";
// Test precondition.
{
std::set<std::pair<int64_t, int64_t>> unique_transition_checker;
for (const std::vector<int64_t>& transition : automaton) {
CHECK_EQ(transition.size(), 3);
const std::pair<int64_t, int64_t> 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<absl::flat_hash_set<int64_t>> possible_values(n);
for (int time = 0; time < n; ++time) {
const auto domain = integer_trail->InitialVariableDomain(vars[time]);
for (const std::vector<int64_t>& 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<std::set<int64_t>> 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<int64_t>& 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<int64_t> new_set;
for (const std::vector<int64_t>& 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<IntegerValue, Literal> encoding;
absl::flat_hash_map<IntegerValue, Literal> in_encoding;
absl::flat_hash_map<IntegerValue, Literal> 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<Literal> tuple_literals;
std::vector<IntegerValue> in_states;
std::vector<IntegerValue> transition_values;
std::vector<IntegerValue> out_states;
for (const std::vector<int64_t>& 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<IntegerValue> s = transition_values;
gtl::STLSortAndRemoveDuplicates(&s);
encoding.clear();
if (s.size() > 1) {
std::vector<int64_t> 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<IntegerValue> 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

17
ortools/sat/table.h
View File

@@ -49,23 +49,6 @@ std::function<void(Model*)> LiteralTableConstraint(
const std::vector<std::vector<Literal>>& literal_tuples,
const std::vector<Literal>& 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<void(Model*)> TransitionConstraint(
const std::vector<IntegerVariable>& vars,
const std::vector<std::vector<int64_t>>& automaton, int64_t initial_state,
const std::vector<int64_t>& final_states);
} // namespace sat
} // namespace operations_research