2025-01-10 11:35:44 +01:00
|
|
|
// Copyright 2010-2025 Google LLC
|
2024-07-12 13:56:11 +02:00
|
|
|
// 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.
|
|
|
|
|
|
2025-11-05 11:34:49 +01:00
|
|
|
#ifndef ORTOOLS_SAT_CP_MODEL_SOLVER_HELPERS_H_
|
|
|
|
|
#define ORTOOLS_SAT_CP_MODEL_SOLVER_HELPERS_H_
|
2024-07-12 13:56:11 +02:00
|
|
|
|
|
|
|
|
#include <cstdint>
|
|
|
|
|
#include <memory>
|
2025-11-05 13:55:12 +01:00
|
|
|
#include <tuple>
|
2024-07-12 13:56:11 +02:00
|
|
|
#include <vector>
|
|
|
|
|
|
2024-12-13 14:50:57 +01:00
|
|
|
#include "absl/types/span.h"
|
2024-07-12 13:56:11 +02:00
|
|
|
#include "ortools/base/timer.h"
|
|
|
|
|
#include "ortools/sat/cp_model.pb.h"
|
2025-11-05 13:55:12 +01:00
|
|
|
#include "ortools/sat/cp_model_solver_logging.h"
|
2024-12-04 17:47:10 +01:00
|
|
|
#include "ortools/sat/integer_base.h"
|
2024-07-12 13:56:11 +02:00
|
|
|
#include "ortools/sat/model.h"
|
|
|
|
|
#include "ortools/sat/sat_parameters.pb.h"
|
|
|
|
|
#include "ortools/sat/stat_tables.h"
|
|
|
|
|
#include "ortools/sat/synchronization.h"
|
|
|
|
|
#include "ortools/sat/util.h"
|
|
|
|
|
#include "ortools/sat/work_assignment.h"
|
|
|
|
|
#include "ortools/util/logging.h"
|
|
|
|
|
|
|
|
|
|
namespace operations_research {
|
|
|
|
|
namespace sat {
|
|
|
|
|
|
|
|
|
|
// Small wrapper containing all the shared classes between our subsolver
|
|
|
|
|
// threads. Note that all these classes can also be retrieved with something
|
|
|
|
|
// like global_model->GetOrCreate<Class>() but it is not thread-safe to do so.
|
|
|
|
|
//
|
|
|
|
|
// All the classes here should be thread-safe, or at least safe in the way they
|
|
|
|
|
// are accessed. For instance the model_proto will be kept constant for the
|
|
|
|
|
// whole duration of the solve.
|
|
|
|
|
struct SharedClasses {
|
|
|
|
|
SharedClasses(const CpModelProto* proto, Model* global_model);
|
|
|
|
|
|
|
|
|
|
// These are never nullptr.
|
|
|
|
|
const CpModelProto& model_proto;
|
|
|
|
|
WallTimer* const wall_timer;
|
|
|
|
|
ModelSharedTimeLimit* const time_limit;
|
|
|
|
|
SolverLogger* const logger;
|
|
|
|
|
SharedStatistics* const stats;
|
2024-12-04 15:29:31 +01:00
|
|
|
SharedStatTables* const stat_tables;
|
2024-07-12 13:56:11 +02:00
|
|
|
SharedResponseManager* const response;
|
|
|
|
|
SharedTreeManager* const shared_tree_manager;
|
2024-12-04 15:29:31 +01:00
|
|
|
SharedLsSolutionRepository* const ls_hints;
|
2025-11-05 13:55:12 +01:00
|
|
|
SolverProgressLogger* const progress_logger;
|
2025-11-17 16:42:09 +01:00
|
|
|
SharedLratProofStatus* const lrat_proof_status;
|
2024-07-12 13:56:11 +02:00
|
|
|
|
|
|
|
|
// These can be nullptr depending on the options.
|
|
|
|
|
std::unique_ptr<SharedBoundsManager> bounds;
|
|
|
|
|
std::unique_ptr<SharedLPSolutionRepository> lp_solutions;
|
|
|
|
|
std::unique_ptr<SharedIncompleteSolutionManager> incomplete_solutions;
|
|
|
|
|
std::unique_ptr<SharedClausesManager> clauses;
|
2025-07-21 17:25:33 +02:00
|
|
|
std::unique_ptr<SharedLinear2Bounds> linear2_bounds;
|
2024-07-12 13:56:11 +02:00
|
|
|
|
2024-12-04 15:29:31 +01:00
|
|
|
// call local_model->Register() on most of the class here, this allow to
|
|
|
|
|
// more easily depends on one of the shared class deep within the solver.
|
|
|
|
|
void RegisterSharedClassesInLocalModel(Model* local_model);
|
2024-07-12 13:56:11 +02:00
|
|
|
|
|
|
|
|
bool SearchIsDone();
|
2025-07-21 17:25:33 +02:00
|
|
|
|
|
|
|
|
void LogFinalStatistics();
|
2024-07-12 13:56:11 +02:00
|
|
|
};
|
|
|
|
|
|
|
|
|
|
// Loads a CpModelProto inside the given model.
|
|
|
|
|
// This should only be called once on a given 'Model' class.
|
|
|
|
|
void LoadCpModel(const CpModelProto& model_proto, Model* model);
|
|
|
|
|
|
|
|
|
|
// Solves an already loaded cp_model_proto.
|
|
|
|
|
// The final CpSolverResponse must be read from the shared_response_manager.
|
|
|
|
|
//
|
|
|
|
|
// TODO(user): This should be transformed so that it can be called many times
|
|
|
|
|
// and resume from the last search state as if it wasn't interrupted. That would
|
|
|
|
|
// allow use to easily interleave different heuristics in the same thread.
|
|
|
|
|
void SolveLoadedCpModel(const CpModelProto& model_proto, Model* model);
|
|
|
|
|
|
|
|
|
|
// Registers a callback that will export variables bounds fixed at level 0 of
|
|
|
|
|
// the search. This should not be registered to a LNS search.
|
|
|
|
|
void RegisterVariableBoundsLevelZeroExport(
|
|
|
|
|
const CpModelProto& /*model_proto*/,
|
|
|
|
|
SharedBoundsManager* shared_bounds_manager, Model* model);
|
|
|
|
|
|
|
|
|
|
// Registers a callback to import new variables bounds stored in the
|
|
|
|
|
// shared_bounds_manager. These bounds are imported at level 0 of the search
|
|
|
|
|
// in the linear scan minimize function.
|
|
|
|
|
void RegisterVariableBoundsLevelZeroImport(
|
|
|
|
|
const CpModelProto& model_proto, SharedBoundsManager* shared_bounds_manager,
|
|
|
|
|
Model* model);
|
|
|
|
|
|
|
|
|
|
// Registers a callback that will report improving objective best bound.
|
|
|
|
|
// It will be called each time new objective bound are propagated at level zero.
|
|
|
|
|
void RegisterObjectiveBestBoundExport(
|
|
|
|
|
IntegerVariable objective_var,
|
|
|
|
|
SharedResponseManager* shared_response_manager, Model* model);
|
|
|
|
|
|
|
|
|
|
// Registers a callback to import new objective bounds. It will be called each
|
|
|
|
|
// time the search main loop is back to level zero. Note that it the presence of
|
|
|
|
|
// assumptions, this will not happen until the set of assumptions is changed.
|
|
|
|
|
void RegisterObjectiveBoundsImport(
|
|
|
|
|
SharedResponseManager* shared_response_manager, Model* model);
|
|
|
|
|
|
|
|
|
|
// Registers a callback that will export good clauses discovered during search.
|
|
|
|
|
void RegisterClausesExport(int id, SharedClausesManager* shared_clauses_manager,
|
|
|
|
|
Model* model);
|
|
|
|
|
|
|
|
|
|
// Registers a callback to import new clauses stored in the
|
|
|
|
|
// shared_clausess_manager. These clauses are imported at level 0 of the search
|
|
|
|
|
// in the linear scan minimize function.
|
|
|
|
|
// it returns the id of the worker in the shared clause manager.
|
|
|
|
|
//
|
|
|
|
|
// TODO(user): Can we import them in the core worker ?
|
|
|
|
|
int RegisterClausesLevelZeroImport(int id,
|
|
|
|
|
SharedClausesManager* shared_clauses_manager,
|
|
|
|
|
Model* model);
|
|
|
|
|
|
2025-07-21 17:25:33 +02:00
|
|
|
// This will register a level zero callback to imports new linear2 from the
|
|
|
|
|
// SharedLinear2Bounds.
|
|
|
|
|
void RegisterLinear2BoundsImport(SharedLinear2Bounds* shared_linear2_bounds,
|
|
|
|
|
Model* model);
|
|
|
|
|
|
2024-07-12 13:56:11 +02:00
|
|
|
void PostsolveResponseWrapper(const SatParameters& params,
|
|
|
|
|
int num_variable_in_original_model,
|
|
|
|
|
const CpModelProto& mapping_proto,
|
2024-12-13 14:50:57 +01:00
|
|
|
absl::Span<const int> postsolve_mapping,
|
2024-07-12 13:56:11 +02:00
|
|
|
std::vector<int64_t>* solution);
|
|
|
|
|
|
|
|
|
|
// Try to find a solution by following the hint and using a low conflict limit.
|
|
|
|
|
// The CpModelProto must already be loaded in the Model.
|
|
|
|
|
void QuickSolveWithHint(const CpModelProto& model_proto, Model* model);
|
|
|
|
|
|
|
|
|
|
// Solve a model with a different objective consisting of minimizing the L1
|
|
|
|
|
// distance with the provided hint. Note that this method creates an in-memory
|
|
|
|
|
// copy of the model and loads a local Model object from the copied model.
|
|
|
|
|
void MinimizeL1DistanceWithHint(const CpModelProto& model_proto, Model* model);
|
|
|
|
|
|
|
|
|
|
void LoadFeasibilityPump(const CpModelProto& model_proto, Model* model);
|
|
|
|
|
|
|
|
|
|
void AdaptGlobalParameters(const CpModelProto& model_proto, Model* model);
|
|
|
|
|
|
|
|
|
|
// This should be called on the presolved model. It will read the file
|
|
|
|
|
// specified by --cp_model_load_debug_solution and properly fill the
|
|
|
|
|
// model->Get<DebugSolution>() proto vector.
|
|
|
|
|
void LoadDebugSolution(const CpModelProto& model_proto, Model* model);
|
|
|
|
|
|
|
|
|
|
} // namespace sat
|
|
|
|
|
} // namespace operations_research
|
|
|
|
|
|
2025-11-05 11:34:49 +01:00
|
|
|
#endif // ORTOOLS_SAT_CP_MODEL_SOLVER_HELPERS_H_
|