21#ifndef OR_TOOLS_SAT_SAT_INPROCESSING_H_
22#define OR_TOOLS_SAT_SAT_INPROCESSING_H_
45 absl::Span<const Literal> clause);
98 blocked_clause_simplifier_(
100 bounded_variable_elimination_(
146 double total_dtime_ = 0.0;
155 int64 last_num_redundant_literals_ = 0;
156 int64 last_num_fixed_variables_ = 0;
199 return first_stamps_[
a.Index()] < first_stamps_[
b.Index()] &&
200 last_stamps_[
b.Index()] < last_stamps_[
a.Index()];
213 bool stamps_are_already_computed_ =
false;
217 int64 num_subsumed_clauses_ = 0;
218 int64 num_removed_literals_ = 0;
219 int64 num_fixed_ = 0;
227 std::vector<LiteralIndex> children_;
231 std::vector<LiteralIndex> dfs_stack_;
261 void InitializeForNewRound();
262 void ProcessLiteral(
Literal current_literal);
263 bool ClauseIsBlocked(
Literal current_literal,
264 absl::Span<const Literal> clause);
273 int32 num_blocked_clauses_ = 0;
274 int64 num_inspected_literals_ = 0;
282 std::deque<Literal> queue_;
286 DEFINE_INT_TYPE(ClauseIndex,
int32);
295 : parameters_(*
model->GetOrCreate<SatParameters>()),
306 int NumClausesContaining(
Literal l);
307 void UpdatePriorityQueue(BooleanVariable
var);
308 bool CrossProduct(BooleanVariable
var);
309 void DeleteClause(
SatClause* sat_clause);
311 void AddClause(absl::Span<const Literal> clause);
320 template <
bool score_only,
bool with_binary_only>
321 bool ResolveAllClauseContaining(
Literal lit);
323 const SatParameters& parameters_;
331 int propagation_index_;
334 int64 num_inspected_literals_ = 0;
335 int64 num_simplifications_ = 0;
336 int64 num_blocked_clauses_ = 0;
337 int64 num_eliminated_variables_ = 0;
338 int64 num_literals_diff_ = 0;
339 int64 num_clauses_diff_ = 0;
342 int64 score_threshold_;
346 std::vector<Literal> resolvant_;
350 struct VariableWithPriority {
355 int Index()
const {
return var.value(); }
356 bool operator<(
const VariableWithPriority& o)
const {
357 return priority < o.priority;
360 IntegerPriorityQueue<VariableWithPriority> queue_;
364 std::vector<BooleanVariable> need_to_be_updated_;
369 DEFINE_INT_TYPE(ClauseIndex,
int32);
An Assignment is a variable -> domains mapping, used to report solutions to the user.
A simple class to enforce both an elapsed time limit and a deterministic time limit in the same threa...
BlockedClauseSimplifier(Model *model)
void DoOneRound(bool log_info)
bool DoOneRound(bool log_info)
BoundedVariableElimination(Model *model)
bool PresolveLoop(SatPresolveOptions options)
bool MoreFixedVariableToClean() const
bool RemoveFixedAndEquivalentVariables(bool log_info)
bool LevelZeroPropagate()
Inprocessing(Model *model)
bool MoreRedundantVariableToClean() const
bool SubsumeAndStrenghtenRound(bool log_info)
bool DetectEquivalencesAndStamp(bool use_transitive_reduction, bool log_info)
Class that owns everything related to a particular optimization model.
bool DoOneRound(bool log_info)
bool ComputeStampsForNextRound(bool log_info)
bool ImplicationIsInTree(Literal a, Literal b) const
StampingSimplifier(Model *model)
void SampleTreeAndFillParent()
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...
std::deque< std::vector< Literal > > clauses
void AddClauseWithSpecialLiteral(Literal literal, absl::Span< const Literal > clause)
bool use_transitive_reduction
bool extract_binary_clauses_in_probing
double deterministic_time_limit