320 : parameters_(*model->GetOrCreate<SatParameters>()),
325 trail_(model->GetOrCreate<
Trail>()),
326 time_limit_(model->GetOrCreate<
TimeLimit>()) {}
331 int NumClausesContaining(
Literal l);
332 void UpdatePriorityQueue(BooleanVariable var);
333 bool CrossProduct(BooleanVariable var);
334 void DeleteClause(
SatClause* sat_clause);
335 void DeleteAllClausesContaining(
Literal literal);
336 void AddClause(absl::Span<const Literal> clause);
345 template <
bool score_only,
bool with_binary_only>
346 bool ResolveAllClauseContaining(
Literal lit);
348 const SatParameters& parameters_;
356 int propagation_index_;
359 int64_t num_inspected_literals_ = 0;
360 int64_t num_simplifications_ = 0;
361 int64_t num_blocked_clauses_ = 0;
362 int64_t num_eliminated_variables_ = 0;
363 int64_t num_literals_diff_ = 0;
364 int64_t num_clauses_diff_ = 0;
367 int64_t score_threshold_;
371 std::vector<Literal> resolvant_;
375 struct VariableWithPriority {
380 int Index()
const {
return var.value(); }
381 bool operator<(
const VariableWithPriority& o)
const {
382 return priority < o.priority;
385 IntegerPriorityQueue<VariableWithPriority> queue_;
388 util_intops::StrongVector<BooleanVariable, bool> in_need_to_be_updated_;
389 std::vector<BooleanVariable> need_to_be_updated_;
395 util_intops::StrongVector<ClauseIndex, SatClause*> clauses_;
396 util_intops::StrongVector<LiteralIndex, std::vector<ClauseIndex>>
398 util_intops::StrongVector<LiteralIndex, int> literal_to_num_clauses_;
std::deque< std::vector< Literal > > clauses
void AddClauseWithSpecialLiteral(Literal literal, absl::Span< const Literal > clause)