[CP-SAT] work on lrat, clause congruence, inprocess ; bug fixes

Author: lperron

ortools/sat/BUILD.bazel

@@ -1638,6 +1638,7 @@ cc_library(
         "//ortools/util:sorted_interval_list",
         "//ortools/util:strong_integers",
         "//ortools/util:time_limit",
+        "@abseil-cpp//absl/algorithm:container",
         "@abseil-cpp//absl/cleanup",
         "@abseil-cpp//absl/container:btree",
         "@abseil-cpp//absl/container:flat_hash_map",

ortools/sat/clause.cc

@@ -125,7 +125,6 @@ ClauseManager::~ClauseManager() {
 }
 
 void ClauseManager::Resize(int num_variables) {
-  DCHECK(is_clean_);
   watchers_on_false_.resize(num_variables << 1);
   reasons_.resize(num_variables);
   needs_cleaning_.Resize(LiteralIndex(num_variables << 1));
@@ -980,8 +979,29 @@ bool BinaryImplicationGraph::AddBinaryClauseInternal(
     trail_->ChangeReason(trail_index, propagator_id_);
   }
 
+  // Deal with literal fixing and do not even add a binary clause in that case.
   if (rep_a == rep_b) {
     return FixLiteral(rep_a, {rep_id});
+  } else if (trail_->CurrentDecisionLevel() == 0) {
+    const auto& assignment = trail_->Assignment();
+
+    // TODO(user): just make GetUnitClauseId() work all the time? for that
+    // we need to make sure all level zero are pushed with kUnitReason.
+    if (lrat_proof_handler_ != nullptr) {
+      if (assignment.LiteralIsFalse(rep_a)) {
+        return FixLiteral(rep_b,
+                          {rep_id, trail_->GetUnitClauseId(rep_a.Variable())});
+      } else if (assignment.LiteralIsFalse(rep_b)) {
+        return FixLiteral(rep_a,
+                          {rep_id, trail_->GetUnitClauseId(rep_b.Variable())});
+      }
+    } else {
+      if (assignment.LiteralIsFalse(rep_a)) {
+        return FixLiteral(rep_b, {});
+      } else if (assignment.LiteralIsFalse(rep_b)) {
+        return FixLiteral(rep_a, {});
+      }
+    }
   }
 
   a = rep_a;

ortools/sat/cp_model_checker.cc

@@ -284,15 +284,6 @@ std::string ValidateLinearExpression(const CpModelProto& model,
   return "";
 }
 
-std::string ValidateConstantExpression(const CpModelProto& model,
-                                       const LinearExpressionProto& expr) {
-  if (!expr.vars().empty()) {
-    return absl::StrCat("expression must be constant: ",
-                        ProtobufShortDebugString(expr));
-  }
-  return ValidateLinearExpression(model, expr);
-}
-
 std::string ValidateLinearConstraint(const CpModelProto& model,
                                      const ConstraintProto& ct) {
   if (!DomainInProtoIsValid(ct.linear())) {
@@ -1376,8 +1367,8 @@ class ConstraintChecker {
   bool LinearConstraintIsFeasible(const ConstraintProto& ct) {
     int64_t sum = 0;
     const int num_variables = ct.linear().coeffs_size();
-    const int* const vars = ct.linear().vars().data();
-    const int64_t* const coeffs = ct.linear().coeffs().data();
+    absl::Span<const int> vars = absl::MakeSpan(ct.linear().vars());
+    absl::Span<const int64_t> coeffs = absl::MakeSpan(ct.linear().coeffs());
     for (int i = 0; i < num_variables; ++i) {
       // We know we only have positive reference now.
       DCHECK(RefIsPositive(vars[i]));

ortools/sat/cp_model_solver.cc

@@ -2529,6 +2529,12 @@ CpSolverResponse SolveCpModel(const CpModelProto& model_proto, Model* model) {
   }
 #endif  // ORTOOLS_TARGET_OS_SUPPORTS_THREADS
 
+  if (DEBUG_MODE) {
+    LOG(WARNING)
+        << "WARNING: CP-SAT is running in debug mode. The solver will "
+           "be slow because we will do a lot of extra checks. Compile in "
+           "optimization mode to gain an order of magnitude speedup.";
+  }
   SOLVER_LOG(logger, "");
   SOLVER_LOG(logger, "Starting ", CpSatSolverVersion());
   SOLVER_LOG(logger, "Parameters: ", ProtobufShortDebugString(params));

ortools/sat/csharp/CpSolver.cs

@@ -210,7 +210,8 @@ public bool BooleanValue(ILiteral literal)
     /// <summary>
     /// Releases unmanaged resources and optionally releases managed resources.
     /// </summary>
-    /// <param name="disposing">true to release both managed and unmanaged resources; false to release only unmanaged resources.</param>
+    /// <param name="disposing">true to release both managed and unmanaged resources; false to release only unmanaged
+    /// resources.</param>
     protected virtual void Dispose(bool disposing)
     {
         if (_disposed)
@@ -270,4 +271,4 @@ class BestBoundCallbackDelegate : BestBoundCallback
     public override void NewBestBound(double bound) => _delegate(bound);
 }
 
-} // namespace Google.OrTools.Sat
+} // namespace Google.OrTools.Sat

ortools/sat/gate_utils.h

@@ -98,6 +98,28 @@ inline int AddHoleAtPosition(int i, int bitset) {
   return (bitset & ((1 << i) - 1)) + ((bitset >> i) << (i + 1));
 }
 
+inline int RemoveFixedInput(int i, bool at_true,
+                            absl::Span<LiteralIndex> inputs,
+                            int& int_function_values) {
+  DCHECK_LT(i, inputs.size());
+  const int value = at_true ? 1 : 0;
+
+  // Re-compute the bitset.
+  SmallBitset values = int_function_values;
+  SmallBitset new_truth_table = 0;
+  const int new_size = inputs.size() - 1;
+  for (int p = 0; p < (1 << new_size); ++p) {
+    const int extended_p = AddHoleAtPosition(i, p) | (value << i);
+    new_truth_table |= ((values >> extended_p) & 1) << p;
+  }
+  int_function_values = new_truth_table;
+
+  for (int j = i + 1; j < inputs.size(); ++j) {
+    inputs[j - 1] = inputs[j];
+  }
+  return new_size;
+}
+
 // The function is target = function_values[inputs as bit position].
 //
 // TODO(user): This can be optimized with more bit twiddling if needed.

ortools/sat/gate_utils_test.cc

@@ -75,6 +75,47 @@ TEST(AddHoleAtPositionTest, BasicTest) {
   EXPECT_EQ(AddHoleAtPosition(8, 0xFF), 0b011111111);
 }
 
+TEST(CanonicalizeFunctionTruthTableTest, AndGateWithXAndNotX) {
+  LiteralIndex output = Literal(+1).Index();
+  std::vector<LiteralIndex> inputs{Literal(+2).Index(), Literal(-2).Index()};
+  int table = 0b1000;
+  const int new_size =
+      CanonicalizeFunctionTruthTable(output, absl::MakeSpan(inputs), table);
+  CHECK_EQ(new_size, 0);  // Fixed to zero.
+}
+
+TEST(RemoveFixedInputTest, BasicTest1) {
+  std::vector<LiteralIndex> inputs{Literal(+1).Index(), Literal(+2).Index(),
+                                   Literal(+3).Index()};
+  int table = 0b01011010;
+  const int new_size = RemoveFixedInput(1, true, absl::MakeSpan(inputs), table);
+  EXPECT_EQ(new_size, 2);
+  EXPECT_EQ(inputs[0], Literal(+1).Index());
+  EXPECT_EQ(inputs[1], Literal(+3).Index());
+  EXPECT_EQ(table, 0b0110) << std::bitset<4>(table);
+}
+
+TEST(RemoveFixedInputTest, BasicTest2) {
+  std::vector<LiteralIndex> inputs{Literal(+1).Index(), Literal(+2).Index(),
+                                   Literal(+3).Index()};
+  int table = 0b01011010;
+  const int new_size =
+      RemoveFixedInput(1, false, absl::MakeSpan(inputs), table);
+  EXPECT_EQ(new_size, 2);
+  EXPECT_EQ(inputs[0], Literal(+1).Index());
+  EXPECT_EQ(inputs[1], Literal(+3).Index());
+  EXPECT_EQ(table, 0b0110) << std::bitset<4>(table);
+}
+
+TEST(CanonicalizeFunctionTruthTableTest, AndGateWithXAndNotX2) {
+  LiteralIndex output = Literal(+1).Index();
+  std::vector<LiteralIndex> inputs{Literal(-2).Index(), Literal(+2).Index()};
+  int table = 0b1000;
+  const int new_size =
+      CanonicalizeFunctionTruthTable(output, absl::MakeSpan(inputs), table);
+  CHECK_EQ(new_size, 0);  // Fixed to zero.
+}
+
 TEST(CanonicalizeFunctionTruthTableTest, RandomTest) {
   absl::BitGen random;
   const int num_vars = 8;

ortools/sat/lrat_proof_handler.cc

@@ -802,7 +802,6 @@ ClauseId LratProofHandler::AddAndProveInferredClauseByEnumeration(
   // That give us 2^(n + 1) intermediate clauses.
   // Their ids will be stored in (1 << k) + binary_encoding_of_the_li.
   const int n = to_dense_index.size() - new_clause.size();
-  CHECK_GT(n, 0);  // We dealt with this above.
   CHECK_EQ(n, relevant_literals.size());
   const int num_intermediates = 1 << (n + 1);
   std::vector<ClauseId> ids(num_intermediates, kNoClauseId);
@@ -838,11 +837,16 @@ ClauseId LratProofHandler::AddAndProveInferredClauseByEnumeration(
       // The clause is the same as the one we try to prove! or smaller.
       if (clauses_for_proof[i].size() == new_clause.size()) {
         return ids_for_proof[i];
+      } else {
+        // TODO(user): Likely we could have simplified what we are trying to
+        // prove. Like I saw this happen when we prove an equivalence but we
+        // can actually prove that the variables are fixed.
+        const ClauseId new_id = id_generator_->GetNextId();
+        if (!AddInferredClause(new_id, new_clause, {ids_for_proof[i]})) {
+          return error("failed trivial inclusion proof");
+        }
+        return new_id;
       }
-
-      // TODO(user): if this ever happen we can create a new id and prove it
-      // with clauses_for_proof[i], but for now I never saw that.
-      return error("Case not yet supported");
     }
 
     mask >>= new_clause.size();