From 15fb1447a4afcab736fedfa8ff08d73996e144cc Mon Sep 17 00:00:00 2001 From: "lperron@google.com" Date: Wed, 11 Jul 2012 22:20:07 +0000 Subject: [PATCH] first successful integration of minisat inside or-tools --- dependencies/sources/Minisat/core/Solver.cc | 5 +- examples/tests/boolean_test.cc | 79 +++++++++++++++++++++ makefiles/Makefile.cpp.mk | 6 ++ src/constraint_solver/booleans.cc | 40 ++++++++--- 4 files changed, 117 insertions(+), 13 deletions(-) create mode 100644 examples/tests/boolean_test.cc diff --git a/dependencies/sources/Minisat/core/Solver.cc b/dependencies/sources/Minisat/core/Solver.cc index d95d0c71d0..bb7432ecad 100644 --- a/dependencies/sources/Minisat/core/Solver.cc +++ b/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 diff --git a/examples/tests/boolean_test.cc b/examples/tests/boolean_test.cc new file mode 100644 index 0000000000..d1c447e40d --- /dev/null +++ b/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& 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& vars); + +bool AddBoolAndArrayEqualFalse(SatPropagator* const sat, + const std::vector& vars); + +SatPropagator* MakeSatPropagator(Solver* const solver); + +void TestApi() { + Solver solver("TestApi"); + SatPropagator* const sat = MakeSatPropagator(&solver); + solver.AddConstraint(reinterpret_cast(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; +} diff --git a/makefiles/Makefile.cpp.mk b/makefiles/Makefile.cpp.mk index 3ca07bbd24..7ef70938e2 100644 --- a/makefiles/Makefile.cpp.mk +++ b/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 diff --git a/src/constraint_solver/booleans.cc b/src/constraint_solver/booleans.cc index bd37e137f4..352577f529 100644 --- a/src/constraint_solver/booleans.cc +++ b/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 vars_; hash_map indices_; + Minisat::vec bound_literals_; + NumericalRev 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