14 #ifndef OR_TOOLS_SAT_INCLUSION_H_
15 #define OR_TOOLS_SAT_INCLUSION_H_
28 #include "absl/types/span.h"
43 int Add(absl::Span<const T> data) {
45 starts_.push_back(buffer_.size());
46 sizes_.push_back(data.size());
47 buffer_.insert(buffer_.end(), data.begin(), data.end());
56 starts_.push_back(buffer_.size());
57 sizes_.push_back(data.size());
59 buffer_.push_back(
literal.Index().value());
67 DCHECK_LT(
index, starts_.size());
68 DCHECK_LT(
index, sizes_.size());
69 const size_t size =
static_cast<size_t>(sizes_[
index]);
70 if (
size == 0)
return {};
80 size_t size()
const {
return starts_.size(); }
83 std::vector<int> starts_;
84 std::vector<int> sizes_;
85 std::vector<T> buffer_;
105 template <
class Storage>
112 num_potential_subsets_ = 0;
113 num_potential_supersets_ = 0;
149 const std::function<
void(
int subset,
int superset)>& process);
154 const std::vector<bool>
IsInSuperset()
const {
return is_in_superset_; }
164 one_watcher_.clear();
165 is_in_superset_.clear();
181 const Storage& storage_;
192 bool CanBeSubset()
const {
return order <= 1; }
193 bool CanBeSuperset()
const {
return order >= 1; }
196 bool operator<(
const Candidate& other)
const {
197 return std::tie(size, order) < std::tie(other.size, other.order);
200 std::vector<Candidate> candidates_;
202 int num_potential_subsets_ = 0;
203 int num_potential_supersets_ = 0;
204 uint64_t work_done_ = 0;
209 bool stop_with_current_subset_;
210 bool stop_with_current_superset_;
211 std::vector<uint64_t> signatures_;
212 std::vector<std::vector<int>> one_watcher_;
213 std::vector<bool> is_in_superset_;
217 template <
typename Storage>
220 template <
typename Storage>
223 DCHECK_LT(
index, storage_.size());
224 const int num_elements = storage_[
index].size();
225 if (num_elements == 0)
return;
227 ++num_potential_subsets_;
228 ++num_potential_supersets_;
229 candidates_.push_back({
index, num_elements, 1});
232 template <
typename Storage>
235 DCHECK_LT(
index, storage_.size());
236 const int num_elements = storage_[
index].size();
237 if (num_elements == 0)
return;
239 ++num_potential_subsets_;
240 candidates_.push_back({
index, num_elements, 0});
243 template <
typename Storage>
246 DCHECK_LT(
index, storage_.size());
247 const int num_elements = storage_[
index].size();
248 if (num_elements == 0)
return;
251 DCHECK_LT(
index, storage_.size());
252 ++num_potential_supersets_;
253 candidates_.push_back({
index, num_elements, 2});
256 template <
typename Storage>
258 const std::function<
void(
int subset,
int superset)>& process) {
260 if (candidates_.size() <= 1)
return;
261 if (num_potential_subsets_ == 0)
return;
262 if (num_potential_supersets_ == 0)
return;
266 DCHECK(is_in_superset_.empty());
267 DCHECK(signatures_.empty());
268 DCHECK(one_watcher_.empty());
272 std::stable_sort(candidates_.begin(), candidates_.end());
273 for (
const Candidate& candidate : candidates_) {
274 const auto& candidate_elements = storage_[candidate.index];
275 const int candidate_index = signatures_.size();
279 uint64_t signature = 0;
281 for (
const int e : candidate_elements) {
283 max_element =
std::max(max_element, e);
284 signature |= (int64_t{1} << (e & 63));
286 DCHECK_EQ(is_in_superset_.size(), one_watcher_.size());
287 if (max_element >= is_in_superset_.size()) {
288 is_in_superset_.resize(max_element + 1,
false);
289 one_watcher_.resize(max_element + 1);
291 signatures_.push_back(signature);
293 stop_with_current_superset_ =
false;
294 if (candidate.CanBeSuperset()) {
295 const Candidate& superset = candidate;
296 const auto& superset_elements = candidate_elements;
299 DCHECK(std::all_of(is_in_superset_.begin(), is_in_superset_.end(),
300 [](
bool b) { return !b; }));
303 work_done_ += 2 * superset.size;
304 if (work_done_ > work_limit_)
return Stop();
305 for (
const int e : superset_elements) {
306 is_in_superset_[e] =
true;
309 const uint64_t superset_signature = signatures_.back();
310 for (
const int superset_e : superset_elements) {
311 for (
int i = 0; i < one_watcher_[superset_e].size(); ++i) {
312 const int c_index = one_watcher_[superset_e][i];
313 const Candidate& subset = candidates_[c_index];
314 DCHECK_LE(subset.size, superset.size);
317 if ((signatures_[c_index] & ~superset_signature) != 0)
continue;
320 bool is_included =
true;
321 work_done_ += subset.size;
322 if (work_done_ > work_limit_)
return Stop();
323 for (
const int subset_e : storage_[subset.index]) {
324 if (!is_in_superset_[subset_e]) {
329 if (!is_included)
continue;
331 stop_with_current_subset_ =
false;
332 process(subset.index, superset.index);
335 if (work_done_ > work_limit_)
return Stop();
337 if (stop_with_current_subset_) {
340 one_watcher_[superset_e].back());
341 one_watcher_[superset_e].pop_back();
344 if (stop_with_current_superset_)
break;
346 if (stop_with_current_superset_)
break;
350 for (
const int e : superset_elements) {
351 is_in_superset_[e] =
false;
359 if (candidate.CanBeSubset() && !stop_with_current_superset_) {
361 int best_choice = -1;
362 work_done_ += candidate.size;
363 if (work_done_ > work_limit_)
return Stop();
364 for (
const int e : candidate_elements) {
366 DCHECK_LT(e, one_watcher_.size());
367 if (best_choice == -1 ||
368 one_watcher_[e].size() < one_watcher_[best_choice].size()) {
372 DCHECK_NE(best_choice, -1);
373 one_watcher_[best_choice].push_back(candidate_index);
absl::Span< const T > operator[](int index) const
int Add(absl::Span< const T > data)
int AddLiterals(const std::vector< L > &data)
int num_potential_supersets() const
uint64_t work_done() const
void AddPotentialSubset(int index)
int num_potential_subsets() const
const std::vector< bool > IsInSuperset() const
void SetWorkLimit(uint64_t work_limit)
void StopProcessingCurrentSubset()
void AddPotentialSet(int index)
void AddPotentialSuperset(int index)
void StopProcessingCurrentSuperset()
void IncreaseWorkDone(uint64_t increase)
InclusionDetector(const Storage &storage)
void DetectInclusions(const std::function< void(int subset, int superset)> &process)
void swap(IdMap< K, V > &a, IdMap< K, V > &b)
InclusionDetector(const Storage &storage) -> InclusionDetector< Storage >
Collection of objects used to extend the Constraint Solver library.