From 5b66707375c08991654a6cab50fa0232c8dcb09a Mon Sep 17 00:00:00 2001 From: Laurent Perron Date: Mon, 3 Dec 2018 08:39:16 +0100 Subject: [PATCH] remove empty layer to use SAT inside the CP solver --- makefiles/Makefile.gen.mk | 28 +-- ortools/constraint_solver/sat_constraint.cc | 48 ---- ortools/constraint_solver/sat_constraint.h | 261 -------------------- ortools/constraint_solver/table.cc | 1 - 4 files changed, 1 insertion(+), 337 deletions(-) delete mode 100644 ortools/constraint_solver/sat_constraint.cc delete mode 100644 ortools/constraint_solver/sat_constraint.h diff --git a/makefiles/Makefile.gen.mk b/makefiles/Makefile.gen.mk index 02585ea4d2..32b0667dcd 100644 --- a/makefiles/Makefile.gen.mk +++ b/makefiles/Makefile.gen.mk @@ -2589,7 +2589,6 @@ CP_DEPS = \ $(SRC_DIR)/ortools/constraint_solver/routing_neighborhoods.h \ $(SRC_DIR)/ortools/constraint_solver/routing_parameters.h \ $(SRC_DIR)/ortools/constraint_solver/routing_types.h \ - $(SRC_DIR)/ortools/constraint_solver/sat_constraint.h \ $(GEN_DIR)/ortools/constraint_solver/assignment.pb.h \ $(GEN_DIR)/ortools/constraint_solver/demon_profiler.pb.h \ $(GEN_DIR)/ortools/constraint_solver/routing_enums.pb.h \ @@ -2626,7 +2625,6 @@ CP_LIB_OBJS = \ $(OBJ_DIR)/constraint_solver/routing_neighborhoods.$O \ $(OBJ_DIR)/constraint_solver/routing_parameters.$O \ $(OBJ_DIR)/constraint_solver/routing_search.$O \ - $(OBJ_DIR)/constraint_solver/sat_constraint.$O \ $(OBJ_DIR)/constraint_solver/sched_constraints.$O \ $(OBJ_DIR)/constraint_solver/sched_expr.$O \ $(OBJ_DIR)/constraint_solver/sched_search.$O \ @@ -3172,30 +3170,6 @@ objs/constraint_solver/routing_search.$O: \ ortools/port/proto_utils.h | $(OBJ_DIR)/constraint_solver $(CCC) $(CFLAGS) -c $(SRC_DIR)$Sortools$Sconstraint_solver$Srouting_search.cc $(OBJ_OUT)$(OBJ_DIR)$Sconstraint_solver$Srouting_search.$O -objs/constraint_solver/sat_constraint.$O: \ - ortools/constraint_solver/sat_constraint.cc \ - ortools/constraint_solver/sat_constraint.h ortools/base/hash.h \ - ortools/base/basictypes.h ortools/base/integral_types.h \ - ortools/base/logging.h ortools/base/macros.h ortools/base/map_util.h \ - ortools/constraint_solver/constraint_solver.h \ - ortools/base/commandlineflags.h ortools/base/random.h \ - ortools/base/sysinfo.h ortools/base/timer.h \ - ortools/gen/ortools/constraint_solver/solver_parameters.pb.h \ - ortools/util/piecewise_linear_function.h \ - ortools/util/saturated_arithmetic.h ortools/util/bitset.h \ - ortools/util/sorted_interval_list.h ortools/util/tuple_set.h \ - ortools/constraint_solver/constraint_solveri.h ortools/util/vector_map.h \ - ortools/sat/sat_solver.h ortools/base/int_type.h \ - ortools/base/int_type_indexed_vector.h ortools/sat/clause.h \ - ortools/sat/drat_proof_handler.h ortools/sat/drat_checker.h \ - ortools/sat/sat_base.h ortools/sat/model.h ortools/base/typeid.h \ - ortools/sat/drat_writer.h ortools/base/file.h ortools/base/status.h \ - ortools/gen/ortools/sat/sat_parameters.pb.h ortools/util/random_engine.h \ - ortools/util/stats.h ortools/sat/pb_constraint.h ortools/sat/restart.h \ - ortools/util/running_stat.h ortools/sat/sat_decision.h \ - ortools/util/integer_pq.h ortools/util/time_limit.h | $(OBJ_DIR)/constraint_solver - $(CCC) $(CFLAGS) -c $(SRC_DIR)$Sortools$Sconstraint_solver$Ssat_constraint.cc $(OBJ_OUT)$(OBJ_DIR)$Sconstraint_solver$Ssat_constraint.$O - objs/constraint_solver/sched_constraints.$O: \ ortools/constraint_solver/sched_constraints.cc \ ortools/base/integral_types.h ortools/base/logging.h \ @@ -3267,7 +3241,7 @@ objs/constraint_solver/table.$O: ortools/constraint_solver/table.cc \ ortools/util/saturated_arithmetic.h ortools/util/bitset.h \ ortools/util/sorted_interval_list.h ortools/util/tuple_set.h \ ortools/constraint_solver/constraint_solveri.h ortools/util/vector_map.h \ - ortools/constraint_solver/sat_constraint.h ortools/sat/sat_solver.h \ + ortools/sat/sat_solver.h \ ortools/base/int_type.h ortools/base/int_type_indexed_vector.h \ ortools/sat/clause.h ortools/sat/drat_proof_handler.h \ ortools/sat/drat_checker.h ortools/sat/sat_base.h ortools/sat/model.h \ diff --git a/ortools/constraint_solver/sat_constraint.cc b/ortools/constraint_solver/sat_constraint.cc deleted file mode 100644 index df8fe38176..0000000000 --- a/ortools/constraint_solver/sat_constraint.cc +++ /dev/null @@ -1,48 +0,0 @@ -// Copyright 2010-2018 Google LLC -// 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 "ortools/constraint_solver/sat_constraint.h" - -namespace operations_research { - -int BooleanVariableManager::RegisterIntVar(IntVar* int_var) { - const int reg_index = gtl::LookupOrInsert(®istration_index_map_, int_var, - registered_int_vars_.size()); - if (reg_index < registered_int_vars_.size()) return reg_index; - registered_int_vars_.push_back(int_var); - - const int num_variables(solver_->NumVariables()); - IntVarLiteralGetter literal_getter(sat::BooleanVariable(num_variables), - int_var->Min(), int_var->Max()); - associated_variables_.push_back(literal_getter); - solver_->SetNumVariables(num_variables + literal_getter.NumVariableUsed()); - - // Note that we want to be robust to the case where new variables where - // created in the solver using other means than this class. - variable_meaning_.resize(num_variables, std::make_pair(nullptr, 0)); - - // Fill variable_meaning_ and add the "at most one value constraint". - std::vector cst; - int64 value = int_var->Min(); - for (int i = 0; i < literal_getter.NumVariableUsed(); ++i) { - variable_meaning_.push_back(std::make_pair(int_var, value)); - cst.push_back(sat::LiteralWithCoeff(literal_getter.IsEqualTo(value), - sat::Coefficient(1))); - ++value; - } - CHECK(solver_->AddLinearConstraint(false, sat::Coefficient(0), true, - sat::Coefficient(1), &cst)); - return reg_index; -} - -} // namespace operations_research diff --git a/ortools/constraint_solver/sat_constraint.h b/ortools/constraint_solver/sat_constraint.h deleted file mode 100644 index 1e0a41c60b..0000000000 --- a/ortools/constraint_solver/sat_constraint.h +++ /dev/null @@ -1,261 +0,0 @@ -// Copyright 2010-2018 Google LLC -// 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. - -// This file contains the definition and implementation of a constraint -// encapsulating a full SAT solver. Such a constraint can basically propagates -// any relationship between Boolean variables that can be expressed using -// clauses or pseudo-Boolean constraint. -// -// It also contains some utility classes to map an IntVar to a set of Boolean -// variables. Using this, a lot of constraints on integer variables can be dealt -// with quite efficiently by just adding their encoding to the underlying sat -// solver (for instance a table constraint propagated this way should be really -// efficient). -// -// TODO(user): Extend so that the constraint solver can use the conflict -// learning mecanism present in the underlying SAT solver. - -#ifndef OR_TOOLS_CONSTRAINT_SOLVER_SAT_CONSTRAINT_H_ -#define OR_TOOLS_CONSTRAINT_SOLVER_SAT_CONSTRAINT_H_ - -#include "absl/container/flat_hash_map.h" -#include "absl/container/flat_hash_set.h" -#include "ortools/base/hash.h" -#include "ortools/base/map_util.h" -#include "ortools/constraint_solver/constraint_solver.h" -#include "ortools/constraint_solver/constraint_solveri.h" -#include "ortools/sat/sat_solver.h" -#include "ortools/util/tuple_set.h" - -namespace operations_research { - -// Given an IntVar, this class fetches the sat::Literal associated with -// the fact that the variable is equal or not to a given value in its domain. -class IntVarLiteralGetter { - public: - // The mapping of IntVar values to Boolean variables is as follow: - // - We always assume the IntVar to take all possible values in [min, max]. - // - We create one Boolean variable per value: {i, i + 1, ..., i + max - min}. - // - If size([min, max] == 2) then we just use one variable i that represent - // the fact that the variable is bound to its min value. - // - // TODO(user): Support holes in the interval. - IntVarLiteralGetter(sat::BooleanVariable i, int64 min, int64 max) - : first_variable_(i), min_value_(min), max_value_(max) {} - - // Returns the literal encoding (var == value). - sat::Literal IsEqualTo(int64 value) const { - if (max_value_ == min_value_ + 1) { - return sat::Literal(first_variable_, value == min_value_); - } else { - return sat::Literal(first_variable_ + value - min_value_, true); - } - } - - // Returns the literal encoding (var != value). - sat::Literal IsNotEqualTo(int64 value) const { - return IsEqualTo(value).Negated(); - } - - // Returns the number of Boolean variables used for the encoding. - int NumVariableUsed() const { - return (max_value_ == min_value_ + 1) ? 1 : max_value_ - min_value_ + 1; - } - - private: - // These should really be const, but this causes problem with our open source - // build because we use std::vector. - sat::BooleanVariable first_variable_; - int64 min_value_; - int64 max_value_; -}; - -// Creates a new set of Boolean variables for each registered IntVar. These -// variables will encode for each possible value, whether or not the IntVar is -// fixed to this value or not. -// -// This class also provide utility to: -// - Find the Boolean variable associated to an IntVar value. -// - Find the corresponding IntVar value from the Boolean variable. -class BooleanVariableManager { - public: - explicit BooleanVariableManager(sat::SatSolver* solver) : solver_(solver) {} - - // If not already done, this register the given IntVar with this manager and - // creates the underlying Boolean variables in the SAT solver. - // Returns the IntVar registration index. - int RegisterIntVar(IntVar* int_var); - - // Returns the list of registered IntVar. - // Note that they are ordered by registration index. - const std::vector& RegisteredIntVars() const { - return registered_int_vars_; - } - - // Returns the IntVarLiteralGetter associated with the IntVar of given - // registration index. The reg_index can be retrieved with RegisterIntVar() - // or by iterating over RegisteredIntVars(). It must be valid. - const IntVarLiteralGetter& AssociatedBooleanVariables(int reg_index) const { - return associated_variables_[reg_index]; - } - - // A Boolean variable associated to an IntVar value means (var == value) if - // it is true. This returns the IntVar and the value. If the pointer is - // nullptr, then this variable index wasn't created by this class. - std::pair BooleanVariableMeaning( - sat::BooleanVariable var) const { - DCHECK_GE(var, 0); - // This test is necessary because the SAT solver may know of variables not - // registered by this class. - if (var >= variable_meaning_.size()) return std::make_pair(nullptr, 0); - return variable_meaning_[var]; - } - - private: - sat::SatSolver* solver_; - std::vector registered_int_vars_; - std::vector associated_variables_; - absl::flat_hash_map registration_index_map_; - gtl::ITIVector> - variable_meaning_; - DISALLOW_COPY_AND_ASSIGN(BooleanVariableManager); -}; - -// The actual constraint encapsulating the SAT solver. -class SatConstraint : public Constraint { - public: - explicit SatConstraint(Solver* const solver) - : Constraint(solver), - variable_manager_(&sat_solver_), - propagated_trail_index_(0), - rev_decision_level_(0) {} - - // Register the demons. - void Post() override { - int i = 0; - for (IntVar* int_var : variable_manager_.RegisteredIntVars()) { - int_var->WhenDomain(MakeConstraintDemon1( - solver(), this, &SatConstraint::Enqueue, "Enqueue", i)); - ++i; - } - } - - // Initial propagation. - void InitialPropagate() override { - if (sat_solver_.IsModelUnsat()) solver()->Fail(); - for (int i = 0; i < variable_manager_.RegisteredIntVars().size(); ++i) { - Enqueue(i); - } - } - - // Returns the underlying solver and variable manager - // These classes are used to create and add new constraint to the SAT solver. - // Note that any mapping IntVar -> Boolean variable must be done with this - // variable manager for the SatConstraint to properly push back to the - // constraint solver the propagated Boolean variables. - sat::SatSolver* SatSolver() { return &sat_solver_; } - BooleanVariableManager* VariableManager() { return &variable_manager_; } - - private: - // Push variable propagated from sat to the constraint solver. - void PropagateFromSatToCp() { - const sat::Trail& trail = sat_solver_.LiteralTrail(); - while (propagated_trail_index_ < trail.Index()) { - const sat::Literal literal = trail[propagated_trail_index_]; - const sat::BooleanVariable var = literal.Variable(); - if (trail.AssignmentType(var) != sat::AssignmentType::kSearchDecision) { - std::pair p = - variable_manager_.BooleanVariableMeaning(var); - IntVar* int_var = p.first; - const int64 value = p.second; - if (int_var != nullptr) { - if (literal.IsPositive()) { - int_var->SetValue(value); - } else { - int_var->RemoveValue(value); - } - } - } - ++propagated_trail_index_; - } - } - - // Called when more information is known on the IntVar with given registration - // index in the BooleanVariableManager. - void Enqueue(int reg_index) { - if (sat_solver_.CurrentDecisionLevel() > rev_decision_level_.Value()) { - // The constraint solver backtracked. Synchronise the state. - sat_solver_.Backtrack(rev_decision_level_.Value()); - propagated_trail_index_ = - std::min(propagated_trail_index_, sat_solver_.LiteralTrail().Index()); - } - - const IntVar* int_var = variable_manager_.RegisteredIntVars()[reg_index]; - const IntVarLiteralGetter literal_getter = - variable_manager_.AssociatedBooleanVariables(reg_index); - - if (int_var->Bound()) { - if (!EnqueueLiteral(literal_getter.IsEqualTo(int_var->Value()))) { - solver()->Fail(); - } - } else { - const int64 vmin = int_var->Min(); - for (int64 value = int_var->OldMin(); value < vmin; ++value) { - if (!EnqueueLiteral(literal_getter.IsNotEqualTo(value))) { - solver()->Fail(); - } - } - - // TODO(user): Investigate caching the hole iterator. - std::unique_ptr it(int_var->MakeHoleIterator(false)); - for (const int64 value : InitAndGetValues(it.get())) { - if (!EnqueueLiteral(literal_getter.IsNotEqualTo(value))) { - solver()->Fail(); - } - } - const int64 old_max = int_var->OldMax(); - for (int64 value = int_var->Max() + 1; value <= old_max; ++value) { - if (!EnqueueLiteral(literal_getter.IsNotEqualTo(value))) { - solver()->Fail(); - } - } - } - - // TODO(user): Use a constraint solver mechanism to just do that once after - // all the possible Enqueue() have been processed? see delayed demon example - // in expr_array.cc - PropagateFromSatToCp(); - rev_decision_level_.SetValue(solver(), sat_solver_.CurrentDecisionLevel()); - } - - // Try to Enqueue the given literal on the sat_trail. Returns false in case of - // conflict, true otherwise. Note that the literal is only enqueued if it is - // not already set. - bool EnqueueLiteral(sat::Literal literal) { - if (sat_solver_.Assignment().LiteralIsFalse(literal)) return false; - if (sat_solver_.Assignment().LiteralIsTrue(literal)) return true; - if (sat_solver_.EnqueueDecisionIfNotConflicting(literal)) return true; - return false; - } - - sat::SatSolver sat_solver_; - BooleanVariableManager variable_manager_; - int propagated_trail_index_; - Rev rev_decision_level_; - - DISALLOW_COPY_AND_ASSIGN(SatConstraint); -}; - -} // namespace operations_research - -#endif // OR_TOOLS_CONSTRAINT_SOLVER_SAT_CONSTRAINT_H_ diff --git a/ortools/constraint_solver/table.cc b/ortools/constraint_solver/table.cc index da4afd272f..c7026587f2 100644 --- a/ortools/constraint_solver/table.cc +++ b/ortools/constraint_solver/table.cc @@ -28,7 +28,6 @@ #include "ortools/base/map_util.h" #include "ortools/constraint_solver/constraint_solver.h" #include "ortools/constraint_solver/constraint_solveri.h" -#include "ortools/constraint_solver/sat_constraint.h" #include "ortools/util/bitset.h" #include "ortools/util/string_array.h" #include "ortools/util/tuple_set.h"