14 #ifndef OR_TOOLS_SAT_BOOLEAN_PROBLEM_H_
15 #define OR_TOOLS_SAT_BOOLEAN_PROBLEM_H_
21 #include "absl/status/status.h"
24 #include "ortools/sat/boolean_problem.pb.h"
25 #include "ortools/sat/cp_model.pb.h"
40 const LinearBooleanProblem& problem, Coefficient v) {
41 return (
static_cast<double>(v.value()) + problem.objective().offset()) *
42 problem.objective().scaling_factor();
55 const SatSolver& solver, std::vector<bool>* assignment);
78 Coefficient upper_bound, SatSolver* solver);
83 bool use_lower_bound, Coefficient lower_bound,
84 bool use_upper_bound, Coefficient upper_bound,
89 const std::vector<bool>& assignment);
93 const std::vector<bool>& assignment);
99 const LinearBooleanProblem& problem);
105 BooleanAssignment* output);
109 const std::vector<int>& constraint_indices,
110 LinearBooleanProblem* subproblem);
121 const LinearBooleanProblem& problem,
122 std::vector<std::unique_ptr<SparsePermutation>>* generators);
133 LinearBooleanProblem* problem);
140 LinearBooleanProblem* problem);
bool AddObjectiveConstraint(const LinearBooleanProblem &problem, bool use_lower_bound, Coefficient lower_bound, bool use_upper_bound, Coefficient upper_bound, SatSolver *solver)
double AddOffsetAndScaleObjectiveValue(const LinearBooleanProblem &problem, Coefficient v)
void StoreAssignment(const VariablesAssignment &assignment, BooleanAssignment *output)
void UseObjectiveForSatAssignmentPreference(const LinearBooleanProblem &problem, SatSolver *solver)
void ExtractSubproblem(const LinearBooleanProblem &problem, const std::vector< int > &constraint_indices, LinearBooleanProblem *subproblem)
absl::Status ValidateBooleanProblem(const LinearBooleanProblem &problem)
bool AddObjectiveUpperBound(const LinearBooleanProblem &problem, Coefficient upper_bound, SatSolver *solver)
void FindLinearBooleanProblemSymmetries(const LinearBooleanProblem &problem, std::vector< std::unique_ptr< SparsePermutation >> *generators)
bool LoadAndConsumeBooleanProblem(LinearBooleanProblem *problem, SatSolver *solver)
void ApplyLiteralMappingToBooleanProblem(const absl::StrongVector< LiteralIndex, LiteralIndex > &mapping, LinearBooleanProblem *problem)
bool IsAssignmentValid(const LinearBooleanProblem &problem, const std::vector< bool > &assignment)
void ChangeOptimizationDirection(LinearBooleanProblem *problem)
void ProbeAndSimplifyProblem(SatPostsolver *postsolver, LinearBooleanProblem *problem)
Coefficient ComputeObjectiveValue(const LinearBooleanProblem &problem, const std::vector< bool > &assignment)
CpModelProto BooleanProblemToCpModelproto(const LinearBooleanProblem &problem)
void MakeAllLiteralsPositive(LinearBooleanProblem *problem)
bool LoadBooleanProblem(const LinearBooleanProblem &problem, SatSolver *solver)
std::string LinearBooleanProblemToCnfString(const LinearBooleanProblem &problem)
void ExtractAssignment(const LinearBooleanProblem &problem, const SatSolver &solver, std::vector< bool > *assignment)
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...