add NoGood API and naive implementation

Makefile.build.cpp

@@ -96,6 +96,7 @@ CONSTRAINT_SOLVER_LIB_OS = \
 	objs/expressions.$O\
 	objs/interval.$O\
 	objs/local_search.$O\
+	objs/nogoods.$O\
 	objs/pack.$O\
 	objs/range_cst.$O\
 	objs/resource.$O\
@@ -162,6 +163,9 @@ objs/interval.$O:constraint_solver/interval.cc
 objs/local_search.$O:constraint_solver/local_search.cc
 	$(CCC) $(CFLAGS) -c constraint_solver/local_search.cc $(OBJOUT)objs/local_search.$O
 
+objs/nogoods.$O:constraint_solver/nogoods.cc
+	$(CCC) $(CFLAGS) -c constraint_solver/nogoods.cc $(OBJOUT)objs/nogoods.$O
+
 objs/pack.$O:constraint_solver/pack.cc
 	$(CCC) $(CFLAGS) -c constraint_solver/pack.cc $(OBJOUT)objs/pack.$O
 

constraint_solver/constraint_solver.h

@@ -120,6 +120,8 @@ class LocalSearchFilter;
 class LocalSearchOperator;
 class LocalSearchPhaseParameters;
 class MPSolver;
+class NoGoodManager;
+class NoGoodTerm;
 class OptimizeVar;
 class Pack;
 class PropagationBaseObject;
@@ -151,8 +153,7 @@ enum MarkerType {
 struct SolverParameters {
  public:
   enum TrailCompression {
-    NO_COMPRESSION,
-    COMPRESS_WITH_ZLIB
+    NO_COMPRESSION, COMPRESS_WITH_ZLIB
   };
 
   enum ProfileLevel {
@@ -1494,6 +1495,13 @@ class Solver {
   // this happens at a leaf the corresponding solution will be rejected.
   SearchLimit* MakeCustomLimit(ResultCallback<bool>* limiter);
 
+  // ----- No Goods -----
+
+  // Creates a non-reversible nogood recorder to store and use nogoods
+  // during search. It can be used during search with restart to avoid
+  // revisiting the same portion of the search tree.
+  NoGoodManager* MakeNoGoodManager();
+
   // ----- Tree Monitor -----
   // Creates a tree monitor that outputs a detailed overview of the
   // decision phase in cpviz format. The XML data is written to files
@@ -2458,6 +2466,7 @@ class Demon : public BaseObject {
 
   // This method un-inhibit the demon that was inhibited.
   void desinhibit(Solver* const s);
+
  private:
   friend class Queue;
   void set_stamp(int64 stamp) { stamp_ = stamp; }
@@ -2893,7 +2902,7 @@ class OptimizeVar : public SearchMonitor {
 
 // ---------- Search Limits ----------
 
-// base class of all search limits
+// Base class of all search limits.
 class SearchLimit : public SearchMonitor {
  public:
   explicit SearchLimit(Solver* const s) : SearchMonitor(s), crossed_(false) { }
@@ -2931,6 +2940,75 @@ class SearchLimit : public SearchMonitor {
   DISALLOW_COPY_AND_ASSIGN(SearchLimit);
 };
 
+// ---------- NoGood Recorder ------
+
+// Nogoods are used to store negative information collected during
+// search. They are by definition non reversible.
+
+// ----- No Good ----
+
+// A nogood is a conjunction if unary constraints that represents a
+// state that must not be visited during search.  For instance if X
+// and Y are variables, (X == 5) && (Y != 3) is a nogood that forbid
+// all part of the search tree where X is 5 and Y is not 3.
+class NoGood {
+ public:
+  ~NoGood();
+  // Creates a term var == value.
+  void AddIntegerVariableEqualValueTerm(IntVar* const var, int64 value);
+  // Creates a term var != value.
+  void AddIntegerVariableNotEqualValueTerm(IntVar* const var, int64 value);
+  // Apply the nogood. That is if there is only one undecided term
+  // and all remaining terms are always true, then the opposite of
+  // this term is added to the solver.
+  void Apply(Solver* const solver);
+  // Pretty print.
+  string DebugString() const;
+  // TODO(user) : support interval variables and more types of constraints.
+ private:
+  std::vector<NoGoodTerm*> terms_;
+};
+
+// ----- Base class of no good manager -----
+
+// A no good recorder is used to store a set of no goods in a non
+// reversible way during search. It will actively propagate nogoods,
+// that is if all its terms minus one are always true, then it will
+// apply the reverse of this term during the search.
+class NoGoodManager : public SearchMonitor {
+ public:
+  explicit NoGoodManager(Solver* const s) : SearchMonitor(s) {}
+  virtual ~NoGoodManager() {}
+
+  // ----- User API -----
+
+  // Clear all stored nogoods.
+  virtual void Clear() = 0;
+  // NoGood factory. Create an empty nogood.
+  NoGood* MakeNoGood();
+  // Add one nogood to the recorder. Ownership is transfered to the recorder.
+  virtual void AddNoGood(NoGood* const nogood) = 0;
+  // Returns the number of nogoods added to the recorder.
+  virtual int NoGoodCount() const = 0;
+  // Pretty Print.
+  virtual string DebugString() const = 0;
+
+
+  // ----- Internal methods that links search events to the recorder API -----
+  virtual void EnterSearch();
+  virtual void BeginNextDecision(DecisionBuilder* const db);
+  virtual bool AcceptSolution();
+ private:
+  // ----- Implementor API -----
+
+  // Initialize data structures.
+  virtual void Init() = 0;
+  // Apply the nogood.
+  virtual void Apply() = 0;
+
+  DISALLOW_COPY_AND_ASSIGN(NoGoodManager);
+};
+
 // ---------- Interval Var ----------
 
 // An interval var is often used in scheduling. Its main

constraint_solver/nogoods.cc

@@ -0,0 +1,212 @@
+// Copyright 2010-2011 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/callback.h"
+#include "base/integral_types.h"
+#include "base/logging.h"
+#include "base/scoped_ptr.h"
+#include "base/stringprintf.h"
+#include "base/concise_iterator.h"
+#include "base/stl_util-inl.h"
+#include "constraint_solver/constraint_solveri.h"
+
+namespace operations_research {
+
+// ----- Base Class -----
+
+void NoGoodManager::EnterSearch() {
+  Init();
+}
+
+void NoGoodManager::BeginNextDecision(DecisionBuilder* const db) {
+  Apply();
+}
+
+bool NoGoodManager::AcceptSolution() {
+  Apply();
+  return true;
+}
+
+NoGood* NoGoodManager::MakeNoGood() {
+  return new NoGood();
+}
+
+// ----- Base class for NoGood terms -----
+
+class NoGoodTerm {
+ public:
+  enum TermStatus {
+    ALWAYS_TRUE,
+    ALWAYS_FALSE,
+    UNDECIDED
+  };
+  NoGoodTerm() {}
+  virtual ~NoGoodTerm() {}
+
+  virtual TermStatus Evaluate() const = 0;
+  virtual void ApplyReverse() = 0;
+  virtual string DebugString() const = 0;
+ private:
+  DISALLOW_COPY_AND_ASSIGN(NoGoodTerm);
+};
+
+// ----- IntegerVariableNoGoodTerm -----
+
+// IntVar == int64 specialization.
+class IntegerVariableNoGoodTerm : public NoGoodTerm {
+ public:
+  IntegerVariableNoGoodTerm(IntVar* const var, int64 value, bool assign)
+      : integer_variable_(var), value_(value), assign_(assign) {
+    CHECK_NOTNULL(integer_variable_);
+  }
+
+  virtual TermStatus Evaluate() const {
+    if (!integer_variable_->Contains(value_)) {
+      return assign_ ? ALWAYS_FALSE : ALWAYS_TRUE;
+    } else if (integer_variable_->Bound()) {
+      return assign_ ? ALWAYS_TRUE : ALWAYS_FALSE;
+    } else {
+      return UNDECIDED;
+    }
+  }
+
+  virtual void ApplyReverse() {
+    if (assign_) {
+      integer_variable_->RemoveValue(value_);
+    } else {
+      integer_variable_->SetValue(value_);
+    }
+  }
+
+  virtual string DebugString() const {
+    return StringPrintf("(%s %s %lld)",
+                        integer_variable_->name().c_str(),
+                        assign_ ? "==" : "!=",
+                        value_);
+  }
+
+  IntVar* integer_variable() const { return integer_variable_; }
+  int64 value() const { return value_; }
+  bool assign() const { return assign_; }
+
+ private:
+  IntVar* const integer_variable_;
+  const int64 value_;
+  const bool assign_;
+  DISALLOW_COPY_AND_ASSIGN(IntegerVariableNoGoodTerm);
+};
+
+// ----- NoGood -----
+
+NoGood::~NoGood() {
+  STLDeleteElements(&terms_);
+}
+
+void NoGood::AddIntegerVariableEqualValueTerm(IntVar* const var, int64 value) {
+  terms_.push_back(new IntegerVariableNoGoodTerm(var, value, true));
+}
+
+void NoGood::AddIntegerVariableNotEqualValueTerm(IntVar* const var,
+                                                 int64 value) {
+  terms_.push_back(new IntegerVariableNoGoodTerm(var, value, false));
+}
+
+void NoGood::Apply(Solver* const solver) {
+  NoGoodTerm* first_undecided = NULL;
+  for (int i = 0; i < terms_.size(); ++i) {
+    switch (terms_[i]->Evaluate()) {
+      case NoGoodTerm::ALWAYS_TRUE: {
+        break;
+      }
+      case NoGoodTerm::ALWAYS_FALSE: {
+        return;
+      }
+      case NoGoodTerm::UNDECIDED: {
+        if (first_undecided == NULL) {
+          first_undecided = terms_[i];
+        } else {
+          // more than one undecided, we cannot deduce anything.
+          return;
+        }
+        break;
+      }
+    }
+  }
+  if (first_undecided == NULL && terms_.size() > 0) {
+    solver->Fail();
+  }
+  if (first_undecided != NULL) {
+    first_undecided->ApplyReverse();
+  }
+}
+
+string NoGood::DebugString() const {
+  string result = "(";
+  for (int i = 0; i < terms_.size(); ++i) {
+    if (i != 0) {
+      result.append(" && ");
+    }
+    result.append(terms_[i]->DebugString());
+  }
+  result.append(")");
+  return result;
+}
+
+// ----- NoGoodManager -----
+
+// This implementation is very naive. It will be kept in the future as
+// a reference point.
+
+class NaiveNoGoodManager : public NoGoodManager {
+ public:
+  explicit NaiveNoGoodManager(Solver* const solver) : NoGoodManager(solver) {}
+  virtual ~NaiveNoGoodManager() {
+    Clear();
+  }
+
+  virtual void Clear() {
+    STLDeleteElements(&nogoods_);
+  }
+
+  virtual void Init() {}
+
+  virtual void AddNoGood(NoGood* const nogood) {
+    nogoods_.push_back(nogood);
+  }
+
+  virtual int NoGoodCount() const {
+    return nogoods_.size();
+  }
+
+  virtual void Apply() {
+    Solver* const s = solver();
+    for (int i = 0; i < nogoods_.size(); ++i) {
+      nogoods_[i]->Apply(s);
+    }
+  }
+
+  string DebugString() const {
+    return StringPrintf("NaiveNoGoodManager(%d)", NoGoodCount());
+  }
+
+ private:
+  std::vector<NoGood*> nogoods_;
+};
+
+// ----- API -----
+
+NoGoodManager* Solver::MakeNoGoodManager() {
+  return RevAlloc(new NaiveNoGoodManager(this));
+}
+
+}  // namespace operations_research