Subsumption and Subsumption Resolution via SAT solving

.gitmodules

@@ -1,3 +1,6 @@
+[submodule "benchmark"]
+	path = benchmark
+	url = https://github.com/google/benchmark.git
 [submodule "z3"]
 	path = z3
 	url = https://github.com/Z3Prover/z3

CMakeLists.txt

@@ -385,7 +385,7 @@ source_group(indexing_source_files FILES ${VAMPIRE_INDEXING_SOURCES})
 set(VAMPIRE_INFERENCE_SOURCES
     Inferences/BackwardDemodulation.cpp
     Inferences/BackwardSubsumptionDemodulation.cpp
-    Inferences/BackwardSubsumptionResolution.cpp
+    Inferences/BackwardSubsumptionAndResolution.cpp
     Inferences/BinaryResolution.cpp
     Inferences/Condensation.cpp
     Inferences/DemodulationHelper.cpp
@@ -417,14 +417,13 @@ set(VAMPIRE_INFERENCE_SOURCES
     Inferences/GaussianVariableElimination.cpp
     Kernel/Rebalancing.cpp
     Kernel/Rebalancing/Inverters.cpp
-    Inferences/SLQueryBackwardSubsumption.cpp
     Inferences/Superposition.cpp
     Inferences/TautologyDeletionISE.cpp
     Inferences/TermAlgebraReasoning.cpp
     Inferences/URResolution.cpp
     Inferences/DefinitionIntroduction.cpp
     Inferences/BackwardDemodulation.hpp
-    Inferences/BackwardSubsumptionResolution.hpp
+    Inferences/BackwardSubsumptionAndResolution.hpp
     Inferences/BinaryResolution.hpp
     Inferences/Condensation.hpp
     Inferences/DemodulationHelper.hpp
@@ -454,7 +453,6 @@ set(VAMPIRE_INFERENCE_SOURCES
     Inferences/GaussianVariableElimination.hpp
     Kernel/Rebalancing.hpp
     Kernel/Rebalancing/Inverters.hpp
-    Inferences/SLQueryBackwardSubsumption.hpp
     Inferences/SubsumptionDemodulationHelper.cpp
     Inferences/Superposition.hpp
     Inferences/TautologyDeletionISE.hpp
@@ -687,6 +685,27 @@ set(VAMPIRE_CASC_SOURCES
     )
 source_group(casc_source_files FILES ${VAMPIRE_CASC_SOURCES})
 
+set(VAMPIRE_SAT_SUBSUMPTION_SOURCES
+    SATSubsumption/SATSubsumptionAndResolution.cpp
+    SATSubsumption/SATSubsumptionAndResolution.hpp
+
+    SATSubsumption/subsat/constraint.cpp
+    SATSubsumption/subsat/constraint.hpp
+    SATSubsumption/subsat/decision_queue.hpp
+    SATSubsumption/subsat/default_init_allocator.hpp
+    SATSubsumption/subsat/log.cpp
+    SATSubsumption/subsat/log.hpp
+    SATSubsumption/subsat/subsat.cpp
+    SATSubsumption/subsat/subsat.hpp
+    SATSubsumption/subsat/subsat_config.hpp
+    SATSubsumption/subsat/SubstitutionTheory.hpp
+    SATSubsumption/subsat/types.cpp
+    SATSubsumption/subsat/types.hpp
+    SATSubsumption/subsat/variable_domain_size.hpp
+    SATSubsumption/subsat/vector_map.hpp
+    )
+source_group(smt_subsumption_source_files FILES ${VAMPIRE_SAT_SUBSUMPTION_SOURCES})
+
 set(VAMPIRE_TESTING_SOURCES
     Test/UnitTesting.cpp
     Test/UnitTesting.hpp
@@ -731,6 +750,7 @@ set(UNIT_TESTS
     UnitTests/tOption.cpp
     UnitTests/tStack.cpp
     UnitTests/tSet.cpp
+    UnitTests/tSATSubsumptionResolution.cpp
     UnitTests/tDeque.cpp
     UnitTests/tTermAlgebra.cpp
     UnitTests/tFunctionDefinitionHandler.cpp
@@ -745,7 +765,6 @@ set(UNIT_TESTS_Z3
 source_group(unit_tests_z3 FILES ${UNIT_TESTS_Z3})
 
 
-
 # also include forwards.hpp?
 set(VAMPIRE_SOURCES
     ${VAMPIRE_DEBUG_SOURCES}
@@ -763,6 +782,7 @@ set(VAMPIRE_SOURCES
     ${VAMPIRE_SMTCOMP_SOURCES}
     ${VAMPIRE_MINISAT_SOURCES}
     ${VAMPIRE_CASC_SOURCES}
+    ${VAMPIRE_SAT_SUBSUMPTION_SOURCES}
     Forwards.hpp
     "${CMAKE_CURRENT_BINARY_DIR}/version.cpp"
     )
@@ -804,7 +824,7 @@ endif()
 ################################################################
 
 # find Z3 automatically!
-# normally this is just in /z3/build/, but this can be overridden
+# normally this is just in /z3/build/, but this can be overridden using -DZ3_DIR
 find_package(
   Z3
   CONFIG
@@ -852,6 +872,7 @@ else ()
   set(UNIT_TESTS ${UNIT_TESTS} ${UNIT_TESTS_Z3})
 endif()
 
+
 ################################################################
 # build objects
 ################################################################

Indexing/LiteralMiniIndex.cpp

@@ -32,6 +32,18 @@ bool LiteralMiniIndex::literalHeaderComparator(const Entry& e1, const Entry& e2)
   return e1._header<e2._header || ( e1._header==e2._header && e1._weight<e2._weight );
 }
 
+LiteralMiniIndex::LiteralMiniIndex()
+    : _cnt(0), _entries()
+{
+}
+
+void LiteralMiniIndex::init(Clause* cl)
+{
+  _cnt = cl->length();
+  _entries.ensure(cl->length()+1);
+  init(cl->literals());
+}
+
 LiteralMiniIndex::LiteralMiniIndex(Clause* cl)
 : _cnt(cl->length()), _entries(cl->length()+1)
 {

Indexing/LiteralMiniIndex.hpp

@@ -31,7 +31,10 @@ class LiteralMiniIndex
 {
 public:
   USE_ALLOCATOR(LiteralMiniIndex);
-
+
+  LiteralMiniIndex();
+  void init(Clause* cl);
+
   LiteralMiniIndex(Clause* cl);
   LiteralMiniIndex(Literal* const * lits, unsigned length);
 
@@ -53,6 +56,7 @@ class LiteralMiniIndex
   unsigned _cnt;
   DArray<Entry> _entries;
 
+  // TODO: name is misleading, because "base" means something different when next to "instance"  (IteratorBase would already be better)
   struct BaseIterator
   {
     BaseIterator(LiteralMiniIndex const& index, Literal* query, bool complementary)
@@ -102,11 +106,11 @@ class LiteralMiniIndex
 
 
   struct InstanceIterator
-  : BaseIterator
-  {
+      : BaseIterator {
     InstanceIterator(LiteralMiniIndex const& index, Literal* base, bool complementary)
-    : BaseIterator(index, base, complementary)
-    {}
+        : BaseIterator(index, base, complementary)
+    {
+    }
 
     bool hasNext()
     {
@@ -120,6 +124,23 @@ class LiteralMiniIndex
       }
       return false;
     }
+
+    template <class Binder>
+    bool hasNext(Binder& binder)
+    {
+      if (_ready) {
+        return true;
+      }
+      while (_curr->_header == _hdr) {
+        if (MatchingUtils::match(_query, _curr->_lit, _compl, binder)) {
+          _ready = true;
+          return true;
+        }
+        _curr++;
+      }
+      return false;
+    }
+
     Literal* next()
     {
       return BaseIterator::next();

Inferences/BackwardSubsumptionAndResolution.cpp

@@ -0,0 +1,204 @@
+/*
+ * This file is part of the source code of the software program
+ * Vampire. It is protected by applicable
+ * copyright laws.
+ *
+ * This source code is distributed under the licence found here
+ * https://vprover.github.io/license.html
+ * and in the source directory
+ */
+/**
+ * @file BackwardSubsumptionAndResolution.cpp
+ * Implements class BackwardSubsumptionAndResolution.
+ */
+
+/**
+ * The subsumption and subsumption resolution are described in the papers:
+ * - 2022: "First-Order Subsumption via SAT Solving." by Jakob Rath, Armin Biere and Laura Kovács
+ * - 2023: "SAT-Based Subsumption Resolution" by Robin Coutelier, Jakob Rath, Michael Rawson and
+ *         Laura Kovács
+ * - 2024: "SAT Solving for Variants of First-Order Subsumption" by Robin Coutelier, Jakob Rath,
+ *         Michael Rawson, Armin Biere and Laura Kovács
+ *
+ * In particular, this file implements the loop optimization described in 2023 and 2024.
+ */
+
+#include "Debug/RuntimeStatistics.hpp"
+
+#include "Lib/DArray.hpp"
+#include "Lib/DHSet.hpp"
+#include "Lib/Environment.hpp"
+#include "Lib/List.hpp"
+#include "Lib/Metaiterators.hpp"
+#include "Lib/VirtualIterator.hpp"
+
+#include "Kernel/Clause.hpp"
+#include "Kernel/Matcher.hpp"
+#include "Kernel/MLMatcher.hpp"
+#include "Kernel/Signature.hpp"
+#include "Kernel/Term.hpp"
+
+#include "Indexing/Index.hpp"
+#include "Indexing/LiteralIndex.hpp"
+#include "Indexing/IndexManager.hpp"
+
+#include "Saturation/SaturationAlgorithm.hpp"
+
+#include "Shell/Statistics.hpp"
+
+#include "ForwardSubsumptionAndResolution.hpp"
+#include "BackwardSubsumptionAndResolution.hpp"
+
+#include <chrono>
+
+namespace Inferences {
+
+using namespace Lib;
+using namespace Kernel;
+using namespace Indexing;
+using namespace Saturation;
+using namespace std::chrono;
+
+/***************************************************************/
+/*                        CORE METHODS                         */
+/***************************************************************/
+void BackwardSubsumptionAndResolution::attach(SaturationAlgorithm *salg)
+{
+  BackwardSimplificationEngine::attach(salg);
+  _bwIndex = static_cast<BackwardSubsumptionIndex *>(
+      _salg->getIndexManager()->request(BACKWARD_SUBSUMPTION_SUBST_TREE)
+  );
+}
+
+void BackwardSubsumptionAndResolution::detach()
+{
+  _bwIndex = 0;
+  _salg->getIndexManager()->release(BACKWARD_SUBSUMPTION_SUBST_TREE);
+  BackwardSimplificationEngine::detach();
+}
+
+
+void BackwardSubsumptionAndResolution::perform(Clause *cl,
+                                               BwSimplificationRecordIterator &simplifications)
+{
+  ASSERT_VALID(*cl)
+  ASS(_bwIndex)
+  simplifications = BwSimplificationRecordIterator::getEmpty();
+
+  if (!_subsumption && !_subsumptionResolution) {
+    return;
+  }
+
+  _checked.reset();
+
+  // The set of clauses that are subsumed by cl
+  static DHSet<Clause *> subsumedSet;
+  subsumedSet.reset();
+  // contains the list of simplifications found so far
+  List<BwSimplificationRecord> *simplificationBuffer = List<BwSimplificationRecord>::empty();
+
+  /********************************************************/
+  /*                      cl is UNIT                      */
+  /********************************************************/
+  // cl is a unit clause and will subsume all clauses that contain its literal
+  // and will be resolved with all clauses that contain its negation
+  if (cl->length() == 1) {
+    Literal *lit = (*cl)[0];
+    // Check for the subsumptions
+    if (_subsumption) {
+      /***************************************************/
+      /*            SUBSUMPTION UNIT CLAUSE              */
+      /***************************************************/
+      auto it = _bwIndex->getInstances(lit, false, false);
+      while (it.hasNext()) {
+        Clause *icl = it.next().data->clause;
+        if (!_checked.insert(icl))
+          continue;
+        subsumedSet.insert(icl);
+        List<BwSimplificationRecord>::push(BwSimplificationRecord(icl), simplificationBuffer);
+      }
+    }
+    if (_subsumptionResolution) {
+      /***************************************************/
+      /*      SUBSUMPTION RESOLUTION UNIT CLAUSE         */
+      /***************************************************/
+      auto it = _bwIndex->getInstances(lit, true, false);
+      while (it.hasNext()) {
+        auto res = it.next();
+        Clause *icl = res.data->clause;
+        if (subsumedSet.contains(icl) || !_checked.insert(icl))
+          continue;
+        Clause *conclusion = SATSubsumption::SATSubsumptionAndResolution::getSubsumptionResolutionConclusion(icl, res.data->literal, cl);
+        ASS(conclusion)
+        List<BwSimplificationRecord>::push(BwSimplificationRecord(icl, conclusion), simplificationBuffer);
+      }
+    }
+    goto finish;
+  }
+
+  if (_subsumptionByUnitsOnly && _srByUnitsOnly) {
+    ASS(!simplificationBuffer)
+    goto finish;
+  }
+
+  /*******************************************************/
+  /*       SUBSUMPTION & RESOLUTION MULTI-LITERAL        */
+  /*******************************************************/
+  if (!_subsumptionByUnitsOnly) {
+    for (unsigned i = 0; i < cl->length(); i++) {
+      Literal *lit = (*cl)[i];
+      // find the positively matched literals
+      auto it = _bwIndex->getInstances(lit, false, false);
+      while (it.hasNext()) {
+        Clause *icl = it.next().data->clause;
+        if (!_checked.insert(icl))
+          continue;
+        // check subsumption and setup subsumption resolution at the same time
+        bool checkS = _subsumption && !_subsumptionByUnitsOnly;
+        bool checkSR = _subsumptionResolution && !_srByUnitsOnly;
+        if (checkS) {
+          if (satSubs.checkSubsumption(cl, icl, checkSR)) {
+            List<BwSimplificationRecord>::push(BwSimplificationRecord(icl), simplificationBuffer);
+            subsumedSet.insert(icl);
+            continue;
+          }
+        }
+        if (checkSR) {
+          // check subsumption resolution
+          Clause *conclusion = satSubs.checkSubsumptionResolution(cl, icl, checkS); // use the previous setup only if subsumption was checked
+          if (conclusion)
+            List<BwSimplificationRecord>::push(BwSimplificationRecord(icl, conclusion), simplificationBuffer);
+        }
+      }
+    }
+  }
+
+  /*******************************************************/
+  /*       SUBSUMPTION RESOLUTION MULTI-LITERAL          */
+  /*******************************************************/
+  if (_subsumptionResolution && !_srByUnitsOnly) {
+    for (unsigned i = 0; i < cl->length(); i++) {
+      Literal *lit = (*cl)[i];
+      // find the negatively matched literals
+      auto it = _bwIndex->getInstances(lit, true, false);
+      while (it.hasNext()) {
+        Clause *icl = it.next().data->clause;
+        if (!_checked.insert(icl))
+          continue;
+        // check subsumption resolution
+        Clause *conclusion = satSubs.checkSubsumptionResolution(cl, icl, false);
+        if (conclusion)
+          List<BwSimplificationRecord>::push(BwSimplificationRecord(icl, conclusion), simplificationBuffer);
+      }
+    }
+  }
+
+finish:
+  if (simplificationBuffer) {
+    simplifications = pvi(List<BwSimplificationRecord>::Iterator(simplificationBuffer));
+  }
+
+  return;
+}
+
+} // namespace Inferences