From 2a397ba9a749839474b7fd209d909049a79f6bfc Mon Sep 17 00:00:00 2001 From: Amalee Wilson Date: Fri, 13 May 2022 13:26:51 -0700 Subject: [PATCH] Add heap-trail partitioning strategy, checks between partitions, and cubes with zero-level learned literals (#8703) These changes extend the partition generator to be able to do the following: Access the order_heap in MiniSat and make partitions from those literals. Specify a number of checks between partitions. This is relevant for only the revised and strict-cube strategies. Append zero-level learned literals to the partitions. --- src/api/cpp/cvc5_types.h | 4 +- src/options/parallel_options.toml | 20 ++++ src/prop/minisat/core/Solver.cc | 11 ++ src/prop/minisat/core/Solver.h | 7 ++ src/prop/minisat/minisat.cpp | 5 + src/prop/minisat/minisat.h | 4 + src/prop/prop_engine.cpp | 10 ++ src/prop/prop_engine.h | 13 +++ src/prop/sat_solver.h | 6 + src/prop/theory_proxy.cpp | 13 ++- src/prop/theory_proxy.h | 2 + src/prop/zero_level_learner.h | 4 +- src/theory/partition_generator.cpp | 181 +++++++++++++++++++++++------ src/theory/partition_generator.h | 54 ++++++--- 14 files changed, 282 insertions(+), 52 deletions(-) diff --git a/src/api/cpp/cvc5_types.h b/src/api/cpp/cvc5_types.h index 87944905d..36e030449 100644 --- a/src/api/cpp/cvc5_types.h +++ b/src/api/cpp/cvc5_types.h @@ -183,7 +183,9 @@ enum LearnedLitType */ CONSTANT_PROP, /** Any internal literal that does not fall into the above categories. */ - INTERNAL + INTERNAL, + /** Special case for when produce-learned-literals is not set. */ + UNKNOWN }; /** Writes a learned literal type to a stream. */ std::ostream& operator<<(std::ostream& out, LearnedLitType ltype); diff --git a/src/options/parallel_options.toml b/src/options/parallel_options.toml index 5ebbc1a1d..675110df0 100644 --- a/src/options/parallel_options.toml +++ b/src/options/parallel_options.toml @@ -17,6 +17,14 @@ name = "Parallel" default = "1" help = "number of standard or full effort checks until partitioning" +[[option]] + name = "checksBetweenPartitions" + category = "expert" + long = "checks-between-partitions=N" + type = "uint64_t" + default = "1" + help = "number of checks between partitions" + [[option]] name = "partitionConflictSize" category = "expert" @@ -43,6 +51,9 @@ name = "Parallel" [[option.mode.DECISION_TRAIL]] name = "decision-trail" help = "Creates mutually exclusive cubes from the decisions in the SAT solver." +[[option.mode.HEAP_TRAIL]] + name = "heap-trail" + help = "Creates mutually exclusive cubes from the order heap in the SAT solver." [[option]] name = "partitionCheck" @@ -69,3 +80,12 @@ name = "Parallel" default = "ManagedOut()" includes = ["", "options/managed_streams.h"] help = "set the output channel for writing partitions" + +[[option]] + name = "appendLearnedLiteralsToCubes" + category = "expert" + long = "append-learned-literals-to-cubes" + type = "bool" + default = "false" + help = "emit learned literals with the cubes" + diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index da1dd5582..ec1edceec 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -2244,5 +2244,16 @@ bool Solver::assertionLevelOnly() const && options().base.incrementalSolving; } +const std::vector Solver::getMiniSatOrderHeap() +{ + std::vector heapList; + for (size_t i = 0, hsize = order_heap.size(); i < hsize; ++i) + { + Node n = d_proxy->getNode(order_heap[i]); + heapList.push_back(n); + } + return heapList; +} + } // namespace Minisat } // namespace cvc5::internal diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h index 39369a78a..8a9a80343 100644 --- a/src/prop/minisat/core/Solver.h +++ b/src/prop/minisat/core/Solver.h @@ -288,8 +288,15 @@ public: bool b); // Declare if a variable should be eligible for // selection in the decision heuristic. + // Return the decision trail const vec& getMiniSatDecisions() { return trail; } + // Return the order_heap, which is a priority queue of variables ordered with + // respect to the variable activity. The order heap is made available here + // in order to make partitions based on the literals contained in the heap. + + const std::vector getMiniSatOrderHeap(); + // Read state: // lbool value(Var x) const; // The current value of a variable. diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp index 2d0680cc3..55eade3b3 100644 --- a/src/prop/minisat/minisat.cpp +++ b/src/prop/minisat/minisat.cpp @@ -278,6 +278,11 @@ std::vector MinisatSatSolver::getDecisions() const return decisions; } +std::vector MinisatSatSolver::getOrderHeap() const +{ + return d_minisat->getMiniSatOrderHeap(); +} + int32_t MinisatSatSolver::getDecisionLevel(SatVariable v) const { return d_minisat->level(v) + d_minisat->user_level(v); diff --git a/src/prop/minisat/minisat.h b/src/prop/minisat/minisat.h index cf37582f4..3be938a52 100644 --- a/src/prop/minisat/minisat.h +++ b/src/prop/minisat/minisat.h @@ -99,6 +99,10 @@ class MinisatSatSolver : public CDCLTSatSolverInterface, protected EnvObj */ std::vector getDecisions() const override; + /** Return the order heap. + */ + std::vector getOrderHeap() const override; + /** Return decision level at which `lit` was decided on. */ int32_t getDecisionLevel(SatVariable v) const override; diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 4ee596f6f..ca93843c2 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -341,6 +341,11 @@ std::vector PropEngine::getPropDecisions() const return decisions; } +std::vector PropEngine::getPropOrderHeap() const +{ + return d_satSolver->getOrderHeap(); +} + int32_t PropEngine::getDecisionLevel(Node lit) const { Assert(isSatLiteral(lit)); @@ -717,5 +722,10 @@ std::vector PropEngine::getLearnedZeroLevelLiteralsForRestart() const return d_theoryProxy->getLearnedZeroLevelLiteralsForRestart(); } +modes::LearnedLitType PropEngine::getLiteralType(const Node& lit) const +{ + return d_theoryProxy->getLiteralType(lit); +} + } // namespace prop } // namespace cvc5::internal diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index 5afb38716..ddf5ad724 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -158,6 +158,16 @@ class PropEngine : protected EnvObj */ std::vector getPropDecisions() const; + /** + * Get the order heap from the SAT solver. + * order_heap is a priority queue of variables ordered with + * respect to the variable activity. The order heap is made available here + * in order to make partitions based on the literals contained in the heap. + * + * @return List of Nodes from the SAT variables order heap. + */ + std::vector getPropOrderHeap() const; + /** * Return SAT context level at which `lit` was decided on. * @@ -317,6 +327,9 @@ class PropEngine : protected EnvObj /** Get the zero-level assertions that should be used on deep restart */ std::vector getLearnedZeroLevelLiteralsForRestart() const; + /** Get the literal type through the ZLL utilities */ + modes::LearnedLitType getLiteralType(const Node& lit) const; + private: /** Dump out the satisfying assignment (after SAT result) */ void printSatisfyingAssignment(); diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h index e9f509a80..9e54db2d2 100644 --- a/src/prop/sat_solver.h +++ b/src/prop/sat_solver.h @@ -148,6 +148,12 @@ class CDCLTSatSolverInterface : public SatSolver */ virtual std::vector getDecisions() const = 0; + /** + * Return the order heap of the SAT solver, which is a priority queueue + * of literals ordered with respect to variable activity. + */ + virtual std::vector getOrderHeap() const = 0; + /** * Return the current decision level of `lit`. */ diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp index ba47061b0..6c6c114ff 100644 --- a/src/prop/theory_proxy.cpp +++ b/src/prop/theory_proxy.cpp @@ -22,6 +22,7 @@ #include "expr/node_algorithm.h" #include "options/base_options.h" #include "options/decision_options.h" +#include "options/parallel_options.h" #include "options/smt_options.h" #include "prop/cnf_stream.h" #include "prop/prop_engine.h" @@ -56,7 +57,8 @@ TheoryProxy::TheoryProxy(Env& env, bool trackZeroLevel = options().smt.deepRestartMode != options::DeepRestartMode::NONE || isOutputOn(OutputTag::LEARNED_LITS) - || options().smt.produceLearnedLiterals; + || options().smt.produceLearnedLiterals + || options().parallel.computePartitions > 0; if (trackZeroLevel) { d_zll = std::make_unique(env, theoryEngine); @@ -345,6 +347,15 @@ std::vector TheoryProxy::getLearnedZeroLevelLiterals( return {}; } +modes::LearnedLitType TheoryProxy::getLiteralType(const Node& lit) const +{ + if (d_zll != nullptr) + { + return d_zll->computeLearnedLiteralType(lit); + } + return modes::LearnedLitType::UNKNOWN; +} + std::vector TheoryProxy::getLearnedZeroLevelLiteralsForRestart() const { if (d_zll != nullptr) diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h index a3b824799..b34673942 100644 --- a/src/prop/theory_proxy.h +++ b/src/prop/theory_proxy.h @@ -181,6 +181,8 @@ class TheoryProxy : protected EnvObj, public Registrar modes::LearnedLitType ltype) const; /** Get the zero-level assertions that should be used on deep restart */ std::vector getLearnedZeroLevelLiteralsForRestart() const; + /** Get literal type using ZLL utility */ + modes::LearnedLitType getLiteralType(const Node& lit) const; private: /** The prop engine we are using. */ diff --git a/src/prop/zero_level_learner.h b/src/prop/zero_level_learner.h index b5dbd7a88..dbcfeb30c 100644 --- a/src/prop/zero_level_learner.h +++ b/src/prop/zero_level_learner.h @@ -66,6 +66,8 @@ class ZeroLevelLearner : protected EnvObj modes::LearnedLitType ltype) const; /** Get the zero-level assertions that should be used on deep restart */ std::vector getLearnedZeroLevelLiteralsForRestart() const; + /** compute type for learned literal */ + modes::LearnedLitType computeLearnedLiteralType(const Node& lit); private: static void getAtoms(TNode a, @@ -73,8 +75,6 @@ class ZeroLevelLearner : protected EnvObj std::unordered_set& atoms); /** Process learned literal */ void processLearnedLiteral(const Node& lit, modes::LearnedLitType ltype); - /** compute type for learned literal */ - modes::LearnedLitType computeLearnedLiteralType(const Node& lit); /** is learnable based on the value of options */ bool isLearnable(modes::LearnedLitType ltype) const; /** get solved */ diff --git a/src/theory/partition_generator.cpp b/src/theory/partition_generator.cpp index f829fd1a0..de309ea5a 100644 --- a/src/theory/partition_generator.cpp +++ b/src/theory/partition_generator.cpp @@ -38,6 +38,7 @@ PartitionGenerator::PartitionGenerator(Env& env, : EnvObj(env), d_numPartitions(options().parallel.computePartitions), d_numChecks(0), + d_betweenChecks(0), d_numPartitionsSoFar(0) { d_valuation = std::make_unique(theoryEngine); @@ -50,33 +51,83 @@ PartitionGenerator::PartitionGenerator(Env& env, } } -std::vector PartitionGenerator::collectDecisionLiterals() +std::vector PartitionGenerator::collectLiterals(LiteralListType litType) { - std::vector literals; - std::vector decisionNodes = d_propEngine->getPropDecisions(); + std::vector filteredLiterals; + std::vector unfilteredLiterals; + + // Filter out the types of literals we don't want. // Make sure the literal does not have a boolean term or skolem in it. const std::unordered_set kinds = { kind::SKOLEM, kind::BOOLEAN_TERM_VARIABLE}; - for (const Node& n : decisionNodes) + switch (litType) { - Node originalN = SkolemManager::getOriginalForm(n); - - // If the literal is the not of some node, do the checks for the child - // of the not instead of the not itself. - Node original = originalN.getKind() == kind::NOT ? originalN[0] : originalN; - if (expr::hasSubtermKinds(kinds, original) - || !d_valuation->isSatLiteral(original) - || !d_valuation->isDecision(original) - || Theory::theoryOf(original) == THEORY_BOOL - || n.isConst()) + case DECISION: { - continue; + unfilteredLiterals = d_propEngine->getPropDecisions(); + break; } + case HEAP: + { + unfilteredLiterals = d_propEngine->getPropOrderHeap(); + break; + } + case ZLL: + { + unfilteredLiterals = d_propEngine->getLearnedZeroLevelLiterals( + modes::LearnedLitType::INPUT); + break; + } + default: return filteredLiterals; + } - literals.push_back(originalN); + if (litType == HEAP || litType == DECISION) + { + for (const Node& n : unfilteredLiterals) + { + Node originalN = SkolemManager::getOriginalForm(n); + modes::LearnedLitType nType = d_propEngine->getLiteralType(n); + + // If the literal is the not of some node, do the checks for the child + // of the not instead of the not itself. + Node original = originalN.getKind() == kind::NOT ? originalN[0] : originalN; + + if (expr::hasSubtermKinds(kinds, original) + || !d_valuation->isSatLiteral(original) + || Theory::theoryOf(original) == THEORY_BOOL + || n.isConst() + || nType != modes::LearnedLitType::INPUT + || !d_valuation->isDecision(original)) + { + continue; + } + filteredLiterals.push_back(originalN); + } } - return literals; + // else it must be zll + else + { + for (const Node& n : unfilteredLiterals) + { + Node originalN = SkolemManager::getOriginalForm(n); + + // If the literal is the not of some node, do the checks for the child + // of the not instead of the not itself. + Node original = originalN.getKind() == kind::NOT ? originalN[0] : originalN; + + if (expr::hasSubtermKinds(kinds, original) + || !d_valuation->isSatLiteral(original) + || Theory::theoryOf(original) == THEORY_BOOL + || n.isConst()) + { + continue; + } + filteredLiterals.push_back(originalN); + } + } + + return filteredLiterals; } void PartitionGenerator::emitCube(Node toEmit) @@ -106,12 +157,12 @@ TrustNode PartitionGenerator::stopPartitioning() const // C2 = l2_{1} & .... & l2_{d_conflictSize} // C3 = l3_{1} & .... & l3_{d_conflictSize} // C4 = !C1 & !C2 & !C3 -TrustNode PartitionGenerator::makeRevisedPartitions(bool strict) +TrustNode PartitionGenerator::makeRevisedPartitions(bool strict, bool emitZLL) { // If we're not at the last cube if (d_numPartitionsSoFar < d_numPartitions - 1) { - std::vector literals = collectDecisionLiterals(); + std::vector literals = collectLiterals(DECISION); // Make sure we have enough literals. // Conflict size can be set through options, but the default is log base 2 @@ -138,13 +189,29 @@ TrustNode PartitionGenerator::makeRevisedPartitions(bool strict) toEmit.push_back(c.notNode()); } toEmit.push_back(conj); - Node cube = NodeManager::currentNM()->mkAnd(toEmit); + Node strict_cube = NodeManager::currentNM()->mkAnd(toEmit); + d_strict_cubes.push_back(strict_cube); - emitCube(cube); + if (emitZLL) + { + // just increment and don't actually output the cube yet + d_numPartitionsSoFar++; + } + else + { + emitCube(strict_cube); + } } - else - { - emitCube(conj); + else { + if (emitZLL) + { + // just increment and don't actually output the cube yet + d_numPartitionsSoFar++; + } + else + { + emitCube(conj); + } } // Add to the list of cubes. d_cubes.push_back(conj); @@ -153,6 +220,21 @@ TrustNode PartitionGenerator::makeRevisedPartitions(bool strict) // At the last cube else { + if (emitZLL) + { + std::vector zllLiterals = d_propEngine->getLearnedZeroLevelLiterals( + modes::LearnedLitType::INPUT); + std::vector* cubes = strict ? &d_strict_cubes : &d_cubes; + + for (const auto& c : *cubes) + { + zllLiterals.push_back(c); + Node lemma = NodeManager::currentNM()->mkAnd(zllLiterals); + emitCube(lemma); + zllLiterals.pop_back(); + } + } + vector nots; for (const Node& c : d_cubes) { @@ -160,15 +242,24 @@ TrustNode PartitionGenerator::makeRevisedPartitions(bool strict) } Node lemma = NodeManager::currentNM()->mkAnd(nots); // Emit not(cube_one) and not(cube_two) and ... and not(cube_n-1) - emitCube(lemma); + if (emitZLL) + { + std::vector zllLiterals = d_propEngine->getLearnedZeroLevelLiterals( + modes::LearnedLitType::INPUT); + zllLiterals.push_back(lemma); + Node zllLemma = NodeManager::currentNM()->mkAnd(zllLiterals); + emitCube(zllLemma); + } + else { + emitCube(lemma); + } return stopPartitioning(); } } - -TrustNode PartitionGenerator::makeFullTrailPartitions() +TrustNode PartitionGenerator::makeFullTrailPartitions(LiteralListType litType, bool emitZLL) { - std::vector literals = collectDecisionLiterals(); + std::vector literals = collectLiterals(litType); uint64_t numVar = static_cast(log2(d_numPartitions)); if (literals.size() >= numVar) { @@ -187,7 +278,7 @@ TrustNode PartitionGenerator::makeFullTrailPartitions() size_t total = pow(2, numVar); // resultNodeLists is built column by column. - std::vector > resultNodeLists(total); + std::vector > resultNodeLists(total); // t is used to determine whether to push the node or its not_node. bool t = false; @@ -225,10 +316,19 @@ TrustNode PartitionGenerator::makeFullTrailPartitions() numConsecutiveTF = numConsecutiveTF / 2; } - for (const std::vector& row : resultNodeLists) + for (const std::vector& row : resultNodeLists) { Node conj = NodeManager::currentNM()->mkAnd(row); - emitCube(conj); + if (emitZLL) + { + std::vector zllLiterals = collectLiterals(ZLL); + zllLiterals.push_back(conj); + Node zllConj = NodeManager::currentNM()->mkAnd(zllLiterals); + emitCube(zllConj); + } + else { + emitCube(conj); + } } return stopPartitioning(); } @@ -247,17 +347,28 @@ TrustNode PartitionGenerator::check(Theory::Effort e) } d_numChecks = d_numChecks + 1; + d_betweenChecks = d_betweenChecks + 1; - if (d_numChecks < options().parallel.checksBeforePartitioning) + if (d_numChecks < options().parallel.checksBeforePartitioning || + d_betweenChecks < options().parallel.checksBetweenPartitions) { return TrustNode::null(); } + // Reset betweenChecks + d_betweenChecks = 0; + + bool emitZLL = options().parallel.appendLearnedLiteralsToCubes; switch (options().parallel.partitionStrategy) { - case options::PartitionMode::DECISION_TRAIL: return makeFullTrailPartitions(); - case options::PartitionMode::STRICT_CUBE: return makeRevisedPartitions(true); - case options::PartitionMode::REVISED: return makeRevisedPartitions(false); + case options::PartitionMode::HEAP_TRAIL: + return makeFullTrailPartitions(/*litType=*/HEAP, emitZLL); + case options::PartitionMode::DECISION_TRAIL: + return makeFullTrailPartitions(/*litType=*/DECISION, emitZLL); + case options::PartitionMode::STRICT_CUBE: + return makeRevisedPartitions(/*strict=*/true, emitZLL); + case options::PartitionMode::REVISED: + return makeRevisedPartitions(/*strict=*/false, emitZLL); default: return TrustNode::null(); } } diff --git a/src/theory/partition_generator.h b/src/theory/partition_generator.h index 43c1c1118..6e1a0c939 100644 --- a/src/theory/partition_generator.h +++ b/src/theory/partition_generator.h @@ -50,28 +50,43 @@ class PartitionGenerator : protected EnvObj TrustNode check(Theory::Effort e); private: + /* LiteralListType is used to specify where to pull literals from when calling + * collectLiterals. HEAP for the order_heap in the SAT solver, DECISION for + * the decision trail in the SAT solver, and ZLL for the zero-level learned + * literals. + */ + enum LiteralListType + { + HEAP, + DECISION, + ZLL + }; /** - * Print the cube to the specified output. + * Increment d_numPartitionsSoFar and print the cube to + * the output file specified by --write-partitions-to. */ void emitCube(Node toEmit); /** * Partition using the "revised" strategy, which emits cubes such as C1, C2, - * 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. + * 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. If + * emitZLL is set to true, then zero-level learned literals will be appended + * to the cubes. */ - TrustNode makeRevisedPartitions(bool strict); + TrustNode makeRevisedPartitions(bool strict, bool emitZLL); /** - * Partition by taking a list of literals and emitting mutually exclusive cubes - * that resemble entries in a truth table: + * 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} + * C2: { l1, l2} + * C3: {!l1, !l2} + * C4: {!l1, l2} + * If emitZLL is set to true, then zero-level learned literals will be + * appended to the cubes. */ - TrustNode makeFullTrailPartitions(); - + TrustNode makeFullTrailPartitions(LiteralListType litType, bool emitZLL); /** * Generate a lemma that is the negation of toBlock which ultimately blocks @@ -85,14 +100,17 @@ class PartitionGenerator : protected EnvObj TrustNode stopPartitioning() const; /** - * Get the list of decisions from the SAT solver + * Get a list of literals. + * litType specifies whether to pull from the decision trail in the sat solver, + * from the order heap in the sat solver, or from the zero level learned literals. */ - std::vector collectDecisionLiterals(); + std::vector collectLiterals(LiteralListType litType); /** * Returns the d_cubes, the cubes that have been created for partitioning the * original problem. */ + std::vector getPartitions() const { return d_cubes; } /** @@ -116,6 +134,11 @@ const uint64_t d_numPartitions; */ uint64_t d_numChecks; +/** + * Number of standard checks that have occured since the last partition that was emitted. + */ +uint64_t d_betweenChecks; + /** * The number of partitions that have been created. */ @@ -131,6 +154,11 @@ std::vector d_assertedLemmas; */ std::vector d_cubes; +/** + * List of the strict cubes that have been created. + */ +std::vector d_strict_cubes; + /** * Minimum number of literals required in the list of decisions for cubes to * be made. -- 2.30.2