14 #ifndef OR_TOOLS_SAT_ALL_DIFFERENT_H_
15 #define OR_TOOLS_SAT_ALL_DIFFERENT_H_
21 #include "absl/container/flat_hash_map.h"
35 const std::vector<IntegerVariable>& vars);
46 const std::vector<IntegerVariable>& vars);
59 const std::vector<IntegerVariable>& variables);
80 bool MakeAugmentingPath(
int start);
83 inline LiteralIndex VariableLiteralIndexOf(
int x,
int64 value);
84 inline bool VariableHasPossibleValue(
int x,
int64 value);
90 const int num_variables_;
91 const std::vector<IntegerVariable> variables_;
92 int64 min_all_values_;
93 int64 num_all_values_;
94 std::vector<int64> variable_min_value_;
95 std::vector<int64> variable_max_value_;
96 std::vector<std::vector<LiteralIndex>> variable_literal_index_;
102 std::vector<std::vector<int>> successor_;
103 std::vector<bool> value_visited_;
104 std::vector<bool> variable_visited_;
105 std::vector<int> value_to_variable_;
106 std::vector<int> variable_to_value_;
107 std::vector<int> prev_matching_;
108 std::vector<int> visiting_;
109 std::vector<int> variable_visited_from_;
127 std::vector<std::vector<int>> residual_graph_successors_;
128 std::vector<int> component_number_;
165 void FillHallReason(IntegerValue hall_lb, IntegerValue hall_ub);
170 bool PropagateLowerBounds();
171 bool PropagateLowerBoundsInternal(IntegerValue min_lb,
172 absl::Span<VarValue> vars);
189 int FindStartIndexAndCompressPath(
int index);
191 int GetIndex(IntegerValue
value)
const {
194 return (
value - base_).value();
197 IntegerValue GetValue(
int index)
const {
return base_ + IntegerValue(
index); }
199 bool PointIsPresent(
int index)
const {
206 std::vector<VarValue> vars_;
207 std::vector<VarValue> negated_vars_;
210 std::vector<IntegerValue> hall_starts_;
211 std::vector<IntegerValue> hall_ends_;
215 std::vector<int> indices_to_clear_;
216 std::vector<int> index_to_start_index_;
217 std::vector<int> index_to_end_index_;
218 std::vector<IntegerVariable> index_to_var_;
221 std::vector<IntegerLiteral> integer_reason_;
229 #endif // OR_TOOLS_SAT_ALL_DIFFERENT_H_