14 #ifndef OR_TOOLS_SAT_SAT_DECISION_H_
15 #define OR_TOOLS_SAT_SAT_DECISION_H_
70 void Untrail(
int target_trail_index);
86 maybe_enable_phase_saving_ = save_phase;
107 void InitializeVariableOrdering();
110 void RescaleVariableActivities(
double scaling_factor);
114 void ResetInitialPolarity(
int from,
bool inverted =
false);
118 void RephaseIfNeeded();
119 void UseLongestAssignmentAsInitialPolarity();
120 void FlipCurrentPolarity();
121 void RandomizeCurrentPolarity();
125 void PqInsertOrUpdate(BooleanVariable
var);
128 const SatParameters& parameters_;
138 struct WeightedVarQueueElement {
140 int Index()
const {
return var.value(); }
157 bool operator<(
const WeightedVarQueueElement& other)
const {
158 return weight < other.weight ||
159 (
weight == other.weight && (tie_breaker < other.tie_breaker));
170 static_assert(
sizeof(WeightedVarQueueElement) == 16,
171 "ERROR_WeightedVarQueueElement_is_not_well_compacted");
173 bool var_ordering_is_initialized_ =
false;
174 IntegerPriorityQueue<WeightedVarQueueElement> var_ordering_;
183 struct NumConflictsStackEntry {
187 int64 num_conflicts_ = 0;
188 std::vector<NumConflictsStackEntry> num_conflicts_stack_;
196 BitQueue64 pq_need_update_for_var_at_trail_index_;
199 double variable_activity_increment_ = 1.0;
212 bool in_stable_phase_ =
false;
213 int target_length_ = 0;
221 bool maybe_enable_phase_saving_ =
true;
222 int64 polarity_phase_ = 0;
223 int64 num_conflicts_until_rephase_ = 1000;
226 std::vector<Literal> best_partial_assignment_;
235 #endif // OR_TOOLS_SAT_SAT_DECISION_H_