18#include "absl/status/status.h"
19#include "absl/status/statusor.h"
24#include "ortools/linear_solver/linear_solver.pb.h"
27#include "ortools/sat/cp_model.pb.h"
35#if defined(PROTOBUF_INTERNAL_IMPL)
36using google::protobuf::Message;
38using google::protobuf::Message;
51 void Reset()
override;
59 const MPVariable*
const variable,
double new_value,
60 double old_value)
override;
77 bool IsLP()
const override;
78 bool IsMIP()
const override;
99 void NonIncrementalChange();
101 std::atomic<bool> interrupt_solve_;
102 sat::SatParameters parameters_;
103 int num_threads_ = 8;
112 interrupt_solve_ =
false;
120 solver_->solver_specific_parameter_string_);
125 parameters_.set_max_time_in_seconds(
130 for (
int i = 0; i <
solver_->variables_.size(); ++i) {
133 for (
int i = 0; i <
solver_->constraints_.size(); ++i) {
137 MPModelRequest request;
139 request.set_solver_specific_parameters(
141 request.set_enable_internal_solver_output(!
quiet_);
142 const absl::StatusOr<MPSolutionResponse> status_or =
146 const MPSolutionResponse&
response = status_or.value();
151 case MPSOLVER_OPTIMAL:
154 case MPSOLVER_FEASIBLE:
157 case MPSOLVER_INFEASIBLE:
160 case MPSOLVER_MODEL_INVALID:
170 if (
response.status() == MPSOLVER_FEASIBLE ||
171 response.status() == MPSOLVER_OPTIMAL) {
174 const size_t num_vars =
solver_->variables_.size();
175 for (
int var_id = 0; var_id < num_vars; ++var_id) {
177 var->set_solution_value(
response.variable_value(var_id));
185 interrupt_solve_ =
true;
192 NonIncrementalChange();
196 NonIncrementalChange();
200 NonIncrementalChange();
204 NonIncrementalChange();
208 NonIncrementalChange();
212 NonIncrementalChange();
217 double new_value,
double old_value) {
218 NonIncrementalChange();
222 NonIncrementalChange();
227 NonIncrementalChange();
241 return MPSolver::BasisStatus::FREE;
245 return MPSolver::BasisStatus::FREE;
253 return "SAT Based MIP Solver";
267 parameters_.set_num_search_workers(num_threads_);
268 parameters_.set_log_search_progress(!
quiet_);
273 num_threads_ = num_threads;
274 return absl::OkStatus();
292void SatInterface::NonIncrementalChange() {
#define VLOG(verboselevel)
The class for constraints of a Mathematical Programming (MP) model.
This mathematical programming (MP) solver class is the main class though which users build and solve ...
ResultStatus
The status of solving the problem.
@ FEASIBLE
feasible, or stopped by limit.
@ NOT_SOLVED
not been solved yet.
@ INFEASIBLE
proven infeasible.
@ ABNORMAL
abnormal, i.e., error of some kind.
@ MODEL_INVALID
the model is trivially invalid (NaN coefficients, etc).
bool SetSolverSpecificParametersAsString(const std::string ¶meters)
Advanced usage: pass solver specific parameters in text format.
void ExportModelToProto(MPModelProto *output_model) const
Exports model to protocol buffer.
BasisStatus
Advanced usage: possible basis status values for a variable and the slack variable of a linear constr...
void set_constraint_as_extracted(int ct_index, bool extracted)
MPSolver::ResultStatus result_status_
double best_objective_bound_
void ResetExtractionInformation()
void set_variable_as_extracted(int var_index, bool extracted)
void SetCommonParameters(const MPSolverParameters ¶m)
SynchronizationStatus sync_status_
This class stores parameter settings for LP and MIP solvers.
The class for variables of a Mathematical Programming (MP) model.
void SetScalingMode(int value) override
void SetDualTolerance(double value) override
void AddRowConstraint(MPConstraint *const ct) override
void SetLpAlgorithm(int value) override
SatInterface(MPSolver *const solver)
int64 nodes() const override
void ExtractObjective() override
void * underlying_solver() override
bool IsContinuous() const override
bool InterruptSolve() override
MPSolver::ResultStatus Solve(const MPSolverParameters ¶m) override
void SetPrimalTolerance(double value) override
void ClearConstraint(MPConstraint *const constraint) override
bool SetSolverSpecificParametersAsString(const std::string ¶meters) override
void SetObjectiveCoefficient(const MPVariable *const variable, double coefficient) override
void SetCoefficient(MPConstraint *const constraint, const MPVariable *const variable, double new_value, double old_value) override
MPSolver::BasisStatus row_status(int constraint_index) const override
void SetObjectiveOffset(double value) override
void SetVariableInteger(int index, bool integer) override
void SetParameters(const MPSolverParameters ¶m) override
void ExtractNewConstraints() override
std::string SolverVersion() const override
void SetRelativeMipGap(double value) override
void SetConstraintBounds(int index, double lb, double ub) override
absl::Status SetNumThreads(int num_threads) override
void SetPresolveMode(int value) override
void SetVariableBounds(int index, double lb, double ub) override
void AddVariable(MPVariable *const var) override
void ExtractNewVariables() override
bool IsLP() const override
bool IsMIP() const override
bool AddIndicatorConstraint(MPConstraint *const ct) override
void SetOptimizationDirection(bool maximize) override
MPSolver::BasisStatus column_status(int variable_index) const override
int64 iterations() const override
void ClearObjective() override
SharedResponseManager * response
A C++ wrapper that provides a simple and unified interface to several linear programming and mixed in...
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...
bool ProtobufTextFormatMergeFromString(const std::string &proto_text_string, ProtoType *proto)
std::string EncodeSatParametersAsString(const sat::SatParameters ¶meters)
MPSolverInterface * BuildSatInterface(MPSolver *const solver)
absl::StatusOr< MPSolutionResponse > SatSolveProto(MPModelRequest request, std::atomic< bool > *interrupt_solve)