Add assumption-based unsat cores. (#6427)

This PR adds an assumption-based unsat cores option. If enabled it will
disable proof logging in the SAT solver and adds input assertions as
assumptions to the SAT solver. When an unsat core is requested we
extract the unsat core in terms of the unsat assumption in the SAT
solver. Assumption-based unsat cores use the proof infrastructure to map
the input assumptions back to the original assertions.

diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h
index 88e344b8a9ae905661dc2f1c761c45d9a38a25d1..432ff1f899f69f8ae935255a7bb35832da0fe73d 100644 (file)
--- a/src/expr/proof_rule.h
+++ b/src/expr/proof_rule.h
@@ -247,6 +247,14 @@ enum class PfRule : uint32_t
   // where F is an equality (= t t') that holds by a form of substitution that
   // could not be determined by the TrustSubstitutionMap.
   TRUST_SUBS_MAP,
+  // ========= SAT Refutation for assumption-based unsat cores
+  // Children: (P1, ..., Pn)
+  // Arguments: none
+  // ---------------------
+  // Conclusion: false
+  // Note: P1, ..., Pn correspond to the unsat core determined by the SAT
+  // solver.
+  SAT_REFUTATION,
 
   //================================================= Boolean rules
   // ======== Resolution

diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index 40274489b77d104258ff6f7bbd06c2e9ddf63d35..19f1bff97884c7da21c55063aa4ecda26f05ceea 100644 (file)
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -484,8 +484,8 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id)
       // If a literal is false at 0 level (both sat and user level) we also
       // ignore it, unless we are tracking the SAT solver's reasoning
       if (value(ps[i]) == l_False) {
-        if (!options::unsatCores() && !isProofEnabled()
-            && level(var(ps[i])) == 0 && user_level(var(ps[i])) == 0)
+        if (!options::unsatCores() && !needProof() && level(var(ps[i])) == 0
+            && user_level(var(ps[i])) == 0)
         {
           continue;
         }
@@ -527,7 +527,7 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id)
 
       // If all false, we're in conflict
       if (ps.size() == falseLiteralsCount) {
-        if (options::unsatCores() || isProofEnabled())
+        if (options::unsatCores() || needProof())
         {
           // Take care of false units here; otherwise, we need to
           // construct the clause below to give to the proof manager
@@ -549,7 +549,7 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id)
               ProofManager::getSatProof()->finalizeProof(
                   cvc5::Minisat::CRef_Lazy);
             }
-            if (isProofEnabled())
+            if (needProof())
             {
               d_pfManager->finalizeProof(ps[0], true);
             }
@@ -574,7 +574,7 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id)
         clauses_persistent.push(cr);
         attachClause(cr);
 
-        if (options::unsatCores() || isProofEnabled())
+        if (options::unsatCores() || needProof())
         {
           if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
           {
@@ -596,7 +596,7 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id)
             {
               ProofManager::getSatProof()->finalizeProof(cr);
             }
-            if (isProofEnabled())
+            if (needProof())
             {
               d_pfManager->finalizeProof(ca[cr], true);
             }
@@ -633,7 +633,7 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id)
             // already been registered, as the ProofCnfStream will not register
             // them and as they are not the result of propagation will be left
             // hanging in assumptions accumulator
-            if (isProofEnabled())
+            if (needProof())
             {
               d_pfManager->registerSatLitAssumption(ps[0]);
             }
@@ -654,7 +654,7 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id)
                 ProofManager::getSatProof()->finalizeProof(confl);
               }
             }
-            if (isProofEnabled())
+            if (needProof())
             {
               if (ca[confl].size() == 1)
               {
@@ -755,7 +755,7 @@ void Solver::removeClause(CRef cr) {
       // Solver::reason, if it appears in a resolution chain built lazily we
       // will be unable to do so after the step below. Thus we eagerly justify
       // this propagation here.
-      if (isProofEnabled())
+      if (needProof())
       {
         Trace("pf::sat")
             << "Solver::removeClause: eagerly compute propagation of " << c[0]
@@ -1001,7 +1001,7 @@ int Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel)
   {
     ProofManager::getSatProof()->startResChain(confl);
     }
-    if (isProofEnabled())
+    if (needProof())
     {
       d_pfManager->startResChain(ca[confl]);
     }
@@ -1066,7 +1066,7 @@ int Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel)
               {
                 ProofManager::getSatProof()->resolveOutUnit(q);
               }
-              if (isProofEnabled())
+              if (needProof())
               {
                 d_pfManager->addResolutionStep(q);
               }
@@ -1088,7 +1088,7 @@ int Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel)
           {
             ProofManager::getSatProof()->addResolutionStep(p, confl, sign(p));
           }
-          if (isProofEnabled())
+          if (needProof())
           {
             d_pfManager->addResolutionStep(ca[confl], p);
           }
@@ -1129,7 +1129,7 @@ int Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel)
                 {
                   ProofManager::getSatProof()->storeLitRedundant(out_learnt[i]);
                 }
-                if (isProofEnabled())
+                if (needProof())
                 {
                   Debug("newproof::sat")
                       << "Solver::analyze: redundant lit "
@@ -1677,7 +1677,7 @@ lbool Solver::search(int nof_conflicts)
         {
           ProofManager::getSatProof()->finalizeProof(confl);
         }
-        if (isProofEnabled())
+        if (needProof())
         {
           if (confl == CRef_Lazy)
           {
@@ -1704,7 +1704,7 @@ lbool Solver::search(int nof_conflicts)
         {
           ProofManager::getSatProof()->endResChain(learnt_clause[0]);
         }
-        if (isProofEnabled())
+        if (needProof())
         {
           d_pfManager->endResChain(learnt_clause[0]);
         }
@@ -1723,7 +1723,7 @@ lbool Solver::search(int nof_conflicts)
           ClauseId id = ProofManager::getSatProof()->registerClause(cr, LEARNT);
           ProofManager::getSatProof()->endResChain(id);
         }
-        if (isProofEnabled())
+        if (needProof())
         {
           d_pfManager->endResChain(ca[cr]);
         }
@@ -2219,7 +2219,7 @@ CRef Solver::updateLemmas() {
 
       // If it's an empty lemma, we have a conflict at zero level
       if (lemma.size() == 0) {
-        Assert(!options::unsatCores() && !isProofEnabled());
+        Assert(!options::unsatCores() && !needProof());
         conflict = CRef_Lazy;
         backtrackLevel = 0;
         Debug("minisat::lemmas") << "Solver::updateLemmas(): found empty clause" << std::endl;
@@ -2249,7 +2249,7 @@ CRef Solver::updateLemmas() {
   // Last index in the trail
   int backtrack_index = trail.size();
 
-  Assert(!options::unsatCores() || isProofEnabled()
+  Assert(!options::unsatCores() || needProof()
          || lemmas.size() == (int)lemmas_cnf_assertion.size());
 
   // Attach all the clauses and enqueue all the propagations
@@ -2320,7 +2320,7 @@ CRef Solver::updateLemmas() {
             {
               ProofManager::getSatProof()->storeUnitConflict(lemma[0], LEARNT);
             }
-            if (isProofEnabled())
+            if (needProof())
             {
               d_pfManager->storeUnitConflict(lemma[0]);
             }
@@ -2334,7 +2334,7 @@ CRef Solver::updateLemmas() {
     }
   }
 
-  Assert(!options::unsatCores() || isProofEnabled()
+  Assert(!options::unsatCores() || needProof()
          || lemmas.size() == (int)lemmas_cnf_assertion.size());
   // Clear the lemmas
   lemmas.clear();
@@ -2400,5 +2400,11 @@ std::shared_ptr<ProofNode> Solver::getProof()
 
 bool Solver::isProofEnabled() const { return d_pfManager != nullptr; }
 
+bool Solver::needProof() const
+{
+  return isProofEnabled()
+         && options::unsatCoresMode() != options::UnsatCoresMode::ASSUMPTIONS;
+}
+
 }  // namespace Minisat
 }  // namespace cvc5

diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h
index cd3f38c9efee3937becfcb86b582b0f755f68522..a9ee25c113d518c78fe124e0e2b2b38ae98fba93 100644 (file)
--- a/src/prop/minisat/core/Solver.h
+++ b/src/prop/minisat/core/Solver.h
@@ -160,6 +160,13 @@ public:
  /** Is proof enabled? */
  bool isProofEnabled() const;
 
+ /**
+  * Checks whether we need a proof.
+  *
+  * SAT proofs are not required for assumption-based unsat cores.
+  */
+ bool needProof() const;
+
  // Less than for literals in a lemma
  struct lemma_lt
  {

diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp
index 813292a21ffac4409cb59bce5e948c7f23bad0d0..611416dbc6ccd0f2a22345d748ba333b98e69a17 100644 (file)
--- a/src/prop/minisat/minisat.cpp
+++ b/src/prop/minisat/minisat.cpp
@@ -32,7 +32,7 @@ namespace prop {
 //// DPllMinisatSatSolver
 
 MinisatSatSolver::MinisatSatSolver(StatisticsRegistry& registry)
-    : d_minisat(NULL), d_context(NULL), d_statistics(registry)
+    : d_minisat(NULL), d_context(NULL), d_assumptions(), d_statistics(registry)
 {}
 
 MinisatSatSolver::~MinisatSatSolver()
@@ -193,6 +193,40 @@ SatValue MinisatSatSolver::solve() {
   return result;
 }
 
+SatValue MinisatSatSolver::solve(const std::vector<SatLiteral>& assumptions)
+{
+  setupOptions();
+  d_minisat->budgetOff();
+
+  d_assumptions.clear();
+  Minisat::vec<Minisat::Lit> assumps;
+
+  for (const SatLiteral& lit : assumptions)
+  {
+    Minisat::Lit mlit = toMinisatLit(lit);
+    assumps.push(mlit);
+    d_assumptions.emplace(lit);
+  }
+
+  SatValue result = toSatLiteralValue(d_minisat->solve(assumps));
+  d_minisat->clearInterrupt();
+  return result;
+}
+
+void MinisatSatSolver::getUnsatAssumptions(
+    std::vector<SatLiteral>& unsat_assumptions)
+{
+  for (size_t i = 0, size = d_minisat->d_conflict.size(); i < size; ++i)
+  {
+    Minisat::Lit mlit = d_minisat->d_conflict[i];
+    SatLiteral lit = ~toSatLiteral(mlit);
+    if (d_assumptions.find(lit) != d_assumptions.end())
+    {
+      unsat_assumptions.push_back(lit);
+    }
+  }
+}
+
 bool MinisatSatSolver::ok() const {
   return d_minisat->okay();
 }

diff --git a/src/prop/minisat/minisat.h b/src/prop/minisat/minisat.h
index 42588080dcb2287dd47258895d35b728d71306e4..74b7ab74910c2f506355c2a5a322b93c7a4238f6 100644 (file)
--- a/src/prop/minisat/minisat.h
+++ b/src/prop/minisat/minisat.h
@@ -58,6 +58,8 @@ class MinisatSatSolver : public CDCLTSatSolverInterface
 
   SatValue solve() override;
   SatValue solve(long unsigned int&) override;
+  SatValue solve(const std::vector<SatLiteral>& assumptions) override;
+  void getUnsatAssumptions(std::vector<SatLiteral>& unsat_assumptions) override;
 
   bool ok() const override;
 
@@ -100,6 +102,14 @@ class MinisatSatSolver : public CDCLTSatSolverInterface
   /** Context we will be using to synchronize the sat solver */
   context::Context* d_context;
 
+  /**
+   * Stores assumptions passed via last solve() call.
+   *
+   * It is used in getUnsatAssumptions() to determine which of the literals in
+   * the final conflict clause are assumptions.
+   */
+  std::unordered_set<SatLiteral, SatLiteralHashFunction> d_assumptions;
+
   void setupOptions();
 
   class Statistics {

diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index c4d929d357829b67c5839d2b0fcf5f4c1b95dff0..23377cb0c8dc7716ab156c03a5522b96712603a3 100644 (file)
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -82,7 +82,8 @@ PropEngine::PropEngine(TheoryEngine* te,
       d_ppm(nullptr),
       d_interrupted(false),
       d_resourceManager(rm),
-      d_outMgr(outMgr)
+      d_outMgr(outMgr),
+      d_assumptions(userContext)
 {
   Debug("prop") << "Constructing the PropEngine" << std::endl;
 
@@ -262,7 +263,18 @@ void PropEngine::assertInternal(
   // Assert as (possibly) removable
   if (isProofEnabled())
   {
-    d_pfCnfStream->convertAndAssert(node, negated, removable, pg);
+    if (options::unsatCoresMode() == options::UnsatCoresMode::ASSUMPTIONS
+        && input)
+    {
+      Assert(!negated);
+      d_pfCnfStream->ensureLiteral(node);
+      d_assumptions.push_back(node);
+    }
+    else
+    {
+      d_pfCnfStream->convertAndAssert(node, negated, removable, pg);
+    }
+
     // if input, register the assertion
     if (input)
     {
@@ -274,6 +286,7 @@ void PropEngine::assertInternal(
     d_cnfStream->convertAndAssert(node, removable, negated, input);
   }
 }
+
 void PropEngine::assertLemmasInternal(
     theory::TrustNode trn,
     const std::vector<theory::TrustNode>& ppLemmas,
@@ -358,7 +371,20 @@ Result PropEngine::checkSat() {
   d_interrupted = false;
 
   // Check the problem
-  SatValue result = d_satSolver->solve();
+  SatValue result;
+  if (d_assumptions.size() == 0)
+  {
+    result = d_satSolver->solve();
+  }
+  else
+  {
+    std::vector<SatLiteral> assumptions;
+    for (const Node& node : d_assumptions)
+    {
+      assumptions.push_back(d_cnfStream->getLiteral(node));
+    }
+    result = d_satSolver->solve(assumptions);
+  }
 
   if( result == SAT_VALUE_UNKNOWN ) {
 
@@ -628,5 +654,27 @@ std::shared_ptr<ProofNode> PropEngine::getProof()
 
 bool PropEngine::isProofEnabled() const { return d_pfCnfStream != nullptr; }
 
+void PropEngine::getUnsatCore(std::vector<Node>& core)
+{
+  Assert(options::unsatCoresMode() == options::UnsatCoresMode::ASSUMPTIONS);
+  std::vector<SatLiteral> unsat_assumptions;
+  d_satSolver->getUnsatAssumptions(unsat_assumptions);
+  for (const SatLiteral& lit : unsat_assumptions)
+  {
+    core.push_back(d_cnfStream->getNode(lit));
+  }
+}
+
+std::shared_ptr<ProofNode> PropEngine::getRefutation()
+{
+  Assert(options::unsatCoresMode() == options::UnsatCoresMode::ASSUMPTIONS);
+  std::vector<Node> core;
+  getUnsatCore(core);
+  CDProof cdp(d_pnm);
+  Node fnode = NodeManager::currentNM()->mkConst(false);
+  cdp.addStep(fnode, PfRule::SAT_REFUTATION, core, {});
+  return cdp.getProofFor(fnode);
+}
+
 }  // namespace prop
 }  // namespace cvc5

diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index a0496a525be622f38b3eb38e76e8e06e194bb52a..6812a65499fb27b9185b400892e95b05f389ea5f 100644 (file)
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -286,6 +286,13 @@ class PropEngine
 
   /** Is proof enabled? */
   bool isProofEnabled() const;
+
+  /** Retrieve unsat core from SAT solver for assumption-based unsat cores. */
+  void getUnsatCore(std::vector<Node>& core);
+
+  /** Return the prop engine proof for assumption-based unsat cores. */
+  std::shared_ptr<ProofNode> getRefutation();
+
  private:
   /** Dump out the satisfying assignment (after SAT result) */
   void printSatisfyingAssignment();
@@ -370,6 +377,12 @@ class PropEngine
 
   /** Reference to the output manager of the smt engine */
   OutputManager& d_outMgr;
+
+  /**
+   * Stores assumptions added via assertInternal() if assumption-based unsat
+   * cores are enabled.
+   */
+  context::CDList<Node> d_assumptions;
 };
 
 }  // namespace prop

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 8e8a1e062c48618d39602e4e7ad5ef2fe6ae39c4..09b3d64abbe237b01d410837328378c290f484d8 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1419,9 +1419,19 @@ UnsatCore SmtEngine::getUnsatCoreInternal()
   // generate with new proofs
   PropEngine* pe = getPropEngine();
   Assert(pe != nullptr);
-  Assert(pe->getProof() != nullptr);
-  std::shared_ptr<ProofNode> pfn = d_pfManager->getFinalProof(
-      pe->getProof(), *d_asserts, *d_definedFunctions);
+
+  std::shared_ptr<ProofNode> pepf;
+  if (options::unsatCoresMode() == options::UnsatCoresMode::ASSUMPTIONS)
+  {
+    pepf = pe->getRefutation();
+  }
+  else
+  {
+    pepf = pe->getProof();
+  }
+  Assert(pepf != nullptr);
+  std::shared_ptr<ProofNode> pfn =
+      d_pfManager->getFinalProof(pepf, *d_asserts, *d_definedFunctions);
   std::vector<Node> core;
   d_ucManager->getUnsatCore(pfn, *d_asserts, core);
   return UnsatCore(core);

diff --git a/src/theory/booleans/proof_checker.cpp b/src/theory/booleans/proof_checker.cpp
index 256ccedce978284ff0cde685fd8655e695ec0074..8b2967fe6d7fed645d17552ca66ade6a8d41de01 100644 (file)
--- a/src/theory/booleans/proof_checker.cpp
+++ b/src/theory/booleans/proof_checker.cpp
@@ -74,6 +74,7 @@ void BoolProofRuleChecker::registerTo(ProofChecker* pc)
   pc->registerChecker(PfRule::CNF_ITE_NEG1, this);
   pc->registerChecker(PfRule::CNF_ITE_NEG2, this);
   pc->registerChecker(PfRule::CNF_ITE_NEG3, this);
+  pc->registerTrustedChecker(PfRule::SAT_REFUTATION, this, 1);
 }
 
 Node BoolProofRuleChecker::checkInternal(PfRule id,
@@ -950,6 +951,11 @@ Node BoolProofRuleChecker::checkInternal(PfRule id,
         args[0], args[0][1].notNode(), args[0][2].notNode()};
     return NodeManager::currentNM()->mkNode(kind::OR, disjuncts);
   }
+  if (id == PfRule::SAT_REFUTATION)
+  {
+    Assert(args.empty());
+    return NodeManager::currentNM()->mkConst(false);
+  }
   // no rule
   return Node::null();
 }