14#ifndef OR_TOOLS_SAT_UTIL_H_
15#define OR_TOOLS_SAT_UTIL_H_
30#include "absl/base/attributes.h"
31#include "absl/container/btree_set.h"
32#include "absl/log/check.h"
33#include "absl/log/log_streamer.h"
34#include "absl/numeric/int128.h"
35#include "absl/random/bit_gen_ref.h"
36#include "absl/random/random.h"
37#include "absl/strings/str_cat.h"
38#include "absl/strings/string_view.h"
39#include "absl/types/span.h"
43#include "ortools/sat/sat_parameters.pb.h"
68template <
typename K =
int,
typename V =
int>
90 starts_.reserve(
size);
104 template <
typename Keys,
typename Values>
106 int minimum_num_nodes = 0);
111 template <
typename Collection>
123 int min_transpose_size = 0);
127 int Add(absl::Span<const V> values);
132 template <
typename L>
143 DCHECK_LT(index, sizes_[key]);
144 const int start = starts_[key];
145 std::swap(buffer_[start + index], buffer_[start + sizes_[key] - 1]);
161 static int InternalKey(K key);
163 std::vector<int> starts_;
164 std::vector<int> sizes_;
165 std::vector<V> buffer_;
178 data_.reset(
new T[
size]);
181 T*
data()
const {
return data_.get(); }
182 T*
begin()
const {
return data_.get(); }
183 T*
end()
const {
return data_.get() + size_; }
184 size_t size()
const {
return size_; }
185 bool empty()
const {
return size_ == 0; }
190 T
back()
const {
return data_[size_ - 1]; }
191 T&
back() {
return data_[size_ - 1]; }
200 std::unique_ptr<T[]> data_ =
nullptr;
208 return absl::StrCat(
"'", name,
"':");
214std::string
FormatTable(std::vector<std::vector<std::string>>& table,
260 int64_t& x0, int64_t& y0);
292 const std::vector<std::vector<int>>& graph, absl::BitGenRef random,
293 std::vector<int>* buffer);
308 int64_t
base, absl::Span<const int64_t> coeffs,
309 absl::Span<const int64_t> lbs, absl::Span<const int64_t> ubs, int64_t rhs,
325 :
absl::BitGenRef(deterministic_random_) {
326 deterministic_random_.seed(params.random_seed());
327 if (params.use_absl_random()) {
328 absl_random_ = absl::BitGen(absl::SeedSeq({params.random_seed()}));
329 absl::BitGenRef::operator=(absl::BitGenRef(absl_random_));
334 :
absl::BitGenRef(deterministic_random_) {
335 absl::BitGenRef::operator=(bit_gen_ref);
350 absl::BitGen absl_random_;
361void RandomizeDecisionHeuristic(absl::BitGenRef random,
362 SatParameters* parameters);
368int WeightedPick(absl::Span<const double>
input, absl::BitGenRef random);
390int MoveOneUnprocessedLiteralLast(
391 const absl::btree_set<LiteralIndex>& processed,
int relevant_prefix_size,
392 std::vector<Literal>* literals);
403 : max_complexity_per_add_(max_complexity_per_add) {
409 void Reset(int64_t bound);
412 int64_t MaxIfAdded(int64_t candidate)
const;
415 void Add(int64_t value);
420 void AddChoices(absl::Span<const int64_t> choices);
423 void AddMultiples(int64_t coeff, int64_t max_value);
429 int64_t
Bound()
const {
return bound_; }
433 void AddChoicesInternal(absl::Span<const int64_t> values);
436 const int max_complexity_per_add_;
439 int64_t current_max_;
440 std::vector<int64_t> sums_;
441 std::vector<bool> expanded_sums_;
442 std::vector<int64_t> filtered_values_;
455 : reachable_(new int64_t[n]), new_reachable_(new int64_t[n]) {
460 for (
int i = 0;
i < n; ++
i) {
461 reachable_[
i] = std::numeric_limits<int64_t>::max();
464 new_reachable_[0] = 0;
470 void Add(
const int64_t positive_value) {
471 DCHECK_GT(positive_value, 0);
472 const int64_t*
reachable = reachable_.get();
473 if (positive_value >=
reachable[n - 1])
return;
479 int64_t* new_reachable = new_reachable_.get();
481 const int64_t candidate =
CapAdd(new_reachable[
base], positive_value);
482 while (j < n &&
i < n &&
reachable[
i] < candidate) {
490 new_reachable[j++] = candidate;
493 std::swap(reachable_, new_reachable_);
499 if (sum >= reachable_[n - 1])
return true;
500 return std::binary_search(&reachable_[0], &reachable_[0] + n, sum);
506 return absl::MakeSpan(reachable_.get(), n);
510 std::unique_ptr<int64_t[]> reachable_;
511 std::unique_ptr<int64_t[]> new_reachable_;
529 absl::Span<const int64_t>
Compute(absl::Span<const int64_t> elements,
531 bool abort_if_maximum_reached =
false);
534 absl::Span<const int64_t>
SortedSums()
const {
return sums_; }
537 std::vector<int64_t> sums_;
538 std::vector<int64_t> new_sums_;
550 int64_t
MaxSubsetSum(absl::Span<const int64_t> elements, int64_t bin_size);
584 absl::Span<const int64_t> coeffs,
585 absl::Span<const int64_t> costs,
const Domain& rhs);
588 Result InternalSolve(int64_t num_values,
const Domain& rhs);
591 std::vector<Domain> domains_;
592 std::vector<int64_t> coeffs_;
593 std::vector<int64_t> costs_;
597 int64_t cost = std::numeric_limits<int64_t>::max();
600 std::vector<std::vector<State>> var_activity_states_;
608 : average_(initial_average) {}
612 void Reset(
double reset_value);
617 void AddData(
double new_record);
620 double average_ = 0.0;
621 int64_t num_records_ = 0;
631 : decaying_factor_(decaying_factor) {
632 DCHECK_GE(decaying_factor, 0.0);
633 DCHECK_LE(decaying_factor, 1.0);
642 void AddData(
double new_record);
645 double average_ = 0.0;
646 int64_t num_records_ = 0;
647 const double decaying_factor_;
660 explicit Percentile(
int record_limit) : record_limit_(record_limit) {}
662 void AddRecord(
double record);
668 double GetPercentile(
double percent);
671 std::deque<double> records_;
672 const int record_limit_;
680template <
typename Element,
typename Score>
683 explicit TopN(
int n) : n_(n) {}
690 void Add(Element e, Score score) {
691 if (heap_.size() < n_) {
692 const int index = elements_.size();
693 heap_.push_back({index, score});
694 elements_.push_back(std::move(e));
695 if (heap_.size() == n_) {
697 std::make_heap(heap_.begin(), heap_.end());
700 if (score <= heap_.front().score)
return;
701 const int index_to_replace = heap_.front().index;
702 elements_[index_to_replace] = std::move(e);
705 std::pop_heap(heap_.begin(), heap_.end());
706 heap_.back() = {index_to_replace, score};
707 std::push_heap(heap_.begin(), heap_.end());
711 bool empty()
const {
return elements_.empty(); }
723 bool operator<(
const HeapElement& other)
const {
724 return score > other.score;
727 std::vector<HeapElement> heap_;
728 std::vector<Element> elements_;
736 if (std::isnan(value))
return 0;
737 if (value >=
static_cast<double>(std::numeric_limits<int64_t>::max())) {
738 return std::numeric_limits<int64_t>::max();
740 if (value <=
static_cast<double>(std::numeric_limits<int64_t>::min())) {
741 return std::numeric_limits<int64_t>::min();
743 return static_cast<int64_t
>(value);
748 return x <= absl::int128(std::numeric_limits<int64_t>::max()) &&
749 x > absl::int128(std::numeric_limits<int64_t>::min());
752template <
typename K,
typename V>
753inline int CompactVectorVector<K, V>::Add(absl::Span<const V> values) {
754 const int index = size();
755 starts_.push_back(buffer_.size());
756 sizes_.push_back(values.size());
757 buffer_.insert(buffer_.end(), values.begin(), values.end());
761template <
typename K,
typename V>
764 buffer_.push_back(value);
767template <
typename K,
typename V>
769 K key, absl::Span<const V> values) {
770 CHECK_LE(values.size(), sizes_[key]);
771 sizes_[key] = values.size();
772 if (values.empty())
return;
773 memcpy(&buffer_[starts_[key]], values.data(),
sizeof(V) * values.size());
776template <
typename K,
typename V>
779 const std::vector<L>& wrapped_values) {
781 starts_.push_back(buffer_.size());
782 sizes_.push_back(wrapped_values.size());
783 for (
const L wrapped_value : wrapped_values) {
784 buffer_.push_back(wrapped_value.Index().value());
790template <
typename K,
typename V>
791inline int CompactVectorVector<K, V>::InternalKey(K key) {
792 if constexpr (std::is_same_v<K, int>) {
799template <
typename K,
typename V>
800inline absl::Span<const V> CompactVectorVector<K, V>::operator[](K key)
const {
802 DCHECK_LT(key, starts_.size());
803 DCHECK_LT(key, sizes_.size());
804 const int k = InternalKey(key);
805 const size_t size =
static_cast<size_t>(sizes_.data()[k]);
806 if (
size == 0)
return {};
807 return {&buffer_.data()[starts_.data()[k]], size};
810template <
typename K,
typename V>
811inline absl::Span<V> CompactVectorVector<K, V>::operator[](K key) {
813 DCHECK_LT(key, starts_.size());
814 DCHECK_LT(key, sizes_.size());
815 const int k = InternalKey(key);
816 const size_t size =
static_cast<size_t>(sizes_.data()[k]);
817 if (
size == 0)
return {};
818 return absl::MakeSpan(&buffer_.data()[starts_.data()[k]], size);
821template <
typename K,
typename V>
822inline std::vector<absl::Span<const V>>
823CompactVectorVector<K, V>::AsVectorOfSpan()
const {
824 std::vector<absl::Span<const V>> result(starts_.size());
825 for (
int k = 0; k < starts_.size(); ++k) {
826 result[k] = (*this)[k];
831template <
typename K,
typename V>
832inline void CompactVectorVector<K, V>::clear() {
838template <
typename K,
typename V>
840 return starts_.size();
843template <
typename K,
typename V>
845 return starts_.empty();
848template <
typename K,
typename V>
849template <
typename Keys,
typename Values>
851 Keys keys, Values values,
int minimum_num_nodes) {
853 int max_key = minimum_num_nodes;
854 for (
const K key : keys) {
855 max_key = std::max(max_key, InternalKey(key) + 1);
860 sizes_.assign(minimum_num_nodes, 0);
861 starts_.assign(minimum_num_nodes, 0);
866 sizes_.assign(max_key, 0);
867 for (
const K key : keys) {
868 sizes_[InternalKey(key)]++;
872 starts_.assign(max_key, 0);
873 for (
int k = 1; k < max_key; ++k) {
874 starts_[k] = starts_[k - 1] + sizes_[k - 1];
878 buffer_.resize(keys.size());
879 for (
int i = 0;
i < keys.size(); ++
i) {
880 buffer_[starts_[InternalKey(keys[i])]++] = values[
i];
884 for (
int k = max_key - 1; k > 0; --k) {
885 starts_[k] = starts_[k - 1];
891template <
typename K,
typename V>
892template <
typename Collection>
893inline void CompactVectorVector<K, V>::ResetFromPairs(
const Collection& pairs,
894 int minimum_num_nodes) {
896 int max_key = minimum_num_nodes;
897 for (
const auto& [key, _] : pairs) {
898 max_key = std::max(max_key, InternalKey(key) + 1);
903 sizes_.assign(minimum_num_nodes, 0);
904 starts_.assign(minimum_num_nodes, 0);
909 sizes_.assign(max_key, 0);
910 for (
const auto& [key, _] : pairs) {
911 sizes_[InternalKey(key)]++;
915 starts_.assign(max_key, 0);
916 for (
int k = 1; k < max_key; ++k) {
917 starts_[k] = starts_[k - 1] + sizes_[k - 1];
921 buffer_.resize(pairs.size());
922 for (
int i = 0;
i < pairs.size(); ++
i) {
923 const auto& [key, value] = pairs[
i];
924 buffer_[starts_[InternalKey(key)]++] = value;
928 for (
int k = max_key - 1; k > 0; --k) {
929 starts_[k] = starts_[k - 1];
935template <
typename K,
typename V>
936inline void CompactVectorVector<K, V>::ResetFromTranspose(
937 const CompactVectorVector<V, K>& other,
int min_transpose_size) {
940 if (min_transpose_size > 0) {
941 starts_.assign(min_transpose_size, 0);
942 sizes_.assign(min_transpose_size, 0);
948 int max_key = min_transpose_size;
949 for (V v = 0; v < other.size(); ++v) {
950 for (
const K k : other[v]) {
951 max_key = std::max(max_key, InternalKey(k) + 1);
956 sizes_.assign(max_key, 0);
957 for (V v = 0; v < other.size(); ++v) {
958 for (
const K k : other[v]) {
959 sizes_[InternalKey(k)]++;
964 starts_.assign(max_key, 0);
965 for (
int k = 1; k < max_key; ++k) {
966 starts_[k] = starts_[k - 1] + sizes_[k - 1];
970 buffer_.resize(other.buffer_.size());
971 for (V v = 0; v < other.size(); ++v) {
972 for (
const K k : other[v]) {
973 buffer_[starts_[InternalKey(k)]++] = v;
978 for (
int k = max_key - 1; k > 0; --k) {
979 starts_[k] = starts_[k - 1];
1009class DagTopologicalSortIterator {
1015 : graph_(size,
std::vector<int>{}) {}
1050 friend bool operator==(
const Iterator& a,
const Iterator&
b) {
1051 return &a.graph_ == &
b.graph_ && a.ordering_index_ ==
b.ordering_index_;
1058 reference
operator*()
const {
return permutation_; }
1064 explicit Iterator(
const std::vector<std::vector<int>>& graph
1065 ABSL_ATTRIBUTE_LIFETIME_BOUND,
1067 : graph_(graph), ordering_index_(-1) {}
1070 explicit Iterator(
const std::vector<std::vector<int>>& graph
1071 ABSL_ATTRIBUTE_LIFETIME_BOUND);
1074 void Unset(
int pos);
1077 void Set(
int pos,
int k);
1080 const std::vector<std::vector<int>>& graph_;
1085 std::vector<int> missing_parent_numbers_;
1088 std::vector<int> permutation_;
1091 std::vector<int> element_original_position_;
1095 int64_t ordering_index_;
1098 Iterator
begin() const ABSL_ATTRIBUTE_LIFETIME_BOUND {
1099 return Iterator(graph_);
1101 Iterator
end() const ABSL_ATTRIBUTE_LIFETIME_BOUND {
1102 return Iterator(graph_,
true);
1105 void Reset(
int size) { graph_.assign(size, {}); }
1110 DCHECK_LT(from, graph_.size());
1112 DCHECK_LT(
to, graph_.size());
1113 graph_[from].push_back(
to);
1118 std::vector<std::vector<int>> graph_;
1140inline DagTopologicalSortIterator::Iterator&
1141DagTopologicalSortIterator::Iterator::operator++() {
1142 CHECK_GE(ordering_index_, 0) <<
"Iteration past end";
1146 ordering_index_ = -1;
1151 for (
int pos = size_ - 2; pos >= 0; --pos) {
1161 const int k = element_original_position_[pos] + 1;
1167 if (k == permutation_.size())
continue;
1170 for (++pos; pos < size_; ++pos) {
1176 CHECK_LT(pos, permutation_.size())
1177 <<
"Unexpected cycle detected during iteration";
1188 ordering_index_ = -1;
1192inline DagTopologicalSortIterator::Iterator::Iterator(
1193 const std::vector<std::vector<int>>& graph)
1195 size_(graph.size()),
1196 missing_parent_numbers_(size_, 0),
1197 element_original_position_(size_, 0),
1198 ordering_index_(0) {
1205 for (
const auto& children : graph_) {
1206 for (
const int child : children) {
1207 missing_parent_numbers_[child]++;
1211 for (
int i = 0;
i < size_; ++
i) {
1212 if (missing_parent_numbers_[
i] == 0) {
1213 permutation_.push_back(
i);
1216 for (
int pos = 0; pos < size_; ++pos) {
1220 if (pos >= permutation_.size()) {
1221 ordering_index_ = -1;
1237inline void DagTopologicalSortIterator::Iterator::Unset(
int pos) {
1238 const int n = permutation_[pos];
1241 for (
const int c : graph_[n]) {
1242 if (missing_parent_numbers_[c] == 0) permutation_.pop_back();
1243 ++missing_parent_numbers_[
c];
1245 std::swap(permutation_[element_original_position_[pos]], permutation_[pos]);
1247 element_original_position_[pos] = pos;
1256inline void DagTopologicalSortIterator::Iterator::Set(
int pos,
int k) {
1257 int n = permutation_[k];
1260 for (
int c : graph_[n]) {
1261 --missing_parent_numbers_[
c];
1262 if (missing_parent_numbers_[c] == 0) permutation_.push_back(c);
1265 std::swap(permutation_[k], permutation_[pos]);
1267 element_original_position_[pos] = k;
SharedTimeLimit(TimeLimit *time_limit)
Result Solve(absl::Span< const Domain > domains, absl::Span< const int64_t > coeffs, absl::Span< const int64_t > costs, const Domain &rhs)
void ResetFromTranspose(const CompactVectorVector< V, K > &other, int min_transpose_size=0)
Similar to ResetFromFlatMapping().
void ResetFromPairs(const Collection &pairs, int minimum_num_nodes=0)
Similar to ResetFromFlatMapping().
void ResetFromFlatMapping(Keys keys, Values values, int minimum_num_nodes=0)
void reserve(int size, int num_entries)
void clear()
Restore to empty vector<vector<>>.
absl::Span< V > operator[](K key)
void emplace_back(V const *begin, V const *end)
size_t num_entries() const
void ReplaceValuesBySmallerSet(K key, absl::Span< const V > values)
std::vector< absl::Span< const V > > AsVectorOfSpan() const
void RemoveBySwap(K key, int index)
int AddLiterals(const std::vector< L > &wrapped_values)
size_t size() const
Size of the "key" space, always in [0, size()).
void reserve(int size)
Reserve memory if it is already known or tightly estimated.
void AppendToLastVector(const V &value)
int Add(absl::Span< const V > values)
const std::vector< int > value_type
ptrdiff_t difference_type
std::input_iterator_tag iterator_category
pointer operator->() const
friend bool operator==(const Iterator &a, const Iterator &b)
DagTopologicalSortIterator()=default
void AddArc(int from, int to)
Must be called before iteration starts or between iterations.
double CurrentAverage() const
Returns exponential moving average for all the added data so far.
int64_t NumRecords() const
Returns the total number of added records so far.
ExponentialMovingAverage(double decaying_factor)
int64_t LastValue() const
absl::Span< const int64_t > reachable()
bool MightBeReachable(int64_t sum) const
void Add(const int64_t positive_value)
void ClearAndReserve(size_t size)
T operator[](int i) const
void Reset(double reset_value)
Sets the number of records to 0 and average to 'reset_value'.
IncrementalAverage()=default
int64_t NumRecords() const
IncrementalAverage(double initial_average)
Initializes the average with 'initial_average' and number of records to 0.
double CurrentAverage() const
Similar to MaxBoundedSubsetSum() above but use a different algo.
double ComplexityEstimate(int num_elements, int64_t bin_size)
int64_t MaxSubsetSum(absl::Span< const int64_t > elements, int64_t bin_size)
int64_t CurrentMax() const
void Reset(int64_t bound)
MaxBoundedSubsetSum(int64_t bound, int max_complexity_per_add=50)
ModelRandomGenerator(const absl::BitGenRef &bit_gen_ref)
ModelRandomGenerator(const SatParameters ¶ms)
ModelRandomGenerator(Model *model)
ModelSharedTimeLimit(Model *model)
int64_t NumRecords() const
Returns number of stored records.
Percentile(int record_limit)
Yet another variant of FirstFewValues or MaxBoundedSubsetSum.
absl::Span< const int64_t > Compute(absl::Span< const int64_t > elements, int64_t maximum_sum, bool abort_if_maximum_reached=false)
absl::Span< const int64_t > SortedSums() const
Returns the possible subset sums sorted.
void Add(Element e, Score score)
std::vector< Element > * MutableUnorderedElements()
const std::vector< Element > & UnorderedElements() const
int64_t ProductWithModularInverse(int64_t coeff, int64_t mod, int64_t rhs)
bool SolveDiophantineEquationOfSizeTwo(int64_t &a, int64_t &b, int64_t &cte, int64_t &x0, int64_t &y0)
int64_t FloorSquareRoot(int64_t a)
The argument must be non-negative.
int64_t CeilSquareRoot(int64_t a)
int64_t ModularInverse(int64_t x, int64_t m)
bool IsNegatableInt64(absl::int128 x)
Tells whether a int128 can be casted to a int64_t that can be negated.
int64_t SafeDoubleToInt64(double value)
std::string FormatCounter(int64_t num)
Prints a positive number with separators for easier reading (ex: 1'348'065).
bool DiophantineEquationOfSizeTwoHasSolutionInDomain(const Domain &x, int64_t a, const Domain &y, int64_t b, int64_t cte)
int64_t ClosestMultiple(int64_t value, int64_t base)
int64_t PositiveMod(int64_t x, int64_t m)
Just returns x % m but with a result always in [0, m).
bool LinearInequalityCanBeReducedWithClosestMultiple(int64_t base, absl::Span< const int64_t > coeffs, absl::Span< const int64_t > lbs, absl::Span< const int64_t > ubs, int64_t rhs, int64_t *new_rhs)
std::vector< absl::Span< int > > AtMostOneDecomposition(const std::vector< std::vector< int > > &graph, absl::BitGenRef random, std::vector< int > *buffer)
LinearExpr operator*(LinearExpr expr, int64_t factor)
std::string FormatName(absl::string_view name)
This is used to format our table first row entry.
std::string FormatTable(std::vector< std::vector< std::string > > &table, int spacing)
In SWIG mode, we don't want anything besides these top-level includes.
int64_t CapAdd(int64_t x, int64_t y)
std::mt19937_64 random_engine_t
ClosedInterval::Iterator end(ClosedInterval interval)
ClosedInterval::Iterator begin(ClosedInterval interval)
trees with all degrees equal to
static int input(yyscan_t yyscanner)
std::vector< int64_t > solution