1 // Copyright 2010-2021 Google LLC 2 // Licensed under the Apache License, Version 2.0 (the "License"); 3 // you may not use this file except in compliance with the License. 4 // You may obtain a copy of the License at 5 // 6 // http://www.apache.org/licenses/LICENSE-2.0 7 // 8 // Unless required by applicable law or agreed to in writing, software 9 // distributed under the License is distributed on an "AS IS" BASIS, 10 // WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. 11 // See the License for the specific language governing permissions and 12 // limitations under the License. 13 14 // Simple framework for choosing and distributing a solver "sub-tasks" on a set 15 // of threads. 16 17 #ifndef OR_TOOLS_SAT_SUBSOLVER_H_ 18 #define OR_TOOLS_SAT_SUBSOLVER_H_ 19 20 #include <algorithm> 21 #include <cmath> 22 #include <cstdint> 23 #include <functional> 24 #include <string> 25 #include <vector> 26 27 #include "ortools/base/integral_types.h" 28 29 #if !defined(__PORTABLE_PLATFORM__) 30 #include "ortools/base/threadpool.h" 31 #endif // __PORTABLE_PLATFORM__ 32 33 namespace operations_research { 34 namespace sat { 35 36 // The API used for distributing work. Each subsolver can generate tasks and 37 // synchronize itself with the rest of the world. 38 // 39 // Note that currently only the main thread interact with subsolvers. Only the 40 // tasks generated by GenerateTask() are executed in parallel in a threadpool. 41 class SubSolver { 42 public: SubSolver(const std::string & name)43 explicit SubSolver(const std::string& name) : name_(name) {} ~SubSolver()44 virtual ~SubSolver() {} 45 46 // Returns true iff GenerateTask() can be called. 47 // 48 // Note(user): In the current design, a SubSolver is never deleted until the 49 // end of the Solve() that created it. But is is okay to always return false 50 // here and release the memory used by the Subsolver internal if there is no 51 // need to call this Subsolver ever again. The overhead of iterating over it 52 // in the main solver loop should be minimal. 53 virtual bool TaskIsAvailable() = 0; 54 55 // Returns a task to run. The task_id is just an ever increasing counter that 56 // correspond to the number of total calls to GenerateTask(). 57 // 58 // TODO(user): We could use a more complex selection logic and pass in the 59 // deterministic time limit this subtask should run for. Unclear at this 60 // stage. 61 virtual std::function<void()> GenerateTask(int64_t task_id) = 0; 62 63 // Synchronizes with the external world from this SubSolver point of view. 64 // Also incorporate the results of the latest completed tasks if any. 65 // 66 // Note(user): The intended implementation for determinism is that tasks 67 // update asynchronously (and so non-deterministically) global "shared" 68 // classes, but this global state is incorporated by the Subsolver only when 69 // Synchronize() is called. 70 virtual void Synchronize() = 0; 71 72 // Returns the score as updated by the completed tasks before the last 73 // Synchronize() call. Everything else being equal, we prefer to run a 74 // SubSolver with the highest score. 75 // 76 // TODO(user): This is unused for now. score()77 double score() const { return score_; } 78 79 // Returns the total deterministic time spend by the completed tasks before 80 // the last Synchronize() call. deterministic_time()81 double deterministic_time() const { return deterministic_time_; } 82 83 // Returns the name of this SubSolver. Used in logs. name()84 std::string name() const { return name_; } 85 86 // Returns search statistics. StatisticsString()87 virtual std::string StatisticsString() const { return std::string(); } 88 89 protected: 90 const std::string name_; 91 double score_ = 0.0; 92 double deterministic_time_ = 0.0; 93 }; 94 95 // A simple wrapper to add a synchronization point in the list of subsolvers. 96 class SynchronizationPoint : public SubSolver { 97 public: SynchronizationPoint(std::function<void ()> f)98 explicit SynchronizationPoint(std::function<void()> f) 99 : SubSolver(""), f_(std::move(f)) {} TaskIsAvailable()100 bool TaskIsAvailable() final { return false; } GenerateTask(int64_t task_id)101 std::function<void()> GenerateTask(int64_t task_id) final { return nullptr; } Synchronize()102 void Synchronize() final { f_(); } 103 104 private: 105 std::function<void()> f_; 106 }; 107 108 // Executes the following loop: 109 // 1/ Synchronize all in given order. 110 // 2/ generate and schedule one task from the current "best" subsolver. 111 // 3/ repeat until no extra task can be generated and all tasks are done. 112 // 113 // The complexity of each selection is in O(num_subsolvers), but that should 114 // be okay given that we don't expect more than 100 such subsolvers. 115 // 116 // Note that it is okay to incorporate "special" subsolver that never produce 117 // any tasks. This can be used to synchronize classes used by many subsolvers 118 // just once for instance. 119 void NonDeterministicLoop( 120 const std::vector<std::unique_ptr<SubSolver>>& subsolvers, int num_threads); 121 122 // Similar to NonDeterministicLoop() except this should result in a 123 // deterministic solver provided that all SubSolver respect the Synchronize() 124 // contract. 125 // 126 // Executes the following loop: 127 // 1/ Synchronize all in given order. 128 // 2/ generate and schedule up to batch_size tasks using an heuristic to select 129 // which one to run. 130 // 3/ wait for all task to finish. 131 // 4/ repeat until no task can be generated in step 2. 132 void DeterministicLoop( 133 const std::vector<std::unique_ptr<SubSolver>>& subsolvers, int num_threads, 134 int batch_size); 135 136 // Same as above, but specialized implementation for the case num_threads=1. 137 // This avoids using a Threadpool altogether. It should have the same behavior 138 // than the functions above with num_threads=1 and batch_size=1. Note that an 139 // higher batch size will not behave in the same way, even if num_threads=1. 140 void SequentialLoop(const std::vector<std::unique_ptr<SubSolver>>& subsolvers); 141 142 } // namespace sat 143 } // namespace operations_research 144 145 #endif // OR_TOOLS_SAT_SUBSOLVER_H_ 146