diff --git a/ortools/linear_solver/linear_solver.proto b/ortools/linear_solver/linear_solver.proto index cf0177325c..3aae55ebad 100644 --- a/ortools/linear_solver/linear_solver.proto +++ b/ortools/linear_solver/linear_solver.proto @@ -263,6 +263,7 @@ message MPModelRequest { // rejected and yield an RPC Application error with code // MPSOLVER_MODEL_INVALID_SOLVER_PARAMETERS. optional string solver_specific_parameters = 5; + } // Status returned by the solver. They follow a hierarchical nomenclature, to diff --git a/ortools/lp_data/lp_data.cc b/ortools/lp_data/lp_data.cc index 1910ce046b..b7ac8d59e7 100644 --- a/ortools/lp_data/lp_data.cc +++ b/ortools/lp_data/lp_data.cc @@ -595,6 +595,7 @@ std::string LinearProgram::DumpSolution(const DenseRow& variable_values) const { return output; } + std::string LinearProgram::GetProblemStats() const { return ProblemStatFormatter( "%d,%d,%lld,%d,%d,%d,%d,%d,%d,%d,%d,%d,%d,%d," diff --git a/ortools/lp_data/lp_data.h b/ortools/lp_data/lp_data.h index ac6771bd45..3081ffc6a3 100644 --- a/ortools/lp_data/lp_data.h +++ b/ortools/lp_data/lp_data.h @@ -291,6 +291,7 @@ class LinearProgram { // format var1 = X, var2 = Y, var3 = Z, ... std::string DumpSolution(const DenseRow& variable_values) const; + // Returns a comma-separated std::string of integers containing (in that order) // num_constraints_, num_variables_in_file_, num_entries_, // num_objective_non_zeros_, num_rhs_non_zeros_, num_less_than_constraints_, diff --git a/ortools/sat/cp_model_solver.cc b/ortools/sat/cp_model_solver.cc index e38ffb66e8..62ee50a965 100644 --- a/ortools/sat/cp_model_solver.cc +++ b/ortools/sat/cp_model_solver.cc @@ -1798,6 +1798,23 @@ void ExtractLinearObjective(const CpModelProto& model_proto, } } +} // namespace + +// Used by NewFeasibleSolutionObserver to register observers. +struct SolutionObservers { + explicit SolutionObservers(Model* model) {} + std::vector& values)>> observers; +}; + +std::function NewFeasibleSolutionObserver( + const std::function& values)>& observer) { + return [=](Model* model) { + model->GetOrCreate()->observers.push_back(observer); + }; +} + +namespace { + CpSolverResponse SolveCpModelInternal(const CpModelProto& model_proto, bool display_fixing_constraints, Model* model) { @@ -1939,10 +1956,28 @@ CpSolverResponse SolveCpModelInternal(const CpModelProto& model_proto, int num_solutions = 0; SatSolver::Status status; if (!model_proto.has_objective()) { - status = SolveIntegerProblemWithLazyEncoding( - /*assumptions=*/{}, next_decision, model); - if (status == SatSolver::MODEL_SAT) { - FillSolutionInResponse(model_proto, m, &response); + int num_solutions = 0; + while (true) { + status = SolveIntegerProblemWithLazyEncoding( + /*assumptions=*/{}, next_decision, model); + if (status != SatSolver::Status::MODEL_SAT) break; + + // TODO(user): add all solutions to the response? or their count? + if (num_solutions == 0) { + FillSolutionInResponse(model_proto, m, &response); + } + + ++num_solutions; + for (const auto& observer : + m.GetOrCreate()->observers) { + observer(m.ExtractFullAssignment()); + } + + if (!parameters.enumerate_all_solutions()) break; + model->Add(ExcludeCurrentSolutionAndBacktrack()); + } + if (num_solutions > 0) { + status = SatSolver::Status::MODEL_SAT; } } else { // Optimization problem. @@ -1952,6 +1987,10 @@ CpSolverResponse SolveCpModelInternal(const CpModelProto& model_proto, [&model_proto, &response, &num_solutions, &obj, &m, objective_var](const Model& sat_model) { num_solutions++; + for (const auto observer : + m.GetOrCreate()->observers) { + observer(m.ExtractFullAssignment()); + } FillSolutionInResponse(model_proto, m, &response); int64 objective_value = 0; for (int i = 0; i < model_proto.objective().vars_size(); ++i) { @@ -2041,22 +2080,6 @@ CpSolverResponse SolveCpModelInternal(const CpModelProto& model_proto, } // namespace -CpSolverResponse SolveCpModelWithoutPresolve(const CpModelProto& model_proto, - Model* model) { - // Validate model_proto. - // TODO(user): provide an option to skip this step for speed? - { - const std::string error = ValidateCpModel(model_proto); - if (!error.empty()) { - VLOG(1) << error; - CpSolverResponse response; - response.set_status(CpSolverStatus::MODEL_INVALID); - return response; - } - } - return SolveCpModelInternal(model_proto, true, model); -} - CpSolverResponse SolveCpModel(const CpModelProto& model_proto, Model* model) { // Validate model_proto. // TODO(user): provide an option to skip this step for speed? @@ -2070,6 +2093,12 @@ CpSolverResponse SolveCpModel(const CpModelProto& model_proto, Model* model) { } } + const SatParameters& parameters = + model->GetOrCreate()->parameters(); + if (!parameters.cp_model_presolve()) { + return SolveCpModelInternal(model_proto, true, model); + } + CpModelProto presolved_proto; CpModelProto mapping_proto; std::vector postsolve_mapping; diff --git a/ortools/sat/cp_model_solver.h b/ortools/sat/cp_model_solver.h index b82eb48ed9..9f05b7b5db 100644 --- a/ortools/sat/cp_model_solver.h +++ b/ortools/sat/cp_model_solver.h @@ -33,15 +33,16 @@ std::string CpSolverResponseStats(const CpSolverResponse& response); // representation of the given CpModelProto. It is done this way so that it is // easy to set custom parameters or time limit on the model with calls like: // - model->SetSingleton(std::move(time_limit)); -// - model->Add(NewSatParameters(parameters_as_string)); +// - model->Add(NewSatParameters(parameters_as_string_or_proto)); CpSolverResponse SolveCpModel(const CpModelProto& model_proto, Model* model); -// Same as above, but do not run the CpModelProto presolver. This is exposed for -// internal usage, all client should use the version above. -// -// TODO(user): add a parameters to enable/disable the presolve. -CpSolverResponse SolveCpModelWithoutPresolve(const CpModelProto& model_proto, - Model* model); +// Allows to register a solution "observer" with the model with +// model.Add(NewFeasibleSolutionObserver([](values){...})); +// The given function will be called on each feasible solution found during the +// search. The values will be in one to one correspondence with the variables +// in the model_proto. +std::function NewFeasibleSolutionObserver( + const std::function& values)>& observer); } // namespace sat } // namespace operations_research diff --git a/ortools/sat/sat_parameters.proto b/ortools/sat/sat_parameters.proto index 5e06d1baee..dc238505e9 100644 --- a/ortools/sat/sat_parameters.proto +++ b/ortools/sat/sat_parameters.proto @@ -18,7 +18,7 @@ package operations_research.sat; // Contains the definitions for all the sat algorithm parameters and their // default values. // -// NEXT TAG: 86 +// NEXT TAG: 88 message SatParameters { // ========================================================================== // Branching and polarity @@ -497,4 +497,10 @@ message SatParameters { // "Automatic Logic-Based Benders Decomposition with MiniZinc" // http://aaai.org/ocs/index.php/AAAI/AAAI17/paper/view/14489 optional bool optimize_with_max_hs = 85 [default = false]; + + // Wheter we presolve the cp_model before solving it. + optional bool cp_model_presolve = 86 [default = true]; + + // Wheter we enumerate all solutions of a SAT problem. + optional bool enumerate_all_solutions = 87 [default = false]; } diff --git a/ortools/util/time_limit.h b/ortools/util/time_limit.h index 4bc582f555..2cd49ea78a 100644 --- a/ortools/util/time_limit.h +++ b/ortools/util/time_limit.h @@ -212,7 +212,7 @@ return 1e-9 * (base::GetCurrentTimeNanos() - start_ns_); const int64 safety_buffer_ns_; RunningMax running_max_; -// Only used when FLAGS_time_limit_use_usertime is true. + // Only used when FLAGS_time_limit_use_usertime is true. UserTimer user_timer_; double limit_in_seconds_;