From: Amalee Wilson Date: Mon, 2 May 2022 23:42:10 +0000 (-0700) Subject: Add strict-cube and decision-trail partitioning strategies (#8651) X-Git-Tag: cvc5-1.0.1~187 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4617392aad80921f49c4eb3f62a06e8ad5c710ab;p=cvc5.git 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 9d5c288b9..5ebbc1a1d 100644 --- 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 8b5ee94e1..f829fd1a0 100644 --- 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 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 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 literals = collectDecisionLiterals(); + uint64_t numVar = static_cast(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 > 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& 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 dfe8533bc..43c1c1118 100644 --- 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