diff --git a/ortools/sat/cp_model.cc b/ortools/sat/cp_model.cc index d724d33d4c..554b279d30 100644 --- a/ortools/sat/cp_model.cc +++ b/ortools/sat/cp_model.cc @@ -348,8 +348,8 @@ int CpModelBuilder::GetOrCreateIntegerIndex(int index) { return index; } if (!gtl::ContainsKey(bool_to_integer_index_map_, index)) { - const int ref = PositiveRef(index); - const IntegerVariableProto& old_var = cp_model_.variables(ref); + const int var = PositiveRef(index); + const IntegerVariableProto& old_var = cp_model_.variables(var); const int new_index = cp_model_.variables_size(); IntegerVariableProto* const new_var = cp_model_.add_variables(); new_var->add_domain(0); @@ -814,6 +814,52 @@ void CpModelBuilder::ClearAssumptions() { cp_model_.mutable_assumptions()->Clear(); } +void CpModelBuilder::CopyFrom(const CpModelProto& model_proto) { + cp_model_ = model_proto; + // Rebuild constant to index map. + constant_to_index_map_.clear(); + for (int i = 0; i < cp_model_.variables_size(); ++i) { + const IntegerVariableProto& var = cp_model_.variables(i); + if (var.domain_size() == 2 && var.domain(0) == var.domain(1)) { + constant_to_index_map_[var.domain(0)] = i; + } + } + // This one would be more complicated to rebuild. Let's just clear it. + bool_to_integer_index_map_.clear(); +} + +BoolVar CpModelBuilder::GetBoolVarFromProtoIndex(int index) { + CHECK_GE(index, 0); + CHECK_LT(index, cp_model_.variables_size()); + const IntegerVariableProto& proto = cp_model_.variables(index); + CHECK_EQ(2, proto.domain_size()) + << "CpModelBuilder::GetBoolVarFromProtoIndex: The domain of the variable " + "is not Boolean"; + CHECK_GE(0, proto.domain(0)) + << "CpModelBuilder::GetBoolVarFromProtoIndex: The domain of the variable " + "is not Boolean"; + CHECK_LE(1, proto.domain(1)) + << "CpModelBuilder::GetBoolVarFromProtoIndex: The domain of the variable " + "is not Boolean"; + return BoolVar(index, &cp_model_); +} + +IntVar CpModelBuilder::GetIntVarFromProtoIndex(int index) { + CHECK_GE(index, 0); + CHECK_LT(index, cp_model_.variables_size()); + return IntVar(index, &cp_model_); +} + +IntervalVar CpModelBuilder::GetIntervalVarFromProtoIndex(int index) { + CHECK_GE(index, 0); + CHECK_LT(index, cp_model_.constraints_size()); + const ConstraintProto& ct = cp_model_.constraints(index); + CHECK_EQ(ct.constraint_case(), ConstraintProto::kInterval) + << "CpModelBuilder::GetIntervalVarFromProtoIndex: the referenced " + "object is not an interval variable"; + return IntervalVar(index, &cp_model_); +} + int64 SolutionIntegerValue(const CpSolverResponse& r, const LinearExpr& expr) { int64 result = expr.constant(); for (int i = 0; i < expr.variables().size(); ++i) { diff --git a/ortools/sat/cp_model.h b/ortools/sat/cp_model.h index e64770d8dd..a1db14b726 100644 --- a/ortools/sat/cp_model.h +++ b/ortools/sat/cp_model.h @@ -878,6 +878,18 @@ class CpModelBuilder { const CpModelProto& Proto() const { return cp_model_; } CpModelProto* MutableProto() { return &cp_model_; } + /// Replace the current model with the one from the given proto. + void CopyFrom(const CpModelProto& model_proto); + + /// Returns the Boolean variable from its index in the proto. + BoolVar GetBoolVarFromProtoIndex(int index); + + /// Returns the integer variable from its index in the proto. + IntVar GetIntVarFromProtoIndex(int index); + + /// Returns the interval variable from its index in the proto. + IntervalVar GetIntervalVarFromProtoIndex(int index); + private: friend class CumulativeConstraint; friend class ReservoirConstraint; diff --git a/ortools/sat/cp_model_solver.cc b/ortools/sat/cp_model_solver.cc index f9a7a5bbdb..89626007d3 100644 --- a/ortools/sat/cp_model_solver.cc +++ b/ortools/sat/cp_model_solver.cc @@ -1600,9 +1600,10 @@ void SolveLoadedCpModel(const CpModelProto& model_proto, solution_info); // Extract a good subset of assumptions and add it to the response. + auto* time_limit = model->GetOrCreate(); auto* sat_solver = model->GetOrCreate(); std::vector core = sat_solver->GetLastIncompatibleDecisions(); - MinimizeCoreWithPropagation(sat_solver, &core); + MinimizeCoreWithPropagation(time_limit, sat_solver, &core); std::vector core_in_proto_format; for (const Literal l : core) { core_in_proto_format.push_back( diff --git a/ortools/sat/cp_model_symmetries.cc b/ortools/sat/cp_model_symmetries.cc index 41b9913644..69b2ca7cc1 100644 --- a/ortools/sat/cp_model_symmetries.cc +++ b/ortools/sat/cp_model_symmetries.cc @@ -315,10 +315,31 @@ std::unique_ptr GenerateGraphForSymmetryDetection( graph->Build(); DCHECK_EQ(graph->num_nodes(), initial_equivalence_classes->size()); + // TODO(user): The symmetry code does not officially support multi-arcs. And + // we shouldn't have any as long as there is no duplicates variable in our + // constraints (but of course, we can't always guarantee that). That said, + // because the symmetry code really only look at the degree, it works as long + // as the maximum degree is bounded by num_nodes. + const int num_nodes = graph->num_nodes(); + std::vector in_degree(num_nodes, 0); + std::vector out_degree(num_nodes, 0); + for (int i = 0; i < num_nodes; ++i) { + out_degree[i] = graph->OutDegree(i); + for (const int head : (*graph)[i]) { + in_degree[head]++; + } + } + for (int i = 0; i < num_nodes; ++i) { + if (in_degree[i] >= num_nodes || out_degree[i] >= num_nodes) { + LOG(ERROR) << "Too many multi-arcs"; + return nullptr; + } + } + // Because this code is running during presolve, a lot a variable might have // no edges. We do not want to detect symmetries between these. // - // Note that this code forces us to "densify" the ids aftewards because the + // Note that this code forces us to "densify" the ids afterwards because the // symmetry detection code relies on that. // // TODO(user): It will probably be more efficient to not even create these diff --git a/ortools/sat/optimization.cc b/ortools/sat/optimization.cc index 9c356712de..5be4dafd2c 100644 --- a/ortools/sat/optimization.cc +++ b/ortools/sat/optimization.cc @@ -215,7 +215,7 @@ class FuMalikSymmetryBreaker { } // namespace -void MinimizeCoreWithPropagation(SatSolver* solver, +void MinimizeCoreWithPropagation(TimeLimit* limit, SatSolver* solver, std::vector* core) { if (solver->IsModelUnsat()) return; std::set moved_last; @@ -223,7 +223,7 @@ void MinimizeCoreWithPropagation(SatSolver* solver, solver->Backtrack(0); solver->SetAssumptionLevel(0); - while (true) { + while (!limit->LimitReached()) { // We want each literal in candidate to appear last once in our propagation // order. We want to do that while maximizing the reutilization of the // current assignment prefix, that is minimizing the number of @@ -232,7 +232,7 @@ void MinimizeCoreWithPropagation(SatSolver* solver, moved_last, solver->CurrentDecisionLevel(), &candidate); if (target_level == -1) break; solver->Backtrack(target_level); - while (!solver->IsModelUnsat() && + while (!solver->IsModelUnsat() && !limit->LimitReached() && solver->CurrentDecisionLevel() < candidate.size()) { const Literal decision = candidate[solver->CurrentDecisionLevel()]; if (solver->Assignment().LiteralIsTrue(decision)) { @@ -1220,7 +1220,7 @@ SatSolver::Status FindCores(std::vector assumptions, if (result != SatSolver::ASSUMPTIONS_UNSAT) return result; std::vector core = sat_solver->GetLastIncompatibleDecisions(); if (sat_solver->parameters().minimize_core()) { - MinimizeCoreWithPropagation(sat_solver, &core); + MinimizeCoreWithPropagation(limit, sat_solver, &core); } CHECK(!core.empty()); cores->push_back(core); @@ -1282,7 +1282,7 @@ SatSolver::Status FindMultipleCoresForMaxHs( if (result != SatSolver::ASSUMPTIONS_UNSAT) return result; std::vector core = sat_solver->GetLastIncompatibleDecisions(); if (sat_solver->parameters().minimize_core()) { - MinimizeCoreWithPropagation(sat_solver, &core); + MinimizeCoreWithPropagation(limit, sat_solver, &core); } CHECK(!core.empty()); cores->push_back(core); diff --git a/ortools/sat/optimization.h b/ortools/sat/optimization.h index 288cd1de11..59246b0e34 100644 --- a/ortools/sat/optimization.h +++ b/ortools/sat/optimization.h @@ -35,7 +35,10 @@ namespace sat { // removed. // // Note that this function doest NOT preserve the order of Literal in the core. -void MinimizeCoreWithPropagation(SatSolver* solver, std::vector* core); +// +// TODO(user): Avoid spending too much time trying to minimize a core. +void MinimizeCoreWithPropagation(TimeLimit* limit, SatSolver* solver, + std::vector* core); // Because the Solve*() functions below are also used in scripts that requires a // special output format, we use this to tell them whether or not to use the diff --git a/ortools/sat/python/cp_model.py b/ortools/sat/python/cp_model.py index 545b3b93a1..d603651e8f 100644 --- a/ortools/sat/python/cp_model.py +++ b/ortools/sat/python/cp_model.py @@ -454,11 +454,22 @@ class IntVar(LinearExpr): def __init__(self, model, domain, name): """See CpModel.NewIntVar below.""" self.__model = model - self.__index = len(model.variables) - self.__var = model.variables.add() - self.__var.domain.extend(domain.FlattenedIntervals()) - self.__var.name = name self.__negation = None + # Python do not support multiple __init__ methods. + # This method is only called from the CpModel class. + # We hack the parameter to support the two cases: + # case 1: + # model is a CpModelProto, domain is a Domain, and name is a string. + # case 2: + # model is a CpModelProto, domain is an index (int), and name is None. + if isinstance(domain, numbers.Integral) and name is None: + self.__index = domain + self.__var = model.variables[domain] + else: + self.__index = len(model.variables) + self.__var = model.variables.add() + self.__var.domain.extend(domain.FlattenedIntervals()) + self.__var.name = name def Index(self): """Returns the index of the variable in the model.""" @@ -638,15 +649,28 @@ class IntervalVar(object): def __init__(self, model, start_index, size_index, end_index, is_present_index, name): self.__model = model - self.__index = len(model.constraints) - self.__ct = self.__model.constraints.add() - self.__ct.interval.start = start_index - self.__ct.interval.size = size_index - self.__ct.interval.end = end_index - if is_present_index is not None: - self.__ct.enforcement_literal.append(is_present_index) - if name: - self.__ct.name = name + # As with the IntVar::__init__ method, we hack the __init__ method to + # support two use cases: + # case 1: called when creating a new interval variable. + # {start|size|end}_index are indices of integer variables + # is_present_index is either None or the index of a Boolean literal. + # name is a string + # case 2: called when querying an existing interval variable. + # start_index is an int, all parameters after are None. + if (size_index is None and end_index is None and + is_present_index is None and name is None): + self.__index = start_index + self.__ct = model.constraints[start_index] + else: + self.__index = len(model.constraints) + self.__ct = self.__model.constraints.add() + self.__ct.interval.start = start_index + self.__ct.interval.size = size_index + self.__ct.interval.end = end_index + if is_present_index is not None: + self.__ct.enforcement_literal.append(is_present_index) + if name: + self.__ct.name = name def Index(self): """Returns the index of the interval constraint in the model.""" @@ -689,7 +713,6 @@ class CpModel(object): def __init__(self): self.__model = cp_model_pb2.CpModelProto() self.__constant_map = {} - self.__optional_constant_map = {} # Integer variable. @@ -733,7 +756,8 @@ class CpModel(object): def NewConstant(self, value): """Declares a constant integer.""" - return IntVar(self.__model, Domain(value, value), '') + return IntVar(self.__model, self.GetOrMakeIndexFromConstant(value), + None) # Linear constraints. @@ -1392,6 +1416,50 @@ class CpModel(object): model_ct.cumulative.capacity = self.GetOrMakeIndex(capacity) return ct + # Support for deep copy. + def CopyFrom(self, other_model): + """Reset the model, and creates a new one from a CpModelProto instance.""" + self.__model = other_model.Proto() + + # Rebuild constant map. + self.__constant_map.clear() + for i, var in enumerate(self.__model.variables): + if len(var.domain) == 2 and var.domain[0] == var.domain[1]: + self.__constant_map[var.domain[0]] = i + + def GetBoolVarFromProtoIndex(self, index): + """Returns an already created Boolean variable from its index.""" + if index < 0 or index >= len(self.__model.variables): + raise ValueError( + f'GetBoolVarFromProtoIndex: out of bound index {index}') + var = self.__model.variables[index] + if len(var.domain) != 2 or var.domain[0] < 0 or var.domain[1] > 1: + raise ValueError( + f'GetBoolVarFromProtoIndex: index {index} does not reference' + + ' a Boolean variable') + + return IntVar(self.__model, index, None) + + def GetIntVarFromProtoIndex(self, index): + """Returns an already created integer variable from its index.""" + if index < 0 or index >= len(self.__model.variables): + raise ValueError( + f'GetIntVarFromProtoIndex: out of bound index {index}') + return IntVar(self.__model, index, None) + + def GetIntervalVarFromProtoIndex(self, index): + """Returns an already created interval variable from its index.""" + if index < 0 or index >= len(self.__model.constraints): + raise ValueError( + f'GetIntervalVarFromProtoIndex: out of bound index {index}') + ct = self.__model.constraints[index] + if not ct.HasField('interval'): + raise ValueError( + f'GetIntervalVarFromProtoIndex: index {index} does not reference an' + + ' interval variable') + + return IntervalVar(self.__model, index, None, None, None, None) + # Helpers. def __str__(self):