Iterative partitioning

CHANGELOG

@@ -9,6 +9,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
  * add AWS docker infrastructure
  * add gate detection for portfolio configurations
+ * allow to use partitioning in parallel solving
 
 ## [4.0-rc3]
 

minisat/core/Solver.cc

@@ -3693,6 +3693,7 @@ void Solver::enableDISTANCEheuristic()
 // NOTE: assumptions passed in member-variable 'assumptions'.
 lbool Solver::solve_()
 {
+    assert(decisionLevel() == 0);
     model.clear();
     conflict.clear();
     if (!ok) {

minisat/parallel/JobQueue.h

@@ -256,7 +256,7 @@ class JobQueue
             _threadState = nullptr;
             if (_threads) delete[] _threads;
             _threads = nullptr;
-            throw "Failed to allocate jobqueue structs";
+            throw("Failed to allocate jobqueue structs");
         }
 
         _workState = 0;

minisat/parallel/ParSolver.h

@@ -23,6 +23,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "mtl/Queue.h"
 #include "simp/SimpSolver.h"
 
+#include "parallel/PartitionTree.h"
 #include "parallel/Sharing.h"
 
 #include <atomic>
@@ -58,6 +59,7 @@ class ParSolver : protected SimpSolver
         lbool _status = l_Undef;                        // status of the associated SAT solver
         double _idle_s = 0;                             // seconds this thread idled while waiting
         uint64_t _attempted_to_sync = 0;                // number of attempts to enter a sync
+        uint64_t _syncs = 0;                            // number of performed syncs
         uint64_t _next_sync_counter_limit = 0;          // indicate when to actually sync next
         uint64_t _next_sync_current_accesses = 0;       // stores number of accesses when entring successful sync
         uint64_t _next_sync_previous_limit = 0;         // stores the previous limit we have seen in a given sync
@@ -69,6 +71,12 @@ class ParSolver : protected SimpSolver
         ClausePool pool;                                // store for learned clauses that are shared by this thread
         uint64_t received_clauses = 0;                  // number of clauses a thread received
 
+        int partitionID = PartitionTree::INVALID_ID;    // index to node in partition tree slot that stores node
+                                                        // assigned to this thread
+        int newPartitionID = PartitionTree::INVALID_ID; // ID of the parititon to be solved next
+        vec<Lit> partitionClauses;     // if non-empty, these clause partition to currently assigned node
+        vec<Lit> partitionAssumptions; // assumptions used by the solver when working on a node
+
         vec<TaskType> tasks; // task to be executed before next sync test
 
         SolverData(ParSolver *parent, int threadnr) : _parent(parent), _threadnr(threadnr) {}
@@ -91,6 +99,20 @@ class ParSolver : protected SimpSolver
             _blocked_by_barrier = 0;
             received_clauses = 0;
         }
+
+        /// tell whether this node solves the original formula or a partition
+        bool solvesPartition() const { return partitionID != PartitionTree::INVALID_ID; }
+
+        /// unassign current partition, and reset status of solver
+        void resetPartitioningState()
+        {
+            assert(solvesPartition() && "only reset in case a partition is active");
+            _status = l_Undef;
+            partitionID = PartitionTree::INVALID_ID;
+            partitionAssumptions.clear();
+            partitionClauses.clear();
+            _status = l_Undef;
+        }
     };
 
     public:
@@ -150,6 +172,7 @@ class ParSolver : protected SimpSolver
 
     // Mode of operation:
     //
+    using SimpSolver::conflict;
     using SimpSolver::parsing;
     void set_parsing(bool is_parsing = true);
     void set_verbosity(int verb);
@@ -209,6 +232,11 @@ class ParSolver : protected SimpSolver
     uint64_t base_sync_increase;              // how much to bump number of accesses before next sync
     SYNC_UPDATE_METHOD sync_step_update_mode; // how to update step limits for next sync
 
+    PartitionTree partitionTree;                // store structure of partitions
+    int32_t partitioningDelaySyncs;             // number of syncs before starting/continuing partitioning
+    uint32_t partitionsPerNode;                 // split a formula into this amount of new partitions
+    std::atomic<bool> notifyEvaluatePartitions; // if set, partitions are found to be unsatisfiable, so that we need to evaluate
+
     std::atomic<int> solved_current_call; // indicate that the current solving task has been solved (10 or 20), if not 0
     std::atomic<bool> sync_by_primary;    // false, if true, search will be non-deterministic
     size_t synced_clauses;                // store number of clauses in primary solver after last sync (after solving)
@@ -255,12 +283,23 @@ class ParSolver : protected SimpSolver
     bool sharingReceiveFilterAccept(const Clause &c, size_t threadnr);
 
     /// assign (new) extra tasks, return false on UNSAT
-    bool assignExtraTask(size_t threadnr);
+    bool assignPartitionAndTasks(size_t threadnr);
     /// evaluate the results of the previously assigned tasks, return false on UNSAT
     bool evaluateExtraTask(size_t threadnr);
     /// check, and execute, pending task for a given extra thread, return false on UNSAT
     bool runAssignedExtraTask(size_t threadnr);
 
+    /// handle assigning a nodeID to a thread
+    void assignNewThreadPartition(size_t threadnr, int partitionID);
+    /// process solver status wrt assumptions, e.g. impact of returned conflict clause to reset partition of the node
+    void evaluateSolverStatus(size_t threadnr);
+    /// Handle partitioning related tasks during synchronization
+    void handlePartitionsDuringSync(size_t threadnr);
+    /// set a thread to partition the node that is currently assigned
+    bool partitionAssignedNode(size_t threadnr);
+    /// check status of partition tree, return false on UNSAT
+    bool evaluatePartitionTree();
+
     /// return new limit to be set next
     uint64_t get_next_sync_limit(size_t threadnr) const;
     /// return additional increment for steps until next sync