[proof-new] Fixing resolution proof checker (#5262)

Previously the binary resolution checker was:

- Checking applications in which for a pivot (not l) the literal (not l) would be eliminated from the first clause and l from the second because double negation was handled implicitly. Now whether the binary resolution is such that the pivot is removed as is from the first clause and negated from the second, or the other way around, is marked via an argument.
- Not producing false the remaining set of literals after resolution was empty.

This commit also updates the informal description of the rule accordingly, as well as to clarify the behavior when the pivot does not occur properly in the clauses (in which case the rule application corresponds to weakening).

Co-authored-by: Gereon Kremer <gereon.kremer@cs.rwth-aachen.de>

diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h
index 9c955d067f62bb825b2dc77cde9c0694e8d5af43..e24d5c5225c996a1b1d29b80231eb39f9839a208 100644 (file)
--- a/src/expr/proof_rule.h
+++ b/src/expr/proof_rule.h
@@ -246,14 +246,28 @@ enum class PfRule : uint32_t
   //================================================= Boolean rules
   // ======== Resolution
   // Children:
-  //  (P1:(or F_1 ... F_i-1 F_i F_i+1 ... F_n),
-  //   P2:(or G_1 ... G_j-1 G_j G_j+1 ... G_m))
-  //
-  // Arguments: (F_i)
+  //  (P1:C1, P2:C2)
+  // Arguments: (id, L)
   // ---------------------
-  // Conclusion: (or F_1 ... F_i-1 F_i+1 ... F_n G_1 ... G_j-1 G_j+1 ... G_m)
+  // Conclusion: C
   // where
-  //   G_j = (not F_i)
+  //   - C1 and C2 are nodes viewed as clauses, i.e., either an OR node with
+  //     each children viewed as a literal or a node viewed as a literal. Note
+  //     that an OR node could also be a literal.
+  //   - id is either true or false
+  //   - L is the pivot of the resolution, which occurs as is (resp. under a
+  //     NOT) in C1 and negatively (as is) in C2 if id = true (id = false).
+  //   C is a clause resulting from collecting all the literals in C1, minus the
+  //   first occurrence of the pivot or its negation, and C2, minus the first
+  //   occurrence of the pivot or its negation, according to the policy above.
+  //   If the resulting clause has a single literal, that literal itself is the
+  //   result; if it has no literals, then the result is false; otherwise it's
+  //   an OR node of the resulting literals.
+  //
+  //   Note that it may be the case that the pivot does not occur in the
+  //   clauses. In this case the rule is not unsound, but it does not correspond
+  //   to resolution but rather to a weakening of the clause that did not have a
+  //   literal eliminated.
   RESOLUTION,
   // ======== Chain Resolution
   // Children: (P1:(or F_{1,1} ... F_{1,n1}), ..., Pm:(or F_{m,1} ... F_{m,nm}))

diff --git a/src/prop/proof_cnf_stream.cpp b/src/prop/proof_cnf_stream.cpp
index c7dd288afdb4473bd45510fccc592a5f340220b8..b2d33a61d92b0917d72f7c31753a080b7405c37e 100644 (file)
--- a/src/prop/proof_cnf_stream.cpp
+++ b/src/prop/proof_cnf_stream.cpp
@@ -548,7 +548,7 @@ void ProofCnfStream::convertPropagation(theory::TrustNode trn)
     d_proof.addStep(clauseExp,
                     PfRule::RESOLUTION,
                     {clauseAndNeg, clauseImpliesElim},
-                    {proven[0]});
+                    {nm->mkConst(true), proven[0]});
   }
   else
   {

diff --git a/src/theory/booleans/proof_checker.cpp b/src/theory/booleans/proof_checker.cpp
index 2f06995e3ad6544eec743879d7954acfcc223c69..3eb523ab5c670f1dd119c811dee97856b55b301c 100644 (file)
--- a/src/theory/booleans/proof_checker.cpp
+++ b/src/theory/booleans/proof_checker.cpp
@@ -80,21 +80,52 @@ Node BoolProofRuleChecker::checkInternal(PfRule id,
   if (id == PfRule::RESOLUTION)
   {
     Assert(children.size() == 2);
-    Assert(args.size() == 1);
+    Assert(args.size() == 2);
+    NodeManager* nm = NodeManager::currentNM();
     std::vector<Node> disjuncts;
+    Node pivots[2];
+    if (args[0] == nm->mkConst(true))
+    {
+      pivots[0] = args[1];
+      pivots[1] = args[1].notNode();
+    }
+    else
+    {
+      Assert(args[0] == nm->mkConst(false));
+      pivots[0] = args[1].notNode();
+      pivots[1] = args[1];
+    }
     for (unsigned i = 0; i < 2; ++i)
     {
-      // if first clause, eliminate pivot, otherwise its negation
-      Node elim = i == 0 ? args[0] : args[0].notNode();
-      for (unsigned j = 0, size = children[i].getNumChildren(); j < size; ++j)
+      // determine whether the clause is unit for effects of resolution, which
+      // is the case if it's not an OR node or it is an OR node but it is equal
+      // to the pivot
+      std::vector<Node> lits;
+      if (children[i].getKind() == kind::OR && pivots[i] != children[i])
       {
-        if (elim != children[i][j])
+        lits.insert(lits.end(), children[i].begin(), children[i].end());
+      }
+      else
+      {
+        lits.push_back(children[i]);
+      }
+      for (unsigned j = 0, size = lits.size(); j < size; ++j)
+      {
+        if (pivots[i] != lits[j])
         {
-          disjuncts.push_back(children[i][j]);
+          disjuncts.push_back(lits[j]);
+        }
+        else
+        {
+          // just eliminate first occurrence
+          pivots[i] = Node::null();
         }
       }
     }
-    return NodeManager::currentNM()->mkNode(kind::OR, disjuncts);
+    return disjuncts.empty()
+               ? nm->mkConst(false)
+               : disjuncts.size() == 1 ? disjuncts[0]
+                                       : nm->mkNode(kind::OR, disjuncts);
   }
   if (id == PfRule::FACTORING)
   {