fix a bug with optional integer variables in sat; change reason protocol

2017-11-20 11:35:29 +01:00
parent 420e261f0c
commit 86cd5bd83f
6 changed files with 132 additions and 159 deletions
--- a/ortools/sat/circuit.cc
+++ b/ortools/sat/circuit.cc
@@ -22,13 +22,13 @@
 namespace operations_research {
 namespace sat {

-CircuitPropagator::CircuitPropagator(
-    std::vector<std::vector<LiteralIndex>> graph, Options options, Trail* trail)
+CircuitPropagator::CircuitPropagator(std::vector<std::vector<Literal>> graph,
+                                     Options options, Model* model)
    : num_nodes_(graph.size()),
      graph_(std::move(graph)),
      options_(options),
-      trail_(trail),
-      assignment_(trail->Assignment()) {
+      trail_(model->GetOrCreate<Trail>()),
+      assignment_(trail_->Assignment()) {
  // TODO(user): add a way to properly handle trivially UNSAT cases.
  // For now we just check that they don't occur at construction.
  CHECK_GT(num_nodes_, 1)
@@ -39,7 +39,7 @@ CircuitPropagator::CircuitPropagator(
  must_be_in_cycle_.resize(num_nodes_);
  std::unordered_map<LiteralIndex, int> literal_to_watch_index;
  for (int tail = 0; tail < num_nodes_; ++tail) {
-    if (LiteralIndexIsFalse(graph_[tail][tail])) {
+    if (assignment_.LiteralIsFalse(graph_[tail][tail])) {
      // For the multiple_subcircuit_through_zero case, must_be_in_cycle_ will
      // be const and only contains zero.
      if (tail == 0 || !options_.multiple_subcircuit_through_zero) {
@@ -47,9 +47,9 @@ CircuitPropagator::CircuitPropagator(
      }
    }
    for (int head = 0; head < num_nodes_; ++head) {
-      LiteralIndex index = graph_[tail][head];
-      if (LiteralIndexIsFalse(index)) continue;
-      if (LiteralIndexIsTrue(index)) {
+      Literal literal = graph_[tail][head];
+      if (assignment_.LiteralIsFalse(literal)) continue;
+      if (assignment_.LiteralIsTrue(literal)) {
        CHECK_EQ(next_[tail], -1)
            << "Trivially UNSAT or duplicate arcs while adding " << tail
            << " -> " << head;
@@ -61,13 +61,14 @@ CircuitPropagator::CircuitPropagator(
      }

      // Tricky: For self-arc, we watch instead when the arc become false.
-      if (tail == head) index = Literal(index).NegatedIndex();
+      if (tail == head) literal = literal.Negated();

-      int watch_index = FindWithDefault(literal_to_watch_index, index, -1);
+      int watch_index =
+          FindWithDefault(literal_to_watch_index, literal.Index(), -1);
      if (watch_index == -1) {
        watch_index = watch_index_to_literal_.size();
-        literal_to_watch_index[index] = watch_index;
-        watch_index_to_literal_.push_back(Literal(index));
+        literal_to_watch_index[literal.Index()] = watch_index;
+        watch_index_to_literal_.push_back(literal);
        watch_index_to_arcs_.push_back(std::vector<Arc>());
      }
      watch_index_to_arcs_[watch_index].push_back({tail, head});
@@ -214,7 +215,7 @@ bool CircuitPropagator::Propagate() {
      const int node = must_be_in_cycle_[i];
      if (!in_current_path_[node]) {
        miss_some_nodes = true;
-        extra_reason = graph_[node][node];
+        extra_reason = graph_[node][node].Index();
        break;
      }
    }
@@ -232,17 +233,17 @@ bool CircuitPropagator::Propagate() {
      // We have an unclosed path. Propagate the fact that it cannot
      // be closed into a cycle, i.e. not(end_node -> start_node).
      if (start_node != end_node) {
-        const LiteralIndex literal_index = graph_[end_node][start_node];
-        if (LiteralIndexIsFalse(literal_index)) continue;
-        CHECK_NE(literal_index, kTrueLiteralIndex);
+        const Literal literal = graph_[end_node][start_node];
+        if (assignment_.LiteralIsFalse(literal)) continue;

        std::vector<Literal>* reason = trail_->GetEmptyVectorToStoreReason();
        FillReasonForPath(start_node, reason);
        if (extra_reason != kFalseLiteralIndex) {
          reason->push_back(Literal(extra_reason));
        }
-        return trail_->EnqueueWithStoredReason(
-            Literal(literal_index).Negated());
+        const bool ok = trail_->EnqueueWithStoredReason(literal.Negated());
+        if (!ok) return false;
+        continue;
      }
    }

@@ -253,7 +254,7 @@ bool CircuitPropagator::Propagate() {
    BooleanVariable variable_with_same_reason = kNoBooleanVariable;
    for (int node = 0; node < num_nodes_; ++node) {
      if (in_current_path_[node]) continue;
-      if (LiteralIndexIsTrue(graph_[node][node])) continue;
+      if (assignment_.LiteralIsTrue(graph_[node][node])) continue;

      // This shouldn't happen because ExactlyOnePerRowAndPerColumn() should
      // have executed first and propagated graph_[node][node] to false.
@@ -262,10 +263,9 @@ bool CircuitPropagator::Propagate() {
      // We should have detected that above (miss_some_nodes == true). But we
      // still need this for corner cases where the same literal is used for
      // many arcs, and we just propagated it here.
-      if (LiteralIndexIsFalse(graph_[node][node])) {
-        CHECK_NE(graph_[node][node], kFalseLiteralIndex);
+      if (assignment_.LiteralIsFalse(graph_[node][node])) {
        FillReasonForPath(start_node, trail_->MutableConflict());
-        trail_->MutableConflict()->push_back(Literal(graph_[node][node]));
+        trail_->MutableConflict()->push_back(graph_[node][node]);
        return false;
      }

@@ -274,7 +274,8 @@ bool CircuitPropagator::Propagate() {
      if (variable_with_same_reason == kNoBooleanVariable) {
        variable_with_same_reason = literal.Variable();
        FillReasonForPath(start_node, trail_->GetEmptyVectorToStoreReason());
-        CHECK(trail_->EnqueueWithStoredReason(literal));
+        const bool ok = trail_->EnqueueWithStoredReason(literal);
+        if (!ok) return false;
      } else {
        trail_->EnqueueWithSameReasonAs(literal, variable_with_same_reason);
      }
@@ -283,52 +284,6 @@ bool CircuitPropagator::Propagate() {
  return true;
 }

-std::function<void(Model*)> ExactlyOnePerRowAndPerColumn(
-    const std::vector<std::vector<LiteralIndex>>& square_matrix,
-    bool ignore_row_and_col_zero) {
-  return [=](Model* model) {
-    int n = square_matrix.size();
-    int num_trivially_false = 0;
-    Trail* trail = model->GetOrCreate<Trail>();
-    std::vector<Literal> exactly_one_constraint;
-    for (const bool transpose : {false, true}) {
-      for (int i = ignore_row_and_col_zero ? 1 : 0; i < n; ++i) {
-        int num_true = 0;
-        exactly_one_constraint.clear();
-        for (int j = 0; j < n; ++j) {
-          CHECK_EQ(n, square_matrix[i].size());
-          const LiteralIndex index =
-              transpose ? square_matrix[j][i] : square_matrix[i][j];
-          if (index == kFalseLiteralIndex) continue;
-          if (index == kTrueLiteralIndex) {
-            ++num_true;
-            continue;
-          }
-          exactly_one_constraint.push_back(Literal(index));
-        }
-        if (num_true > 1) {
-          LOG(WARNING) << "UNSAT in ExactlyOnePerRowAndPerColumn().";
-          return model->GetOrCreate<SatSolver>()->NotifyThatModelIsUnsat();
-        }
-        CHECK_LE(num_true, 1);
-        if (num_true == 1) {
-          for (const Literal l : exactly_one_constraint) {
-            if (!trail->Assignment().VariableIsAssigned(l.Variable())) {
-              ++num_trivially_false;
-              trail->EnqueueWithUnitReason(l.Negated());
-            }
-          }
-        } else {
-          model->Add(ExactlyOneConstraint(exactly_one_constraint));
-        }
-      }
-    }
-    if (num_trivially_false > 0) {
-      LOG(INFO) << "Num extra fixed literal: " << num_trivially_false;
-    }
-  };
-}
-
 CircuitCoveringPropagator::CircuitCoveringPropagator(
    std::vector<std::vector<Literal>> graph,
    const std::vector<int>& distinguished_nodes, Model* model)
@@ -386,7 +341,6 @@ bool CircuitCoveringPropagator::IncrementalPropagate(
 void CircuitCoveringPropagator::FillFixedPathInReason(
    int start, int end, std::vector<Literal>* reason) {
  reason->clear();
-
  int current = start;
  do {
    DCHECK_NE(next_[current], -1);
@@ -403,15 +357,17 @@ bool CircuitCoveringPropagator::Propagate() {
  for (const auto& arc : fixed_arcs_) {
    // Two arcs go out of arc.first, forbidden.
    if (next_[arc.first] != -1) {
-      *trail_->MutableConflict() = {graph_[arc.first][next_[arc.first]],
-                                    graph_[arc.first][arc.second]};
+      *trail_->MutableConflict() = {
+          graph_[arc.first][next_[arc.first]].Negated(),
+          graph_[arc.first][arc.second].Negated()};
      return false;
    }
    next_[arc.first] = arc.second;
    // Two arcs come into arc.second, forbidden.
    if (prev_[arc.second] != -1) {
-      *trail_->MutableConflict() = {graph_[prev_[arc.second]][arc.second],
-                                    graph_[arc.first][arc.second]};
+      *trail_->MutableConflict() = {
+          graph_[prev_[arc.second]][arc.second].Negated(),
+          graph_[arc.first][arc.second].Negated()};
      return false;
    }
    prev_[arc.second] = arc.first;
@@ -472,28 +428,57 @@ bool CircuitCoveringPropagator::Propagate() {
  return true;
 }

-std::function<void(Model*)> CircuitCovering(
-    const std::vector<std::vector<LiteralIndex>>& next,
-    const std::vector<int>& distinguished_nodes) {
-  return [&next, &distinguished_nodes](Model* model) {
-    const int num_nodes = next.size();
-    // Convert LiteralIndex to Literal.
-    IntegerEncoder* encoder = model->GetOrCreate<IntegerEncoder>();
-    std::vector<std::vector<Literal>> graph(num_nodes,
-                                            std::vector<Literal>(num_nodes));
-    for (int row = 0; row < num_nodes; row++) {
-      for (int col = 0; col < num_nodes; col++) {
-        if (next[row][col] == kTrueLiteralIndex) {
-          graph[row][col] = encoder->GetLiteralTrue();
-        } else if (next[row][col] == kFalseLiteralIndex) {
-          graph[row][col] = encoder->GetLiteralTrue().Negated();
-        } else {
-          graph[row][col] = Literal(next[row][col]);
+std::function<void(Model*)> ExactlyOnePerRowAndPerColumn(
+    const std::vector<std::vector<Literal>>& graph,
+    bool ignore_row_and_col_zero) {
+  return [=](Model* model) {
+    std::vector<Literal> exactly_one_constraint;
+    for (const bool transpose : {false, true}) {
+      const int n = graph.size();
+      for (int i = ignore_row_and_col_zero ? 1 : 0; i < n; ++i) {
+        exactly_one_constraint.clear();
+        for (int j = 0; j < n; ++j) {
+          exactly_one_constraint.push_back(transpose ? graph[j][i]
+                                                     : graph[i][j]);
        }
+        model->Add(ExactlyOneConstraint(exactly_one_constraint));
      }
    }
+  };
+}

-    // Register, pass ownership.
+std::function<void(Model*)> SubcircuitConstraint(
+    const std::vector<std::vector<Literal>>& graph) {
+  return [=](Model* model) {
+    if (graph.empty()) return;
+    model->Add(ExactlyOnePerRowAndPerColumn(graph));
+    CircuitPropagator::Options options;
+    CircuitPropagator* constraint =
+        new CircuitPropagator(graph, options, model);
+    constraint->RegisterWith(model->GetOrCreate<GenericLiteralWatcher>());
+    model->TakeOwnership(constraint);
+  };
+}
+
+std::function<void(Model*)> MultipleSubcircuitThroughZeroConstraint(
+    const std::vector<std::vector<Literal>>& graph) {
+  return [=](Model* model) {
+    if (graph.empty()) return;
+    model->Add(ExactlyOnePerRowAndPerColumn(
+        graph, /*ignore_row_and_column_zero=*/true));
+    CircuitPropagator::Options options;
+    options.multiple_subcircuit_through_zero = true;
+    CircuitPropagator* constraint =
+        new CircuitPropagator(graph, options, model);
+    constraint->RegisterWith(model->GetOrCreate<GenericLiteralWatcher>());
+    model->TakeOwnership(constraint);
+  };
+}
+
+std::function<void(Model*)> CircuitCovering(
+    const std::vector<std::vector<Literal>>& graph,
+    const std::vector<int>& distinguished_nodes) {
+  return [=](Model* model) {
    CircuitCoveringPropagator* constraint =
        new CircuitCoveringPropagator(graph, distinguished_nodes, model);
    constraint->RegisterWith(model->GetOrCreate<GenericLiteralWatcher>());
--- a/ortools/sat/circuit.h
+++ b/ortools/sat/circuit.h
@@ -51,8 +51,8 @@ class CircuitPropagator : PropagatorInterface, ReversibleInterface {
  // being present when the given literal is true. The special values
  // kTrueLiteralIndex and kFalseLiteralIndex can be used for arcs that are
  // either always there or never there.
-  CircuitPropagator(std::vector<std::vector<LiteralIndex>> graph,
-                    Options options, Trail* trail);
+  CircuitPropagator(std::vector<std::vector<Literal>> graph, Options options,
+                    Model* model);

  void SetLevel(int level) final;
  bool Propagate() final;
@@ -60,18 +60,6 @@ class CircuitPropagator : PropagatorInterface, ReversibleInterface {
  void RegisterWith(GenericLiteralWatcher* watcher);

 private:
-  // Helper to deal with kTrueLiteralIndex and kFalseLiteralIndex.
-  bool LiteralIndexIsTrue(LiteralIndex index) {
-    if (index == kTrueLiteralIndex) return true;
-    if (index == kFalseLiteralIndex) return false;
-    return assignment_.LiteralIsTrue(Literal(index));
-  }
-  bool LiteralIndexIsFalse(LiteralIndex index) {
-    if (index == kTrueLiteralIndex) return false;
-    if (index == kFalseLiteralIndex) return true;
-    return assignment_.LiteralIsFalse(Literal(index));
-  }
-
  // Updates the structures when the given arc is added to the paths.
  void AddArc(int tail, int head, LiteralIndex literal_index);

@@ -81,7 +69,7 @@ class CircuitPropagator : PropagatorInterface, ReversibleInterface {
  void FillReasonForPath(int start_node, std::vector<Literal>* reason) const;

  const int num_nodes_;
-  const std::vector<std::vector<LiteralIndex>> graph_;
+  const std::vector<std::vector<Literal>> graph_;
  const Options options_;
  Trail* trail_;
  const VariablesAssignment& assignment_;
@@ -161,7 +149,7 @@ class CircuitCoveringPropagator : PropagatorInterface, ReversibleInterface {
  // Used in Propagate() to represent paths and circuits.
  std::vector<int> next_;
  std::vector<int> prev_;
-  std::vector<int> visited_;
+  std::vector<bool> visited_;
 };

 // ============================================================================
@@ -176,39 +164,17 @@ class CircuitCoveringPropagator : PropagatorInterface, ReversibleInterface {
 // the other constraints are not changed, i.e. matrix[0][5] is still counted
 // in column 5.
 std::function<void(Model*)> ExactlyOnePerRowAndPerColumn(
-    const std::vector<std::vector<LiteralIndex>>& square_matrix,
+    const std::vector<std::vector<Literal>>& graph,
    bool ignore_row_and_column_zero = false);

-inline std::function<void(Model*)> SubcircuitConstraint(
-    const std::vector<std::vector<LiteralIndex>>& graph) {
-  return [=](Model* model) {
-    if (graph.empty()) return;
-    model->Add(ExactlyOnePerRowAndPerColumn(graph));
-    CircuitPropagator::Options options;
-    CircuitPropagator* constraint =
-        new CircuitPropagator(graph, options, model->GetOrCreate<Trail>());
-    constraint->RegisterWith(model->GetOrCreate<GenericLiteralWatcher>());
-    model->TakeOwnership(constraint);
-  };
-}
+std::function<void(Model*)> SubcircuitConstraint(
+    const std::vector<std::vector<Literal>>& graph);

-inline std::function<void(Model*)> MultipleSubcircuitThroughZeroConstraint(
-    const std::vector<std::vector<LiteralIndex>>& graph) {
-  return [=](Model* model) {
-    if (graph.empty()) return;
-    model->Add(ExactlyOnePerRowAndPerColumn(
-        graph, /*ignore_row_and_column_zero=*/true));
-    CircuitPropagator::Options options;
-    options.multiple_subcircuit_through_zero = true;
-    CircuitPropagator* constraint =
-        new CircuitPropagator(graph, options, model->GetOrCreate<Trail>());
-    constraint->RegisterWith(model->GetOrCreate<GenericLiteralWatcher>());
-    model->TakeOwnership(constraint);
-  };
-}
+std::function<void(Model*)> MultipleSubcircuitThroughZeroConstraint(
+    const std::vector<std::vector<Literal>>& graph);

 std::function<void(Model*)> CircuitCovering(
-    const std::vector<std::vector<LiteralIndex>>& next,
+    const std::vector<std::vector<Literal>>& graph,
    const std::vector<int>& distinguished_nodes);

 }  // namespace sat
--- a/ortools/sat/cp_model_presolve.cc
+++ b/ortools/sat/cp_model_presolve.cc
@@ -1572,6 +1572,18 @@ void PresolveCpModel(const CpModelProto& initial_model,
    context.UpdateConstraintVariableUsage(c);
  }

+  // Hack for the optional variable so their literal is never considered to
+  // appear in only one constraint. TODO(user): if it appears in none, then we
+  // can remove the variable...
+  for (int i = 0; i < initial_model.variables_size(); ++i) {
+    if (!initial_model.variables(i).enforcement_literal().empty()) {
+      context
+          .var_to_constraints[PositiveRef(
+              initial_model.variables(i).enforcement_literal(0))]
+          .insert(-1);
+    }
+  }
+
  // Hack for the objective so that it is never considered to appear in only one
  // constraint.
  if (initial_model.has_objective()) {
--- a/ortools/sat/cp_model_solver.cc
+++ b/ortools/sat/cp_model_solver.cc
@@ -117,8 +117,14 @@ VariableUsage ComputeVariableUsage(const CpModelProto& model_proto,
    }
  }

-  // Make sure that an unused variable is instantiated as an IntegerVariable
  for (int i = 0; i < model_proto.variables_size(); ++i) {
+    // Take into account the presence literal of optional variables.
+    if (!model_proto.variables(i).enforcement_literal().empty()) {
+      references.literals.insert(
+          model_proto.variables(i).enforcement_literal(0));
+    }
+
+    // Make sure that an unused variable is instantiated as an IntegerVariable.
    if (ContainsKey(references.literals, i)) continue;
    if (ContainsKey(references.literals, NegatedRef(i))) continue;
    if (ContainsKey(references.variables, i)) continue;
@@ -186,9 +192,8 @@ class ModelWithMapping {
  }

  IntegerVariable Integer(int i) const {
-    CHECK_LT(PositiveRef(i), integers_.size());
+    DCHECK(IsInteger(i));
    const IntegerVariable var = integers_[PositiveRef(i)];
-    CHECK_NE(var, kNoIntegerVariable);
    return RefIsPositive(i) ? var : NegationOf(var);
  }

@@ -207,7 +212,7 @@ class ModelWithMapping {
  }

  sat::Literal Literal(int i) const {
-    CHECK_LT(PositiveRef(i), booleans_.size());
+    DCHECK(IsBoolean(i));
    return sat::Literal(booleans_[PositiveRef(i)], RefIsPositive(i));
  }

@@ -1237,39 +1242,41 @@ void LoadAutomataConstraint(const ConstraintProto& ct, ModelWithMapping* m) {
  m->Add(TransitionConstraint(vars, transitions, starting_state, final_states));
 }

-// From vector of n IntegerVariables, fill an n x n matrix of LiteralIndex
-// such that matrix[i][j] is the LiteralIndex of vars[i] == j.
-void FillLiteralIndexSquareMatrixFromIntegerVariableVector(
-    ModelWithMapping* m, const std::vector<IntegerVariable>& vars,
-    std::vector<std::vector<LiteralIndex>>* matrix) {
+// 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(
+    const std::vector<IntegerVariable>& vars, ModelWithMapping* m) {
  const int n = vars.size();
-  matrix->resize(n);
+  const Literal kTrueLiteral =
+      m->GetOrCreate<IntegerEncoder>()->GetTrueLiteral();
+  const Literal kFalseLiteral =
+      m->GetOrCreate<IntegerEncoder>()->GetFalseLiteral();
+  std::vector<std::vector<Literal>> matrix(
+      n, std::vector<Literal>(n, kFalseLiteral));
  for (int i = 0; i < n; i++) {
-    (*matrix)[i].resize(n, kFalseLiteralIndex);
    for (int j = 0; j < n; j++) {
      if (m->Get(IsFixed(vars[i]))) {
        const int value = m->Get(Value(vars[i]));
        DCHECK_LE(0, value);
        DCHECK_LT(value, n);
-        (*matrix)[i][value] = kTrueLiteralIndex;
+        matrix[i][value] = kTrueLiteral;
      } else {
        const auto encoding = m->Add(FullyEncodeVariable(vars[i]));
        for (const auto& entry : encoding) {
          const int value = entry.value.value();
          DCHECK_LE(0, value);
          DCHECK_LT(value, n);
-          (*matrix)[i][value] = entry.literal.Index();
+          matrix[i][value] = entry.literal;
        }
      }
    }
  }
+  return matrix;
 }

 void LoadCircuitConstraint(const ConstraintProto& ct, ModelWithMapping* m) {
  const std::vector<IntegerVariable> nexts = m->Integers(ct.circuit().nexts());
-  std::vector<std::vector<LiteralIndex>> graph;
-  FillLiteralIndexSquareMatrixFromIntegerVariableVector(m, nexts, &graph);
-  m->Add(SubcircuitConstraint(graph));
+  m->Add(SubcircuitConstraint(GetSquareMatrixFromIntegerVariables(nexts, m)));
 }

 // TODO(user): provide a sparse API.
@@ -1282,12 +1289,14 @@ void LoadRoutesConstraint(const ConstraintProto& ct, ModelWithMapping* m) {
  for (const int32 head : arg.heads()) {
    num_nodes = std::max(num_nodes, head + 1);
  }
-  std::vector<std::vector<LiteralIndex>> graph(
-      num_nodes, std::vector<LiteralIndex>(num_nodes, kFalseLiteralIndex));

+  const Literal kFalseLiteral =
+      m->GetOrCreate<IntegerEncoder>()->GetFalseLiteral();
+  std::vector<std::vector<Literal>> graph(
+      num_nodes, std::vector<Literal>(num_nodes, kFalseLiteral));
  const int num_arcs = arg.tails_size();
  for (int i = 0; i < num_arcs; ++i) {
-    graph[arg.tails(i)][arg.heads(i)] = m->Literal(arg.literals(i)).Index();
+    graph[arg.tails(i)][arg.heads(i)] = m->Literal(arg.literals(i));
  }
  m->Add(MultipleSubcircuitThroughZeroConstraint(graph));
 }
@@ -1296,8 +1305,8 @@ void LoadCircuitCoveringConstraint(const ConstraintProto& ct,
                                   ModelWithMapping* m) {
  const std::vector<IntegerVariable> nexts =
      m->Integers(ct.circuit_covering().nexts());
-  std::vector<std::vector<LiteralIndex>> graph;
-  FillLiteralIndexSquareMatrixFromIntegerVariableVector(m, nexts, &graph);
+  const std::vector<std::vector<Literal>> graph =
+      GetSquareMatrixFromIntegerVariables(nexts, m);
  const std::vector<int> distinguished(
      ct.circuit_covering().distinguished_nodes().begin(),
      ct.circuit_covering().distinguished_nodes().end());
--- a/ortools/sat/integer.cc
+++ b/ortools/sat/integer.cc
@@ -49,7 +49,7 @@ void IntegerEncoder::FullyEncodeVariable(IntegerVariable var) {

  std::vector<Literal> literals;
  if (values.size() == 1) {
-    literals.push_back(GetLiteralTrue());
+    literals.push_back(GetTrueLiteral());
  } else if (values.size() == 2) {
    literals.push_back(GetOrCreateAssociatedLiteral(
        IntegerLiteral::LowerOrEqual(var, values[0])));
--- a/ortools/sat/integer.h
+++ b/ortools/sat/integer.h
@@ -299,7 +299,7 @@ class IntegerEncoder {
  LiteralIndex SearchForLiteralAtOrBefore(IntegerLiteral i) const;

  // Get the literal always set to true, make it if it does not exist.
-  Literal GetLiteralTrue() {
+  Literal GetTrueLiteral() {
    DCHECK_EQ(0, sat_solver_->CurrentDecisionLevel());
    if (literal_index_true_ == kNoLiteralIndex) {
      const Literal literal_true =
@@ -309,6 +309,7 @@ class IntegerEncoder {
    }
    return Literal(literal_index_true_);
  }
+  Literal GetFalseLiteral() { return GetTrueLiteral().Negated(); }

 private:
  // Only add the equivalence between i_lit and literal, if there is already an