14 #ifndef OR_TOOLS_SAT_PROBING_H_
15 #define OR_TOOLS_SAT_PROBING_H_
17 #include "absl/types/span.h"
66 bool log_info =
false);
71 absl::Span<const BooleanVariable> bool_vars,
72 bool log_info =
false);
77 bool ProbeOneVariableInternal(BooleanVariable
b);
94 std::vector<Literal> to_fix_at_true_;
95 std::vector<IntegerLiteral> new_integer_bounds_;
96 std::vector<std::pair<Literal, Literal>> new_binary_clauses_;
99 int num_new_holes_ = 0;
100 int num_new_binary_ = 0;
101 int num_new_integer_bounds_ = 0;
115 bool log_info =
false);
A simple class to enforce both an elapsed time limit and a deterministic time limit in the same threa...
Class that owns everything related to a particular optimization model.
bool ProbeOneVariable(BooleanVariable b)
bool ProbeBooleanVariables(double deterministic_time_limit, bool log_info=false)
bool LookForTrivialSatSolution(double deterministic_time_limit, Model *model, bool log_info)
bool FailedLiteralProbingRound(ProbingOptions options, Model *model)
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...
std::string ToString() const
double deterministic_limit
bool subsume_with_binary_clause
bool extract_binary_clauses