C++ Reference: optimization

This documentation is automatically generated.

Optimization algorithms to solve a LinearBooleanProblem by using the SAT solver as a black-box.

TODO(user): Currently, only the MINIMIZATION problem type is supported.

Function Type Arguments Comments
MinimizeCore

Return type: void

Arguments: SatSolver* solver, std::vector<Literal>* core

MinimizeCoreWithPropagation

Return type: void

Arguments: SatSolver* solver, std::vector<Literal>* core

MinimizeIntegerVariableWithLinearScan

Return type: SatSolver::Status

Arguments: IntegerVariable objective_var, const std::function<void(const Model&)>& feasible_solution_observer, Model* model

MinimizeIntegerVariableWithLinearScanAndLazyEncoding

Return type: SatSolver::Status

Arguments: bool log_info, IntegerVariable objective_var, const std::function<LiteralIndex()>& next_decision, const std::function<void(const Model&)>& feasible_solution_observer, Model* model

MinimizeWithCoreAndLazyEncoding

Return type: SatSolver::Status

Arguments: bool log_info, IntegerVariable objective_var, const std::vector<IntegerVariable>& variables, const std::vector<IntegerValue>& coefficients, const std::function<LiteralIndex()>& next_decision, const std::function<void(const Model&)>& feasible_solution_observer, Model* model

MinimizeWithHittingSetAndLazyEncoding

Return type: SatSolver::Status

Arguments: bool log_info, IntegerVariable objective_var, std::vector<IntegerVariable> variables, std::vector<IntegerValue> coefficients, const std::function<LiteralIndex()>& next_decision, const std::function<void(const Model&)>& feasible_solution_observer, Model* model

RestrictObjectiveDomainWithBinarySearch

Return type: void

Arguments: IntegerVariable objective_var, const std::function<LiteralIndex()>& next_decision, const std::function<void(const Model&)>& feasible_solution_observer, Model* model

SolveWithCardinalityEncoding

Return type: SatSolver::Status

Arguments: LogBehavior log, const LinearBooleanProblem& problem, SatSolver* solver, std::vector<bool>* solution

SolveWithCardinalityEncodingAndCore

Return type: SatSolver::Status

Arguments: LogBehavior log, const LinearBooleanProblem& problem, SatSolver* solver, std::vector<bool>* solution

SolveWithFuMalik

Return type: SatSolver::Status

Arguments: LogBehavior log, const LinearBooleanProblem& problem, SatSolver* solver, std::vector<bool>* solution

SolveWithLinearScan

Return type: SatSolver::Status

Arguments: LogBehavior log, const LinearBooleanProblem& problem, SatSolver* solver, std::vector<bool>* solution

SolveWithRandomParameters

Return type: SatSolver::Status

Arguments: LogBehavior log, const LinearBooleanProblem& problem, int num_times, SatSolver* solver, std::vector<bool>* solution

SolveWithWPM1

Return type: SatSolver::Status

Arguments: LogBehavior log, const LinearBooleanProblem& problem, SatSolver* solver, std::vector<bool>* solution

Send feedback about...