14#ifndef OR_TOOLS_SAT_OPTIMIZATION_H_
15#define OR_TOOLS_SAT_OPTIMIZATION_H_
20#include "ortools/sat/boolean_problem.pb.h"
41 std::vector<Literal>* core);
68 const LinearBooleanProblem& problem,
70 std::vector<bool>* solution);
81 const LinearBooleanProblem& problem,
82 SatSolver* solver, std::vector<bool>* solution);
89 const LinearBooleanProblem& problem,
90 int num_times, SatSolver* solver,
91 std::vector<bool>* solution);
101 const LinearBooleanProblem& problem,
103 std::vector<bool>* solution);
109 LogBehavior log,
const LinearBooleanProblem& problem, SatSolver* solver,
110 std::vector<bool>* solution);
115 LogBehavior log,
const LinearBooleanProblem& problem, SatSolver* solver,
116 std::vector<bool>* solution);
129 IntegerVariable objective_var,
130 const std::function<
void()>& feasible_solution_observer, Model*
model);
135 IntegerVariable objective_var,
136 const std::function<
void()>& feasible_solution_observer, Model*
model);
149 const std::vector<IntegerVariable>& variables,
151 std::function<
void()> feasible_solution_observer,
163 struct ObjectiveTerm {
167 IntegerValue old_var_lb;
171 IntegerValue cover_ub;
177 bool ProcessSolution();
181 bool PropagateObjectiveBounds();
185 bool CoverOptimization();
189 void ComputeNextStratificationThreshold();
191 SatParameters* parameters_;
198 IntegerVariable objective_var_;
199 std::vector<ObjectiveTerm> terms_;
200 IntegerValue stratification_threshold_;
201 std::function<void()> feasible_solution_observer_;
205 bool already_switched_to_linear_scan_ =
false;
231 const std::function<
void()>& feasible_solution_observer,
Model*
model);
A simple class to enforce both an elapsed time limit and a deterministic time limit in the same threa...
CoreBasedOptimizer(IntegerVariable objective_var, const std::vector< IntegerVariable > &variables, const std::vector< IntegerValue > &coefficients, std::function< void()> feasible_solution_observer, Model *model)
SatSolver::Status Optimize()
Class that owns everything related to a particular optimization model.
void RestrictObjectiveDomainWithBinarySearch(IntegerVariable objective_var, const std::function< void()> &feasible_solution_observer, Model *model)
SatSolver::Status SolveWithCardinalityEncodingAndCore(LogBehavior log, const LinearBooleanProblem &problem, SatSolver *solver, std::vector< bool > *solution)
SatSolver::Status SolveWithLinearScan(LogBehavior log, const LinearBooleanProblem &problem, SatSolver *solver, std::vector< bool > *solution)
SatSolver::Status MinimizeWithHittingSetAndLazyEncoding(const ObjectiveDefinition &objective_definition, const std::function< void()> &feasible_solution_observer, Model *model)
SatSolver::Status SolveWithWPM1(LogBehavior log, const LinearBooleanProblem &problem, SatSolver *solver, std::vector< bool > *solution)
void MinimizeCoreWithPropagation(TimeLimit *limit, SatSolver *solver, std::vector< Literal > *core)
SatSolver::Status SolveWithFuMalik(LogBehavior log, const LinearBooleanProblem &problem, SatSolver *solver, std::vector< bool > *solution)
SatSolver::Status SolveWithRandomParameters(LogBehavior log, const LinearBooleanProblem &problem, int num_times, SatSolver *solver, std::vector< bool > *solution)
SatSolver::Status SolveWithCardinalityEncoding(LogBehavior log, const LinearBooleanProblem &problem, SatSolver *solver, std::vector< bool > *solution)
SatSolver::Status MinimizeIntegerVariableWithLinearScanAndLazyEncoding(IntegerVariable objective_var, const std::function< void()> &feasible_solution_observer, Model *model)
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...
std::vector< double > coefficients