Synchronizing the CNF and IS hypotheses

lib/comp_hypothesis.cpp

@@ -562,6 +562,20 @@ SUBool::CompHypothesis::FindEmpoweringQuery(AbsCheckerSAT &checker)
    return checker.FindEmpowering(mHypothesis, cl2lit, mImplSystemProvider);
 }
 
+const SUBool::EncISProvider &
+SUBool::CompHypothesis::ImplSystemProvider()
+{
+   if (!mImplSystemInitialized)
+   {
+      logs.TLog(3) << "[CompHypothesis::FindEmpoweringQuery] Initializing "
+                      "the implication system"
+                   << std::endl;
+      mImplSystemProvider->Cleanup(mHypothesis);
+      mImplSystemInitialized = true;
+   }
+   return *mImplSystemProvider;
+}
+
 std::optional<SUBool::Clause>
 SUBool::CompHypothesis::FindEmpowering(
     AbsCheckerSAT &checker, bool level_minimize)

lib/comp_hypothesis.h

@@ -63,7 +63,7 @@ namespace SUBool
       std::vector<Literal> mBackbone{};
       CNFCompressor mCompressor{};
       std::shared_ptr<EncISProvider> mImplSystemProvider{};
-      bool mImplSystemInitialized{false};
+      std::atomic<bool> mImplSystemInitialized{false};
       IMPL_SYSTEM_REBUILD mImplSystemRebuild{IMPL_SYSTEM_REBUILD::CLAUSE_ADDED};
 
       std::unordered_set<Clause> mLearnedCache{};
@@ -148,6 +148,7 @@ namespace SUBool
       {
          return mCompressor;
       }
+      const EncISProvider &ImplSystemProvider();
 
       std::optional<Clause> NextLearnedClause();
       bool HasLearnedClause() const;

lib/pclearncomp.cpp

@@ -86,6 +86,12 @@ const SUBool::EnumAnnotation<
             {PCLearnComp::CANDIDATES_FROM_NEGATIVE_POLICY::NONE, "none",
                 "No candidates are extracted from the clause added to the "
                 "hypothesis"}, //
+            {PCLearnComp::CANDIDATES_FROM_NEGATIVE_POLICY::SYNCHRONIZE,
+                "synchronize",
+                "Like none, but before the construction of the encoding of PC, "
+                "consider the bodies in the implicational system associated "
+                "with the CNF and try to reconsider them as candidates on "
+                "negative examples."}, //
             {PCLearnComp::CANDIDATES_FROM_NEGATIVE_POLICY::SEMANTIC, "semantic",
                 "Semantic closure is computed and compared with the forward "
                 "chaining closure with respect to the implicational system"}, //
@@ -102,7 +108,9 @@ SUBool::PCLearnComp::PCLearnComp(CNF cnf, Config conf)
    mConf.preprocess = AbsComp::PMRemoveMinimize(mConf.preprocess);
    mPCCheckerSAT.Init(mConf.EncoderConfig(), true, mConf.timeouts);
    mPCCheckerSAT.SetSolverType(mConf.solver_type);
-   if (mPCCheckerSAT.RequiresImplSystem())
+   if (mPCCheckerSAT.RequiresImplSystem()
+       || mConf.candidates_from_negative_policy
+              == CANDIDATES_FROM_NEGATIVE_POLICY::SYNCHRONIZE)
    {
       mHypothesis.SetImplSystemProvider(
           conf.use_cnf_hypothesis_for_empowerment
@@ -424,28 +432,6 @@ SUBool::PCLearnComp::InitialCandidatesBodyMinimal()
    return std::move(is).Implications();
 }
 
-std::vector<SUBool::LitImpl>
-SUBool::PCLearnComp::ComputeClosuresOfNegatives(std::vector<LitImpl> negatives)
-{
-   if (!State(COMPUTE_CLOSURES_OF_NEGATIVES))
-   {
-      return negatives;
-   }
-   CPUTime cpu_time;
-   bool nonprime = false;
-   for (auto &neg : negatives)
-   {
-      nonprime = UpdateClosureWithMinimizing(neg) || nonprime;
-   }
-   if (nonprime)
-   {
-      negatives = RemoveDuplicitiesInNegatives(std::move(negatives));
-   }
-   logs.TLog(3) << "Finished computing closures of negatives, time=" << cpu_time
-                << std::endl;
-   return negatives;
-}
-
 std::vector<SUBool::LitImpl>
 SUBool::PCLearnComp::RemoveDuplicitiesInNegatives(
     std::vector<LitImpl> negatives)
@@ -702,7 +688,32 @@ SUBool::PCLearnComp::UpdateCandidate(const LitImpl &neg)
 bool
 SUBool::PCLearnComp::CheckPC()
 {
-   return CheckPCRandomly() && CheckPCWithSAT();
+   return CheckPCRandomly() && !SynchronizeHypothesis() && CheckPCWithSAT();
+}
+
+bool
+SUBool::PCLearnComp::SynchronizeHypothesis()
+{
+   if (!mHypothesisSyncNeeded)
+   {
+      return false;
+   }
+   mHypothesisSyncNeeded = false;
+   const auto &is_provider = mHypothesis.ImplSystemProvider();
+   const auto &is = is_provider.OneProveImplSystem();
+   bool found_candidate{false};
+   for (const auto &impl : is)
+   {
+      auto i_cached_closure = CachedClosure(impl.Body());
+      if (i_cached_closure != mClosureCache.end())
+      {
+         continue;
+      }
+      found_candidate = true;
+      ++mCandidatesFromNegativesCount;
+      mCandidatesWithoutClosure.push(LitImpl{impl.Body(), {}, true});
+   }
+   return found_candidate;
 }
 
 bool
@@ -1003,6 +1014,9 @@ SUBool::PCLearnComp::AddCandidatesForAddedClause(const Clause &clause)
    {
    case CANDIDATES_FROM_NEGATIVE_POLICY::NONE:
       return 0;
+   case CANDIDATES_FROM_NEGATIVE_POLICY::SYNCHRONIZE:
+      mHypothesisSyncNeeded = true;
+      return 0;
    case CANDIDATES_FROM_NEGATIVE_POLICY::SEMANTIC:
       return AddNegativesForImplicate(clause, false);
    case CANDIDATES_FROM_NEGATIVE_POLICY::UNITPROP:

lib/pclearncomp.h

@@ -49,12 +49,15 @@ namespace SUBool
 
       enum class CANDIDATES_FROM_NEGATIVE_POLICY
       {
-         NONE,     // No candidates extracted from the clause added to the
-                   // hypothesis
-         SEMANTIC, // Semantic closure is used to determine if the set of
-                   // literals is a negative example
-         UNITPROP  // Only UP closures of the hypothesis with the implication
-                   // system are compared
+         NONE,        // No candidates extracted from the clause added to the
+                      // hypothesis
+         SYNCHRONIZE, // Regularly synchronize the CNF hypothesis with the IS
+                      // hypothesis by reconsidering the bodies of the
+                      // implicational system associated with the CNF hypothesis
+         SEMANTIC,    // Semantic closure is used to determine if the set of
+                      // literals is a negative example
+         UNITPROP     // Only UP closures of the hypothesis with the implication
+                      // system are compared
       };
       static const EnumAnnotation<CANDIDATES_FROM_NEGATIVE_POLICY>
           kCandidatesFromNegativePolicyAnnotation;
@@ -106,6 +109,8 @@ namespace SUBool
       PCCheckerSAT mPCCheckerSAT;
       unsigned mPCCheckRandomBudget;
 
+      bool mHypothesisSyncNeeded{false};
+
       // Statistical data
       double mTimeTillTheLastSATEqCheck{0.0};
       double mTimeOfLastSATEqCheck{0.0};
@@ -141,8 +146,6 @@ namespace SUBool
       std::vector<LitImpl> InitialCandidatesGDBasis();
       std::vector<LitImpl> InitialCandidatesBodyMinimal();
 
-      std::vector<LitImpl> ComputeClosuresOfNegatives(
-          std::vector<LitImpl> negatives);
       void SortNegatives();
       std::optional<LitImpl> NextNegativeExample();
       bool Refine(const LitImpl &e);
@@ -173,6 +176,7 @@ namespace SUBool
       bool CheckPCWithSAT();
       void CheckRandomImplicate(const Clause &c);
       void CheckRandomBody(std::vector<Literal> literals);
+      bool SynchronizeHypothesis(); // true, if any example added to any queue
 
       // Returns the number of added negatives
       unsigned AddNegativesForImplicate(