first successful integration of minisat inside or-tools

dependencies/sources/Minisat/core/Solver.cc

@@ -46,9 +46,7 @@ DEFINE_double(restart_inc, 2, "Restart interval increase factor");
 DEFINE_double(garbage_frac, 0.20, "The fraction of wasted memory allowed "
               "before a garbage collection is triggered");
 
-using namespace Minisat;
-
-
+namespace Minisat {
 //=============================================================================
 // Constructor/Destructor:
 
@@ -864,3 +862,4 @@ void Solver::garbageCollect() {
            ClauseAllocator::Unit_Size);
   to.moveTo(ca);
 }
+}  // namespace Minisat

examples/tests/boolean_test.cc

@@ -0,0 +1,79 @@
+// Copyright 2011-2012 Google
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+//     http://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+
+
+#include "base/hash.h"
+#include "base/map-util.h"
+#include "base/stl_util.h"
+#include "base/random.h"
+#include "constraint_solver/constraint_solveri.h"
+#include "constraint_solver/constraint_solver.h"
+#include "constraint_solver/model.pb.h"
+#include "util/string_array.h"
+
+namespace operations_research {
+class SatPropagator;
+bool AddBoolEq(SatPropagator* const sat,
+               IntExpr* const left,
+               IntExpr* const right);
+
+bool AddBoolLe(SatPropagator* const sat,
+               IntExpr* const left,
+               IntExpr* const right);
+
+bool AddBoolNot(SatPropagator* const sat,
+                IntExpr* const left,
+                IntExpr* const right);
+
+bool AddBoolAndArrayEqVar(SatPropagator* const sat,
+                          const std::vector<IntVar*>& vars,
+                          IntVar* const target);
+
+bool AddBoolAndEqVar(SatPropagator* const sat,
+                     IntVar* const left,
+                     IntVar* const right,
+                     IntVar* const target);
+
+bool AddBoolOrArrayEqualTrue(SatPropagator* const sat,
+                             const std::vector<IntVar*>& vars);
+
+bool AddBoolAndArrayEqualFalse(SatPropagator* const sat,
+                               const std::vector<IntVar*>& vars);
+
+SatPropagator* MakeSatPropagator(Solver* const solver);
+
+void TestApi() {
+  Solver solver("TestApi");
+  SatPropagator* const sat = MakeSatPropagator(&solver);
+  solver.AddConstraint(reinterpret_cast<Constraint*>(sat));
+  IntVar* const x = solver.MakeBoolVar("x");
+  IntVar* const y = solver.MakeBoolVar("y");
+  CHECK(AddBoolEq(sat, x, solver.MakeDifference(1, y)));
+  DecisionBuilder* const db =
+      solver.MakePhase(x, y,
+                       Solver::CHOOSE_FIRST_UNBOUND,
+                       Solver::ASSIGN_MIN_VALUE);
+  solver.NewSearch(db);
+  while (solver.NextSolution()) {
+    LOG(INFO) << " x = " << x->Value() << ", y = " << y->Value();
+  }
+  solver.EndSearch();
+}
+}  // namespace operations_research
+
+
+int main(int argc, char** argv) {
+  google::ParseCommandLineFlags(&argc, &argv, true);
+  operations_research::TestApi();
+  return 0;
+}

makefiles/Makefile.cpp.mk

@@ -758,6 +758,12 @@ $(OBJ_DIR)/visitor_test.$O:$(EX_DIR)/tests/visitor_test.cc $(SRC_DIR)/constraint
 $(BIN_DIR)/visitor_test$E: $(CP_DEPS) $(OBJ_DIR)/visitor_test.$O
 	$(CCC) $(CFLAGS) $(OBJ_DIR)/visitor_test.$O $(CP_LNK) $(LDFLAGS) $(EXEOUT)visitor_test$E
 
+$(OBJ_DIR)/boolean_test.$O:$(EX_DIR)/tests/boolean_test.cc $(SRC_DIR)/constraint_solver/constraint_solver.h
+	$(CCC) $(CFLAGS) -c $(EX_DIR)$Stests/boolean_test.cc $(OBJ_OUT)boolean_test.$O
+
+$(BIN_DIR)/boolean_test$E: $(CP_DEPS) $(OBJ_DIR)/boolean_test.$O
+	$(CCC) $(CFLAGS) $(OBJ_DIR)/boolean_test.$O $(CP_LNK) $(LDFLAGS) $(EXEOUT)boolean_test$E
+
 # Linear Programming Examples
 
 $(OBJ_DIR)/strawberry_fields_with_column_generation.$O: $(EX_DIR)/cpp/strawberry_fields_with_column_generation.cc $(SRC_DIR)/linear_solver/linear_solver.h

src/constraint_solver/booleans.cc

@@ -37,11 +37,11 @@
 #include "core/Solver.cc"
 
 namespace operations_research {
-namespace {
-
 class SatPropagator : public Constraint {
  public:
-  SatPropagator(Solver* const solver) : Constraint(solver) {}
+  SatPropagator(Solver* const solver)
+  : Constraint(solver),
+    num_bound_literals_(0) {}
 
   ~SatPropagator() {}
 
@@ -66,21 +66,36 @@ class SatPropagator : public Constraint {
     if (!solver()->IsBooleanVar(expr, &expr_var, &expr_negated)) {
       return Minisat::lit_Error;
     }
+    VLOG(1) << "SAT: Parse " << expr->DebugString() << " to "
+            << expr_var->DebugString() << "/" << expr_negated;
     if (ContainsKey(indices_, expr_var)) {
       return Minisat::mkLit(indices_[expr_var], expr_negated);
     } else {
       const Minisat::Var var = minisat_.newVar(true, true);
       vars_.push_back(expr_var);
-      return Minisat::mkLit(var, expr_negated);
+      indices_[expr_var] = var;
+      Minisat::Lit lit = Minisat::mkLit(var, expr_negated);
+      VLOG(1) << "Created var = " << Minisat::toInt(var)
+              << ", lit = " << Minisat::toInt(lit);
+      return lit;
     }
   }
 
   void VariableBound(int index) {
-    // if (indices_[index]->Min() == 0) {
-    //   Flip(Minisat::Var(-1 - index));
-    // } else {
-    //   Flip(Minisat::Var(1 + index));
-    // }
+    Minisat::Var var(index);
+    Minisat::Lit lit = Minisat::mkLit(var, vars_[index]->Value());
+    VLOG(1) << "Assign " << vars_[index]->DebugString()
+            << ", enqueue lit = " << Minisat::toInt(lit);
+    if (num_bound_literals_.Value() < bound_literals_.size()) {
+      bound_literals_.shrink(
+          bound_literals_.size() - num_bound_literals_.Value());
+    }
+    num_bound_literals_.Incr(solver());
+    bound_literals_.push(lit);
+    if (!minisat_.solve(bound_literals_)) {
+      VLOG(1) << "  - failure detected";
+      solver()->Fail();
+    }
   }
 
   virtual void Post() {
@@ -136,8 +151,9 @@ class SatPropagator : public Constraint {
   Minisat::Solver minisat_;
   std::vector<IntVar*> vars_;
   hash_map<IntVar*, Minisat::Var> indices_;
+  Minisat::vec<Minisat::Lit> bound_literals_;
+  NumericalRev<int> num_bound_literals_;
 };
-}  // namespace
 
 bool AddBoolEq(SatPropagator* const sat,
                IntExpr* const left,
@@ -236,4 +252,8 @@ bool AddBoolAndArrayEqualFalse(SatPropagator* const sat,
   sat->AddClause(lits);
   return false;
 }
+
+SatPropagator* MakeSatPropagator(Solver* const solver) {
+  return solver->RevAlloc(new SatPropagator(solver));
+}
 }  // namespace operations_research