14#ifndef OR_TOOLS_SAT_UTIL_H_
15#define OR_TOOLS_SAT_UTIL_H_
29#include "absl/container/btree_set.h"
30#include "absl/log/check.h"
31#include "absl/log/log_streamer.h"
32#include "absl/numeric/int128.h"
33#include "absl/random/bit_gen_ref.h"
34#include "absl/random/random.h"
35#include "absl/strings/str_cat.h"
36#include "absl/strings/string_view.h"
37#include "absl/types/span.h"
41#include "ortools/sat/sat_parameters.pb.h"
66template <
typename K =
int,
typename V =
int>
88 starts_.reserve(
size);
102 template <
typename Keys,
typename Values>
108 template <
typename Collection>
120 int min_transpose_size = 0);
124 int Add(absl::Span<const V> values);
129 template <
typename L>
140 DCHECK_LT(index, sizes_[key]);
141 const int start = starts_[key];
142 std::swap(buffer_[start + index], buffer_[start + sizes_[key] - 1]);
153 Add(absl::MakeSpan(begin, end - begin));
158 static int InternalKey(K key);
160 std::vector<int> starts_;
161 std::vector<int> sizes_;
162 std::vector<V> buffer_;
175 data_.reset(
new T[
size]);
178 T*
data()
const {
return data_.get(); }
179 T*
begin()
const {
return data_.get(); }
180 T*
end()
const {
return data_.get() + size_; }
181 size_t size()
const {
return size_; }
182 bool empty()
const {
return size_ == 0; }
187 T
back()
const {
return data_[size_ - 1]; }
188 T&
back() {
return data_[size_ - 1]; }
197 std::unique_ptr<T[]> data_ =
nullptr;
205 return absl::StrCat(
"'", name,
"':");
211std::string
FormatTable(std::vector<std::vector<std::string>>& table,
257 int64_t& x0, int64_t& y0);
289 const std::vector<std::vector<int>>& graph, absl::BitGenRef random,
290 std::vector<int>* buffer);
305 int64_t
base, absl::Span<const int64_t> coeffs,
306 absl::Span<const int64_t> lbs, absl::Span<const int64_t> ubs, int64_t rhs,
322 :
absl::BitGenRef(deterministic_random_) {
323 deterministic_random_.seed(params.random_seed());
324 if (params.use_absl_random()) {
325 absl_random_ = absl::BitGen(absl::SeedSeq({params.random_seed()}));
326 absl::BitGenRef::operator=(absl::BitGenRef(absl_random_));
341 absl::BitGen absl_random_;
352void RandomizeDecisionHeuristic(absl::BitGenRef random,
353 SatParameters* parameters);
359int WeightedPick(absl::Span<const double>
input, absl::BitGenRef random);
381int MoveOneUnprocessedLiteralLast(
382 const absl::btree_set<LiteralIndex>& processed,
int relevant_prefix_size,
383 std::vector<Literal>* literals);
394 : max_complexity_per_add_(max_complexity_per_add) {
400 void Reset(int64_t bound);
403 int64_t MaxIfAdded(int64_t candidate)
const;
406 void Add(int64_t value);
411 void AddChoices(absl::Span<const int64_t> choices);
414 void AddMultiples(int64_t coeff, int64_t max_value);
420 int64_t
Bound()
const {
return bound_; }
424 void AddChoicesInternal(absl::Span<const int64_t> values);
427 const int max_complexity_per_add_;
430 int64_t current_max_;
431 std::vector<int64_t> sums_;
432 std::vector<bool> expanded_sums_;
433 std::vector<int64_t> filtered_values_;
446 : reachable_(new int64_t[n]), new_reachable_(new int64_t[n]) {
451 for (
int i = 0;
i < n; ++
i) {
452 reachable_[
i] = std::numeric_limits<int64_t>::max();
455 new_reachable_[0] = 0;
461 void Add(
const int64_t positive_value) {
462 DCHECK_GT(positive_value, 0);
463 const int64_t*
reachable = reachable_.get();
464 if (positive_value >=
reachable[n - 1])
return;
470 int64_t* new_reachable = new_reachable_.get();
472 const int64_t candidate =
CapAdd(new_reachable[
base], positive_value);
473 while (j < n &&
i < n &&
reachable[
i] < candidate) {
481 new_reachable[j++] = candidate;
484 std::swap(reachable_, new_reachable_);
490 if (sum >= reachable_[n - 1])
return true;
491 return std::binary_search(&reachable_[0], &reachable_[0] + n, sum);
497 return absl::MakeSpan(reachable_.get(), n);
501 std::unique_ptr<int64_t[]> reachable_;
502 std::unique_ptr<int64_t[]> new_reachable_;
520 absl::Span<const int64_t>
Compute(absl::Span<const int64_t> elements,
522 bool abort_if_maximum_reached =
false);
525 absl::Span<const int64_t>
SortedSums()
const {
return sums_; }
528 std::vector<int64_t> sums_;
529 std::vector<int64_t> new_sums_;
541 int64_t
MaxSubsetSum(absl::Span<const int64_t> elements, int64_t bin_size);
575 absl::Span<const int64_t> coeffs,
576 absl::Span<const int64_t> costs,
const Domain& rhs);
579 Result InternalSolve(int64_t num_values,
const Domain& rhs);
582 std::vector<Domain> domains_;
583 std::vector<int64_t> coeffs_;
584 std::vector<int64_t> costs_;
588 int64_t cost = std::numeric_limits<int64_t>::max();
591 std::vector<std::vector<State>> var_activity_states_;
599 : average_(initial_average) {}
603 void Reset(
double reset_value);
608 void AddData(
double new_record);
611 double average_ = 0.0;
612 int64_t num_records_ = 0;
622 : decaying_factor_(decaying_factor) {
623 DCHECK_GE(decaying_factor, 0.0);
624 DCHECK_LE(decaying_factor, 1.0);
633 void AddData(
double new_record);
636 double average_ = 0.0;
637 int64_t num_records_ = 0;
638 const double decaying_factor_;
651 explicit Percentile(
int record_limit) : record_limit_(record_limit) {}
653 void AddRecord(
double record);
659 double GetPercentile(
double percent);
662 std::deque<double> records_;
663 const int record_limit_;
671template <
typename Element,
typename Score>
674 explicit TopN(
int n) : n_(n) {}
681 void Add(Element e, Score score) {
682 if (heap_.size() < n_) {
683 const int index = elements_.size();
684 heap_.push_back({index, score});
685 elements_.push_back(std::move(e));
686 if (heap_.size() == n_) {
688 std::make_heap(heap_.begin(), heap_.end());
691 if (score <= heap_.front().score)
return;
692 const int index_to_replace = heap_.front().index;
693 elements_[index_to_replace] = std::move(e);
696 std::pop_heap(heap_.begin(), heap_.end());
697 heap_.back() = {index_to_replace, score};
698 std::push_heap(heap_.begin(), heap_.end());
702 bool empty()
const {
return elements_.empty(); }
714 bool operator<(
const HeapElement& other)
const {
715 return score > other.score;
718 std::vector<HeapElement> heap_;
719 std::vector<Element> elements_;
727 if (std::isnan(value))
return 0;
728 if (value >=
static_cast<double>(std::numeric_limits<int64_t>::max())) {
729 return std::numeric_limits<int64_t>::max();
731 if (value <=
static_cast<double>(std::numeric_limits<int64_t>::min())) {
732 return std::numeric_limits<int64_t>::min();
734 return static_cast<int64_t
>(value);
739 return x <= absl::int128(std::numeric_limits<int64_t>::max()) &&
740 x > absl::int128(std::numeric_limits<int64_t>::min());
743template <
typename K,
typename V>
744inline int CompactVectorVector<K, V>::Add(absl::Span<const V> values) {
745 const int index = size();
746 starts_.push_back(buffer_.size());
747 sizes_.push_back(values.size());
748 buffer_.insert(buffer_.end(), values.begin(), values.end());
752template <
typename K,
typename V>
755 buffer_.push_back(value);
758template <
typename K,
typename V>
760 K key, absl::Span<const V> values) {
761 CHECK_LE(values.size(), sizes_[key]);
762 sizes_[key] = values.size();
763 if (values.empty())
return;
764 memcpy(&buffer_[starts_[key]], values.data(),
sizeof(V) * values.size());
767template <
typename K,
typename V>
770 const std::vector<L>& wrapped_values) {
772 starts_.push_back(buffer_.size());
773 sizes_.push_back(wrapped_values.size());
774 for (
const L wrapped_value : wrapped_values) {
775 buffer_.push_back(wrapped_value.Index().value());
781template <
typename K,
typename V>
782inline int CompactVectorVector<K, V>::InternalKey(K key) {
783 if constexpr (std::is_same_v<K, int>) {
790template <
typename K,
typename V>
791inline absl::Span<const V> CompactVectorVector<K, V>::operator[](K key)
const {
793 DCHECK_LT(key, starts_.size());
794 DCHECK_LT(key, sizes_.size());
795 const int k = InternalKey(key);
796 const size_t size =
static_cast<size_t>(sizes_.data()[k]);
797 if (
size == 0)
return {};
798 return {&buffer_.data()[starts_.data()[k]], size};
801template <
typename K,
typename V>
802inline absl::Span<V> CompactVectorVector<K, V>::operator[](K key) {
804 DCHECK_LT(key, starts_.size());
805 DCHECK_LT(key, sizes_.size());
806 const int k = InternalKey(key);
807 const size_t size =
static_cast<size_t>(sizes_.data()[k]);
808 if (
size == 0)
return {};
809 return absl::MakeSpan(&buffer_.data()[starts_.data()[k]], size);
812template <
typename K,
typename V>
813inline std::vector<absl::Span<const V>>
814CompactVectorVector<K, V>::AsVectorOfSpan()
const {
815 std::vector<absl::Span<const V>> result(starts_.size());
816 for (
int k = 0; k < starts_.size(); ++k) {
817 result[k] = (*this)[k];
822template <
typename K,
typename V>
823inline void CompactVectorVector<K, V>::clear() {
829template <
typename K,
typename V>
831 return starts_.size();
834template <
typename K,
typename V>
836 return starts_.empty();
839template <
typename K,
typename V>
840template <
typename Keys,
typename Values>
847 for (
const K key : keys) {
848 max_key = std::max(max_key, InternalKey(key) + 1);
852 sizes_.assign(max_key, 0);
853 for (
const K key : keys) {
854 sizes_[InternalKey(key)]++;
858 starts_.assign(max_key, 0);
859 for (
int k = 1; k < max_key; ++k) {
860 starts_[k] = starts_[k - 1] + sizes_[k - 1];
864 buffer_.resize(keys.size());
865 for (
int i = 0; i < keys.size(); ++i) {
866 buffer_[starts_[InternalKey(keys[i])]++] = values[i];
870 for (
int k = max_key - 1; k > 0; --k) {
871 starts_[k] = starts_[k - 1];
877template <
typename K,
typename V>
878template <
typename Collection>
879inline void CompactVectorVector<K, V>::ResetFromPairs(
const Collection& pairs,
880 int minimum_num_nodes) {
882 int max_key = minimum_num_nodes;
883 for (
const auto& [key, _] : pairs) {
884 max_key = std::max(max_key, InternalKey(key) + 1);
889 sizes_.assign(minimum_num_nodes, 0);
890 starts_.assign(minimum_num_nodes, 0);
895 sizes_.assign(max_key, 0);
896 for (
const auto& [key, _] : pairs) {
897 sizes_[InternalKey(key)]++;
901 starts_.assign(max_key, 0);
902 for (
int k = 1; k < max_key; ++k) {
903 starts_[k] = starts_[k - 1] + sizes_[k - 1];
907 buffer_.resize(pairs.size());
908 for (
int i = 0;
i < pairs.size(); ++
i) {
909 const auto& [key, value] = pairs[
i];
910 buffer_[starts_[InternalKey(key)]++] = value;
914 for (
int k = max_key - 1; k > 0; --k) {
915 starts_[k] = starts_[k - 1];
921template <
typename K,
typename V>
922inline void CompactVectorVector<K, V>::ResetFromTranspose(
923 const CompactVectorVector<V, K>& other,
int min_transpose_size) {
926 if (min_transpose_size > 0) {
927 starts_.assign(min_transpose_size, 0);
928 sizes_.assign(min_transpose_size, 0);
934 int max_key = min_transpose_size;
935 for (V v = 0; v < other.size(); ++v) {
936 for (
const K k : other[v]) {
937 max_key = std::max(max_key, InternalKey(k) + 1);
942 sizes_.assign(max_key, 0);
943 for (V v = 0; v < other.size(); ++v) {
944 for (
const K k : other[v]) {
945 sizes_[InternalKey(k)]++;
950 starts_.assign(max_key, 0);
951 for (
int k = 1; k < max_key; ++k) {
952 starts_[k] = starts_[k - 1] + sizes_[k - 1];
956 buffer_.resize(other.buffer_.size());
957 for (V v = 0; v < other.size(); ++v) {
958 for (
const K k : other[v]) {
959 buffer_[starts_[InternalKey(k)]++] = v;
964 for (
int k = max_key - 1; k > 0; --k) {
965 starts_[k] = starts_[k - 1];
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 ResetFromFlatMapping(Keys keys, Values values)
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 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
absl::Span< const V > operator[](K key) 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)
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 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)
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
static int input(yyscan_t yyscanner)
std::vector< int64_t > solution