168 absl::MutexLock mutex_lock(mutex_);

171 }

174 absl::MutexLock mutex_lock(mutex_);

175 return num_non_improving_;

176 }

179 absl::MutexLock mutex_lock(mutex_);

180 new_solutions_.clear();

181 solutions_.clear();

182 ++source_id_;

183 }

186 absl::MutexLock mutex_lock(mutex_);

187 return source_id_;

188 }

191 absl::MutexLock mutex_lock(mutex_);

192 return num_queried_;

193 }

226 public:

230

231 void NewLPSolution(std::vector<double> lp_solution);

232};

237 public:

245

249

250

251

252 std::shared_ptr<const SharedSolutionRepository<int64_t>::Solution>

270

271 std::shared_ptr<const SharedSolutionRepository<int64_t>::Solution> Add(

273

274 void Synchronize(absl::BitGenRef random);

275

280

281 private:

282

285

286

287

288

289

290

291

292

293

294 absl::Mutex mutex_;

295 int64_t max_rank_ ABSL_GUARDED_BY(mutex_) =

296 std::numeric_limits<int64_t>::min();

297 int64_t min_rank_ ABSL_GUARDED_BY(mutex_) =

298 std::numeric_limits<int64_t>::max();

299 std::vector<int64_t> ranks_;

300 std::vector<

301 std::shared_ptr<const SharedSolutionRepository<int64_t>::Solution>>

302 ABSL_GUARDED_BY(mutex_) seeds_;

303};

315 public:

318

325};

336 public:

337

338

339 void AddSolution(const std::vector<double>& lp_solution);

340

342

343

344 std::vector<double> PopLast();

345

351

352 private:

353 mutable absl::Mutex mutex_;

354 std::deque<std::vector<double>> solutions_ ABSL_GUARDED_BY(mutex_);

355 int64_t num_added_ ABSL_GUARDED_BY(mutex_) = 0;

356 mutable int64_t num_queried_ ABSL_GUARDED_BY(mutex_) = 0;

357};

365 public:

367

368

369

370

371

372

374

375

376

377

379

380

381

382

383

384

385

387

388

389

391 std::function<void(std::vector<int64_t>*)> postprocessor);

392

393

394

397

398

399

402

403

404

407

408

409

411

412

413

414

415

416

417

418

419

420

424

425

426

427

428

431

432

433

434

435

436

437

438

439

440

442 std::function<std::string(const CpSolverResponse&)> callback);

444

445

446

447

448

449

452

453

454

455

456

457

458

459

470

471

472

474

475

476

477

478

479

480

481

482

483

484

485

486

487

488

489

492

493

494

495

497

498

499

500

501

502

504

505

507 IntegerValue lb, IntegerValue ub);

508

509

510

511

512

513 std::shared_ptr<const SharedSolutionRepository<int64_t>::Solution>

514 NewSolution(absl::Span<const int64_t> solution_values,

515 absl::string_view solution_info, Model* model = nullptr,

516 int source_id = -1);

517

518

519

520

521

522

523

525

526

527

528 void AddUnsatCore(const std::vector<int>& core);

529

530

531

532

534

538

539

540

542

543

547

548

549 void LogMessage(absl::string_view prefix, absl::string_view message);

551 absl::string_view message);

553

555

559

560

561

565 const std::vector<int64_t>& DebugSolution() const { return debug_solution_; }

566

567 private:

568 void TestGapLimitsIfNeeded() ABSL_EXCLUSIVE_LOCKS_REQUIRED(mutex_);

569 void FillObjectiveValuesInResponse(CpSolverResponse* response) const

570 ABSL_EXCLUSIVE_LOCKS_REQUIRED(mutex_);

571 void UpdateGapIntegralInternal() ABSL_EXCLUSIVE_LOCKS_REQUIRED(mutex_);

572

574 ABSL_EXCLUSIVE_LOCKS_REQUIRED(mutex_);

575

577 ABSL_EXCLUSIVE_LOCKS_REQUIRED(mutex_);

578

579

581 absl::Span<const int64_t> variable_values,

582 absl::string_view solution_info) ABSL_EXCLUSIVE_LOCKS_REQUIRED(mutex_);

583

589

590 mutable absl::Mutex mutex_;

591

592

593 double absolute_gap_limit_ ABSL_GUARDED_BY(mutex_) = 0.0;

594 double relative_gap_limit_ ABSL_GUARDED_BY(mutex_) = 0.0;

595

597 CpSolverStatus synchronized_best_status_ ABSL_GUARDED_BY(mutex_) =

599 std::vector<int> unsat_cores_ ABSL_GUARDED_BY(mutex_);

601

602 int num_solutions_ ABSL_GUARDED_BY(mutex_) = 0;

603 int64_t inner_objective_lower_bound_ ABSL_GUARDED_BY(mutex_) =

604 std::numeric_limits<int64_t>::min();

605 int64_t inner_objective_upper_bound_ ABSL_GUARDED_BY(mutex_) =

606 std::numeric_limits<int64_t>::max();

607 int64_t best_solution_objective_value_ ABSL_GUARDED_BY(mutex_) =

608 std::numeric_limits<int64_t>::max();

609

610 bool always_synchronize_ ABSL_GUARDED_BY(mutex_) = true;

611 IntegerValue synchronized_inner_objective_lower_bound_ ABSL_GUARDED_BY(

612 mutex_) = IntegerValue(std::numeric_limits<int64_t>::min());

613 IntegerValue synchronized_inner_objective_upper_bound_ ABSL_GUARDED_BY(

614 mutex_) = IntegerValue(std::numeric_limits<int64_t>::max());

615

616 bool update_integral_on_each_change_ ABSL_GUARDED_BY(mutex_) = false;

617 double gap_integral_ ABSL_GUARDED_BY(mutex_) = 0.0;

618 double last_absolute_gap_ ABSL_GUARDED_BY(mutex_) = 0.0;

619 double last_gap_integral_time_stamp_ ABSL_GUARDED_BY(mutex_) = 0.0;

620

621 int next_callback_id_ ABSL_GUARDED_BY(mutex_) = 0;

623 callbacks_ ABSL_GUARDED_BY(mutex_);

624

625 int next_search_log_callback_id_ ABSL_GUARDED_BY(mutex_) = 0;

626 std::vector<

628 search_log_callbacks_ ABSL_GUARDED_BY(mutex_);

629

630 int next_best_bound_callback_id_ ABSL_GUARDED_BY(mutex_) = 0;

631 std::vector<std::pair<int, std::function<void(double)>>> best_bound_callbacks_

632 ABSL_GUARDED_BY(mutex_);

633

634 std::vector<std::function<void(std::vector<int64_t>*)>>

635 solution_postprocessors_ ABSL_GUARDED_BY(mutex_);

637 ABSL_GUARDED_BY(mutex_);

639 ABSL_GUARDED_BY(mutex_);

641 statistics_postprocessors_ ABSL_GUARDED_BY(mutex_);

643 status_change_callbacks_ ABSL_GUARDED_BY(mutex_);

644

645

646 std::string dump_prefix_;

647

648 SolverLogger* logger_ ABSL_GUARDED_BY(mutex_);

649 absl::flat_hash_map<std::string, int> throttling_ids_ ABSL_GUARDED_BY(mutex_);

650

651 int bounds_logging_id_;

652 std::vector<CpSolverResponse> subsolver_responses_ ABSL_GUARDED_BY(mutex_);

653

654 std::atomic<bool> first_solution_solvers_should_stop_ = false;

655

656 std::vector<int64_t> debug_solution_;

657};

662 public:

664

665

666

667

669 absl::Span<const int> variables,

670 absl::Span<const int64_t> new_lower_bounds,

671 absl::Span<const int64_t> new_upper_bounds);

672

673

674

675

676

677

678

679

680

681

683 absl::Span<const int> variables_to_fix);

684

685

686

687

689

690

691

693 std::vector<int64_t>* new_lower_bounds,

694 std::vector<int64_t>* new_upper_bounds);

695

696

697

698 void UpdateDomains(std::vector<Domain>* domains);

699

700

701

703

706

707

708

709

713

714

718

719 private:

720 const int num_variables_;

722

723 absl::Mutex mutex_;

724

725

726 std::vector<int64_t> lower_bounds_ ABSL_GUARDED_BY(mutex_);

727 std::vector<int64_t> upper_bounds_ ABSL_GUARDED_BY(mutex_);

729 ABSL_GUARDED_BY(mutex_);

730 int64_t total_num_improvements_ ABSL_GUARDED_BY(mutex_) = 0;

731

732

733 std::vector<int64_t> synchronized_lower_bounds_ ABSL_GUARDED_BY(mutex_);

734 std::vector<int64_t> synchronized_upper_bounds_ ABSL_GUARDED_BY(mutex_);

735 std::deque<SparseBitset<int>> id_to_changed_variables_

736 ABSL_GUARDED_BY(mutex_);

737

738

739

740 struct Counters {

741 int64_t num_exported = 0;

742 int64_t num_symmetric = 0;

743 };

744 absl::btree_map<std::string, Counters> bounds_exported_

745 ABSL_GUARDED_BY(mutex_);

746

747

748 bool has_symmetry_ = false;

749 std::vector<int> var_to_representative_;

750 std::vector<int> var_to_orbit_index_;

751 CompactVectorVector<int, int> orbits_;

752

753 std::vector<int64_t> debug_solution_;

754 std::string dump_prefix_;

755 int export_counter_ = 0;

756};

776 public:

781

783

785

788

789

790

791 bool Add(absl::Span<const int> clause, int lbd = 2);

792

793

794

795

796

797 bool BlockClause(absl::Span<const int> clause);

798

799

800

801

802

804

810

811

812 int NumLiteralsOfSize(int size) const;

813 int NumBufferedLiterals() const;

814

817

818

819 static size_t HashClause(absl::Span<const int> clause, size_t hash_seed = 0);

820

821 private:

822

823

824 constexpr static size_t kMaxFingerprints = 1024 * 1024 / sizeof(size_t);

825 constexpr static int kNumSizes = kMaxClauseSize - kMinClauseSize + 1;

826

827 std::vector<int>* MutableBufferForSize(int size) {

828 return &clauses_by_size_[size - kMinClauseSize];

829 }

830 absl::Span<const int> BufferForSize(int size) const {

831 return clauses_by_size_[size - kMinClauseSize];

832 }

833 absl::Span<const int> NextClause(int size) const;

834 void PopClause(int size);

835

836 int NumClausesOfSize(int size) const;

837

838 int lbd_threshold_ = kMinLbd;

839 int64_t dropped_literals_since_last_batch_ = 0;

840

841 absl::flat_hash_set<size_t> fingerprints_;

842 absl::flat_hash_set<size_t> old_fingerprints_;

843 std::array<std::vector<int>, kNumSizes> clauses_by_size_;

844};

854 public:

857

858

859

860

862

864

865

866

867

868

870 std::vector<std::pair<int, int>>* new_clauses);

871

872

873 int RegisterNewId(absl::string_view worker_name, bool may_terminate_early);

874

875

876

878

879

880

882

883

885

886 private:

887

888 bool ShouldReadBatch(int reader_id, int writer_id)

889 ABSL_EXCLUSIVE_LOCKS_REQUIRED(mutex_);

890

891 static constexpr int kMinBatches = 64;

892 mutable absl::Mutex mutex_;

893

894

895

896 absl::flat_hash_set<std::pair<int, int>> added_binary_clauses_set_

897 ABSL_GUARDED_BY(mutex_);

898 std::vector<std::pair<int, int>> added_binary_clauses_

899 ABSL_GUARDED_BY(mutex_);

900 std::vector<int> id_to_last_processed_binary_clause_ ABSL_GUARDED_BY(mutex_);

901 int last_visible_binary_clause_ ABSL_GUARDED_BY(mutex_) = 0;

902

903

904

905

906 std::vector<int> id_to_last_returned_batch_ ABSL_GUARDED_BY(mutex_);

907 std::vector<int> id_to_last_finished_batch_ ABSL_GUARDED_BY(mutex_);

908

909 std::deque<CompactVectorVector<int>> batches_ ABSL_GUARDED_BY(mutex_);

910

911

912

913

914 std::vector<CompactVectorVector<int>> pending_batches_

915 ABSL_GUARDED_BY(mutex_);

916 int num_full_workers_ ABSL_GUARDED_BY(mutex_) = 0;

917

918 const bool always_synchronize_ = true;

919

920

921 std::vector<int64_t> id_to_num_exported_ ABSL_GUARDED_BY(mutex_);

922 std::vector<int64_t> id_to_num_imported_ ABSL_GUARDED_BY(mutex_);

923 std::vector<int64_t> id_to_num_updated_ ABSL_GUARDED_BY(mutex_);

924 std::vector<std::string> id_to_worker_name_ ABSL_GUARDED_BY(mutex_);

925};

932 public:

935

936

937

964

965

966 void Add(int id, Key expr, IntegerValue lb, IntegerValue ub);

967

968

969

970

971

972 int RegisterNewImportId(std::string name);

973

974

975

976 std::vector<std::pair<Key, std::pair<IntegerValue, IntegerValue>>>

977 NewlyUpdatedBounds(int import_id);

978

979

980

981

986

987 private:

988 void MaybeCompressNewlyUpdateKeys() ABSL_EXCLUSIVE_LOCKS_REQUIRED(mutex_);

989

990 absl::Mutex mutex_;

991

992

993 absl::flat_hash_map<Key, std::pair<IntegerValue, IntegerValue>> shared_bounds_

994 ABSL_GUARDED_BY(mutex_);

995

996

997

998

999

1000

1001

1002

1003

1004 std::vector<Key> newly_updated_keys_;

1005

1006

1007 std::vector<std::string> import_id_to_name_ ABSL_GUARDED_BY(mutex_);

1008 std::vector<int> import_id_to_index_ ABSL_GUARDED_BY(mutex_);

1009 std::vector<int> import_id_to_num_imported_ ABSL_GUARDED_BY(mutex_);

1010

1011

1012 struct Stats {

1013 int64_t num_new = 0;

1014 int64_t num_update = 0;

1015 int64_t num_imported = 0;

1016 bool empty() const {

1017 return num_new == 0 && num_update == 0 && num_imported == 0;

1018 }

1019 };

1020 std::vector<Stats> id_to_stats_ ABSL_GUARDED_BY(mutex_);

1021 std::vector<std::string> id_to_worker_name_ ABSL_GUARDED_BY(mutex_);

1022};

1026 public:

1028

1029

1030 void AddStats(absl::Span<const std::pair<std::string, int64_t>> stats);

1031

1032

1034

1035 private:

1036 absl::Mutex mutex_;

1037 absl::flat_hash_map<std::string, int64_t> stats_ ABSL_GUARDED_BY(mutex_);

1038};

1042 absl::MutexLock mutex_lock(mutex_);

1043 return solutions_.size();

1044}

1049 absl::MutexLock mutex_lock(mutex_);

1050 if (i >= solutions_.size()) return nullptr;

1051 ++num_queried_;

1052 return solutions_[i];

1053}

1057 absl::MutexLock mutex_lock(mutex_);

1058 if (solutions_.empty()) return std::numeric_limits<int64_t>::max();

1059 return solutions_[0]->rank;

1060}

1066 absl::MutexLock mutex_lock(mutex_);

1067

1068 DCHECK(absl::c_is_sorted(solutions_,

1069 [](const std::shared_ptr<const Solution>& a,

1070 const std::shared_ptr<const Solution>& b) {

1071 return a->rank < b->rank;

1072 }));

1073 DCHECK(absl::c_adjacent_find(solutions_,

1074 [](const std::shared_ptr<const Solution>& a,

1075 const std::shared_ptr<const Solution>& b) {

1076 return *a == *b;

1077 }) == solutions_.end());

1078 std::vector<std::shared_ptr<const Solution>> result;

1079 const int num_solutions = std::min(static_cast<int>(solutions_.size()), n);

1080 result.reserve(num_solutions);

1081 for (int i = 0; i < num_solutions; ++i) {

1082 result.push_back(solutions_[i]);

1083 }

1084 return result;

1085}

1089 int var_index, int solution_index) const {

1090 absl::MutexLock mutex_lock(mutex_);

1091 return solutions_[solution_index]->variable_values[var_index];

1092}

1098 absl::BitGenRef random) const {

1099 absl::MutexLock mutex_lock(mutex_);

1100 if (solutions_.empty()) return nullptr;

1101 ++num_queried_;

1102 int index = 0;

1103

1104 if (solutions_.size() > 1) {

1105 const int64_t best_rank = solutions_[0]->rank;

1106

1107

1108

1109

1110

1111

1112

1113

1114 const int kExplorationThreshold = 100;

1115

1116

1117 tmp_indices_.clear();

1118 for (int i = 0; i < solutions_.size(); ++i) {

1119 std::shared_ptr<const Solution> solution = solutions_[i];

1120 if (solution->rank == best_rank &&

1121 solution->num_selected <= kExplorationThreshold) {

1122 tmp_indices_.push_back(i);

1123 }

1124 }

1125

1126 if (tmp_indices_.empty()) {

1127 index = absl::Uniform<int>(random, 0, solutions_.size());

1128 } else {

1129 index = tmp_indices_[absl::Uniform<int>(random, 0, tmp_indices_.size())];

1130 }

1131 }

1132

1133 CHECK_GE(index, 0);

1134 CHECK_LT(index, solutions_.size());

1135 solutions_[index]->num_selected++;

1136 return solutions_[index];

1137}

1142 std::shared_ptr<Solution> solution_ptr =

1143 std::make_shared<Solution>(std::move(solution));

1145 {

1146 absl::MutexLock mutex_lock(mutex_);

1147 ++num_added_;

1148 solution_ptr->source_id = source_id_;

1149 new_solutions_.push_back(solution_ptr);

1150 }

1151 return solution_ptr;

1152}

1157 absl::MutexLock mutex_lock(mutex_);

1158 if (new_solutions_.empty()) {

1159 const int64_t diff = num_queried_ - num_queried_at_last_sync_;

1160 num_non_improving_ += diff;

1161 num_queried_at_last_sync_ = num_queried_;

1162 return;

1163 }

1164

1165 if (f != nullptr) {

1167 &new_solutions_,

1168 [](const std::shared_ptr<Solution>& a,

1169 const std::shared_ptr<Solution>& b) { return *a < *b; });

1170 for (const auto& ptr : new_solutions_) {

1171 f(*ptr);

1172 }

1173 }

1174

1175 const int64_t old_best_rank = solutions_.empty()

1176 ? std::numeric_limits<int64_t>::max()

1177 : solutions_[0]->rank;

1178

1179 solutions_.insert(solutions_.end(), new_solutions_.begin(),

1180 new_solutions_.end());

1181 new_solutions_.clear();

1182

1183

1184

1186 &solutions_, [](const std::shared_ptr<Solution>& a,

1187 const std::shared_ptr<Solution>& b) { return *a < *b; });

1188 const int64_t new_best_rank = solutions_[0]->rank;

1189

1190

1191

1194 int num_best = 1;

1195 while (num_best < solutions_.size() &&

1196 solutions_[num_best]->rank == new_best_rank) {

1197 ++num_best;

1198 }

1199

1202

1203

1204

1205 for (auto& solution : solutions_) {

1206 if (solution->num_selected == 0) {

1207

1208 std::swap(solutions_[0], solution);

1209 break;

1210 }

1211 }

1212

1213

1214

1216

1217

1218 const int n = solutions_.size();

1219 distances_.resize(n * n);

1220 const int size = solutions_[0]->variable_values.size();

1221 for (int i = 0; i < n; ++i) {

1222 for (int j = i + 1; j < n; ++j) {

1223 int64_t dist = 0;

1224 for (int k = 0; k < size; ++k) {

1225 if (solutions_[i]->variable_values[k] !=

1226 solutions_[j]->variable_values[k]) {

1227 ++dist;

1228 }

1229 }

1230 distances_[i * n + j] = distances_[j * n + i] = dist;

1231 }

1232 }

1233

1234

1235

1236

1237

1238

1239

1240

1241

1242

1243 const std::vector<int> selected =

1245 1);

1246

1247 DCHECK(std::is_sorted(selected.begin(), selected.end()));

1248 int new_size = 0;

1249 for (const int s : selected) {

1250 solutions_[new_size++] = std::move(solutions_[s]);

1251 }

1252 solutions_.resize(new_size);

1253

1254 if (VLOG_IS_ON(3)) {

1255 int min_count = std::numeric_limits<int>::max();

1256 int max_count = 0;

1257 for (const auto& s : solutions_) {

1258 CHECK(s != nullptr);

1259 min_count = std::min(s->num_selected, min_count);

1260 max_count = std::max(s->num_selected, max_count);

1261 }

1262 int64_t score = 0;

1263 for (const int i : selected) {

1264 for (const int j : selected) {

1265 if (i > j) score += distances_[i * n + j];

1266 }

1267 }

1268 LOG(INFO) << name_ << " rank=" << new_best_rank

1270 << " orthogonality=" << score << " count=[" << min_count

1271 << ", " << max_count << "]";

1272 }

1273 }

1274 }

1275

1278 }

1279 CHECK(!solutions_.empty());

1280 if (!solutions_.empty()) {

1281 VLOG(4) << "Solution pool update:" << " num_solutions=" << solutions_.size()

1282 << " min_rank=" << solutions_[0]->rank

1283 << " max_rank=" << solutions_.back()->rank;

1284 }

1285

1286 num_synchronization_++;

1287 if (new_best_rank < old_best_rank) {

1288 num_non_improving_ = 0;

1289 } else {

1290 const int64_t diff = num_queried_ - num_queried_at_last_sync_;

1291 num_non_improving_ += diff;

1292 }

1293 num_queried_at_last_sync_ = num_queried_;

1294}