14 #ifndef OR_TOOLS_SAT_OPTIMIZATION_H_
15 #define OR_TOOLS_SAT_OPTIMIZATION_H_
65 const LinearBooleanProblem& problem,
67 std::vector<bool>* solution);
78 const LinearBooleanProblem& problem,
79 SatSolver* solver, std::vector<bool>* solution);
86 const LinearBooleanProblem& problem,
87 int num_times, SatSolver* solver,
88 std::vector<bool>* solution);
98 const LinearBooleanProblem& problem,
100 std::vector<bool>* solution);
106 LogBehavior log,
const LinearBooleanProblem& problem, SatSolver* solver,
107 std::vector<bool>* solution);
112 LogBehavior log,
const LinearBooleanProblem& problem, SatSolver* solver,
113 std::vector<bool>* solution);
126 IntegerVariable objective_var,
127 const std::function<
void()>& feasible_solution_observer, Model*
model);
132 IntegerVariable objective_var,
133 const std::function<
void()>& feasible_solution_observer, Model*
model);
146 const std::vector<IntegerVariable>& variables,
148 std::function<
void()> feasible_solution_observer,
160 struct ObjectiveTerm {
164 IntegerValue old_var_lb;
168 IntegerValue cover_ub;
174 bool ProcessSolution();
178 bool PropagateObjectiveBounds();
182 bool CoverOptimization();
186 void ComputeNextStratificationThreshold();
188 SatParameters* parameters_;
195 IntegerVariable objective_var_;
196 std::vector<ObjectiveTerm> terms_;
197 IntegerValue stratification_threshold_;
198 std::function<void()> feasible_solution_observer_;
202 bool already_switched_to_linear_scan_ =
false;
228 const std::function<
void()>& feasible_solution_observer,
Model*
model);
233 #endif // OR_TOOLS_SAT_OPTIMIZATION_H_