Add strict-cube and decision-trail partitioning strategies (#8651)

Add the strict-cube modification to the revised partitioning algorithm and add the full-trail partitioning strategy.

diff --git a/src/options/parallel_options.toml b/src/options/parallel_options.toml
index 9d5c288b90148b79669d19e45b61358c91d9d9de..5ebbc1a1d9c029dacd780c01f77474cc692a9da3 100644 (file)
--- a/src/options/parallel_options.toml
+++ b/src/options/parallel_options.toml
@@ -37,6 +37,12 @@ name   = "Parallel"
 [[option.mode.REVISED]]
   name = "revised"
   help = "For 4 partitions, creates cubes C1, C2, C3, !C1 & !C2 & !C3"
+[[option.mode.STRICT_CUBE]]
+  name = "strict-cube"
+  help = "For 4 partitions, creates cubes C1, !C1 & C2, !C1 & !C2 & C3, !C1 & !C2 & !C3"
+[[option.mode.DECISION_TRAIL]]
+  name = "decision-trail"
+  help = "Creates mutually exclusive cubes from the decisions in the SAT solver."
 
 [[option]]
   name       = "partitionCheck"

diff --git a/src/theory/partition_generator.cpp b/src/theory/partition_generator.cpp
index 8b5ee94e116f1c8443275d4450349e2cbff8924b..f829fd1a09ec70d5e5f85763eb8409c91bd7fe92 100644 (file)
--- a/src/theory/partition_generator.cpp
+++ b/src/theory/partition_generator.cpp
@@ -106,7 +106,7 @@ TrustNode PartitionGenerator::stopPartitioning() const
 // C2 = l2_{1} & .... & l2_{d_conflictSize}
 // C3 = l3_{1} & .... & l3_{d_conflictSize}
 // C4 = !C1 & !C2 & !C3
-TrustNode PartitionGenerator::makeRevisedPartitions()
+TrustNode PartitionGenerator::makeRevisedPartitions(bool strict)
 {
   // If we're not at the last cube
   if (d_numPartitionsSoFar < d_numPartitions - 1)
@@ -122,9 +122,30 @@ TrustNode PartitionGenerator::makeRevisedPartitions()
     }
 
     literals.resize(d_conflictSize);
-    // Make first cube and emit it.
+    // Make cube from literals
     Node conj = NodeManager::currentNM()->mkAnd(literals);
-    emitCube(conj);
+
+    // For the strict-cube strategy, cubes look like the following:
+    // C1 =             l1_{1} & .... & l1_{d_conflictSize}
+    // C2 = !C1 &       l2_{1} & .... & l2_{d_conflictSize}
+    // C3 = !C1 & !C2 & l3_{1} & .... & l3_{d_conflictSize}
+    // C4 = !C1 & !C2 & !C3
+    if (strict)
+    {
+      vector<Node> toEmit;
+      for (const Node& c : d_cubes) 
+      {
+        toEmit.push_back(c.notNode());
+      }
+      toEmit.push_back(conj);
+      Node cube = NodeManager::currentNM()->mkAnd(toEmit);
+
+      emitCube(cube);
+    }
+    else
+    {
+      emitCube(conj);
+    }
     // Add to the list of cubes.
     d_cubes.push_back(conj);
     return blockPath(conj);
@@ -133,7 +154,10 @@ TrustNode PartitionGenerator::makeRevisedPartitions()
   else
   {
     vector<Node> nots;
-    for (auto c : d_cubes) nots.push_back(c.notNode());
+    for (const Node& c : d_cubes)
+    {
+      nots.push_back(c.notNode());
+    }
     Node lemma = NodeManager::currentNM()->mkAnd(nots);
     // Emit not(cube_one) and not(cube_two) and ... and not(cube_n-1)
     emitCube(lemma);
@@ -141,6 +165,76 @@ TrustNode PartitionGenerator::makeRevisedPartitions()
   }
 }
 
+
+TrustNode PartitionGenerator::makeFullTrailPartitions()
+{
+  std::vector<TNode> literals = collectDecisionLiterals();
+  uint64_t numVar = static_cast<uint64_t>(log2(d_numPartitions));
+  if (literals.size() >= numVar)
+  {
+    literals.resize(numVar);
+
+    // This complicated thing is basically making a truth table
+    // of with 2^numVar variable so that each row can be emitted as a partition
+    // later. Each entry in resultNodeLists is a row corresponding to a cube:
+    // resultNodeLists = {
+    //   { l1,  l2}
+    //   { l1, !l2}
+    //   {!l1,  l2}
+    //   {!l1, !l2} }
+
+    // total number of cubes/rows
+    size_t total = pow(2, numVar);
+
+    // resultNodeLists is built column by column. 
+    std::vector<std::vector<TNode> > resultNodeLists(total);
+
+    // t is used to determine whether to push the node or its not_node.
+    bool t = false;
+
+    // numConsecutiveTF tracks how many times the node should be consectuively 
+    // true or false in a column.
+    // For example, if numVar=3:
+    // x y z
+    // T T T
+    // T T F
+    // T F T
+    // T F F
+    // F T T
+    // F T F
+    // F F T
+    // F F F
+    // For the first column, numConsecutiveTF = 4, then 2 for the second column, 
+    // and 1 for the third column.
+    size_t numConsecutiveTF = total / 2;
+    for (Node n : literals)
+    {
+      Node not_n = n.notNode();
+
+      // loc tracks which row/cube we're on 
+      size_t loc = 0;
+      for (size_t z = 0; z < total / numConsecutiveTF; ++z)
+      {
+        t = !t;
+        for (size_t j = 0; j < numConsecutiveTF; ++j)
+        {
+          resultNodeLists[loc].push_back(t ? n : not_n);
+          ++loc;
+        }
+      }
+
+      numConsecutiveTF = numConsecutiveTF / 2;
+    }
+    for (const std::vector<TNode>& row : resultNodeLists)
+    {
+      Node conj = NodeManager::currentNM()->mkAnd(row);
+      emitCube(conj);
+    }
+    return stopPartitioning();
+  }
+  return TrustNode::null();
+}
+
 TrustNode PartitionGenerator::check(Theory::Effort e)
 {
   if ((options().parallel.partitionCheck == options::CheckMode::FULL
@@ -161,7 +255,9 @@ TrustNode PartitionGenerator::check(Theory::Effort e)
 
   switch (options().parallel.partitionStrategy)
   {
-    case options::PartitionMode::REVISED: return makeRevisedPartitions();
+    case options::PartitionMode::DECISION_TRAIL: return makeFullTrailPartitions(); 
+    case options::PartitionMode::STRICT_CUBE: return makeRevisedPartitions(true); 
+    case options::PartitionMode::REVISED: return makeRevisedPartitions(false);
     default: return TrustNode::null();
   }
 }

diff --git a/src/theory/partition_generator.h b/src/theory/partition_generator.h
index dfe8533bcb154381f94a7a9df41c64b30a064c70..43c1c1118c301e92c84c606155216ba8e36cfcf0 100644 (file)
--- a/src/theory/partition_generator.h
+++ b/src/theory/partition_generator.h
@@ -57,9 +57,21 @@ class PartitionGenerator : protected EnvObj
 
   /**
    * Partition using the "revised" strategy, which emits cubes such as C1, C2,
-   * C3, !C1 & !C2 & !C3
+   * C3, !C1 & !C2 & !C3. If strict is set to true, a modified version of this emits
+   * "strict cubes:" C1, !C1 & C2, !C1 & !C2 & C3, !C1 & !C2 & !C3.
    */
-  TrustNode makeRevisedPartitions();
+  TrustNode makeRevisedPartitions(bool strict);
+
+  /**
+   * Partition by taking a list of literals and emitting mutually exclusive cubes 
+   * that resemble entries in a truth table: 
+   * C1: { l1, !l2}
+   * C2: { l1,  l2} 
+   * C3: {!l1, !l2} 
+   * C4: {!l1,  l2} 
+   */
+  TrustNode makeFullTrailPartitions();
+
 
   /**
    * Generate a lemma that is the negation of toBlock which ultimately blocks