Option for the policy of extracting candidates from clauses added to the

hypothesis given a negative example added to the implicational system

lib/assign.cpp

@@ -22,14 +22,13 @@ SUBool::Assignment::Assignment(size_t n_values, double probability_true)
    }
 }
 
-SUBool::PartialAssignment::PartialAssignment(size_t n_values,
-                                             double probability_false,
-                                             double probability_true)
+SUBool::PartialAssignment::PartialAssignment(
+    size_t n_values, double probability_false, double probability_true)
     : BaseClass(n_values, PartialValue::FALSE)
 {
    // double pf = probability_false + probability_true;
    std::discrete_distribution dd({1.0 - probability_false - probability_true,
-                                  probability_false, probability_true});
+       probability_false, probability_true});
    for (auto &&v : *this)
    {
       v = static_cast<PartialValue>(dd(sub_rand));
@@ -68,8 +67,8 @@ SUBool::PartialAssignment::PartialAssignment(const Assignment &alpha)
    }
 }
 
-SUBool::PartialAssignment::PartialAssignment(size_t n_values,
-                                             std::vector<Literal> literals)
+SUBool::PartialAssignment::PartialAssignment(
+    size_t n_values, std::vector<Literal> literals)
     : PartialAssignment(n_values, PartialValue::UNDEF)
 {
    for (const auto &lit : literals)
@@ -129,11 +128,11 @@ SUBool::pv_and(PartialValue a, PartialValue b)
    case PartialValue::FALSE:
       return PartialValue::FALSE;
    case PartialValue::UNDEF:
-      return (b == PartialValue::FALSE ? PartialValue::FALSE
-                                       : PartialValue::UNDEF);
+      return (
+          b == PartialValue::FALSE ? PartialValue::FALSE : PartialValue::UNDEF);
    default:
-      throw BadParameterException("operator&(PartialValue, PartialValue)",
-                                  "unknown value of a");
+      throw BadParameterException(
+          "operator&(PartialValue, PartialValue)", "unknown value of a");
    }
 }
 
@@ -147,11 +146,11 @@ SUBool::pv_or(PartialValue a, PartialValue b)
    case PartialValue::FALSE:
       return b;
    case PartialValue::UNDEF:
-      return (b == PartialValue::TRUE ? PartialValue::TRUE
-                                      : PartialValue::UNDEF);
+      return (
+          b == PartialValue::TRUE ? PartialValue::TRUE : PartialValue::UNDEF);
    default:
-      throw BadParameterException("operator|(PartialValue, PartialValue)",
-                                  "unknown value of a");
+      throw BadParameterException(
+          "operator|(PartialValue, PartialValue)", "unknown value of a");
    }
 }
 
@@ -175,10 +174,25 @@ SUBool::next_value(PartialValue val)
    case PartialValue::FALSE:
       return PartialValue::TRUE;
    case PartialValue::TRUE:
-      throw OverflowException("next_value(PartialValue)",
-                              "TRUE cannot be increased");
+      throw OverflowException(
+          "next_value(PartialValue)", "TRUE cannot be increased");
    default:
-      throw InvariantFailedException("next_value(PartialValue)",
-                                     "Invalid value");
+      throw InvariantFailedException(
+          "next_value(PartialValue)", "Invalid value");
    }
 }
+
+bool
+SUBool::pa_equal(const PartialAssignment &alpha, const PartialAssignment &beta)
+{
+   size_t m = std::max(alpha.Size(), beta.Size());
+   for (size_t i = 0; i < m; ++i)
+   {
+      if (alpha.XValue(i) != beta.XValue(i))
+      {
+         return false;
+      }
+   }
+   return true;
+}
+

lib/assign.h

@@ -214,8 +214,18 @@ namespace SUBool
       void SetLiteralsNegated(InputIterator begin, InputIterator end);
       template <class InputIterator>
       void UnsetLiterals(InputIterator begin, InputIterator end);
+
+      PartialValue
+      XValue(size_t index) const
+      {
+         return index < Size() ? (*this)[index] : PartialValue::UNDEF;
+      }
    };
 
+   // Differs from the comparison operators in that if the lengths do not agree,
+   // then the shorter assignment is considered to be padded with undefs.
+   bool pa_equal(const PartialAssignment &alpha, const PartialAssignment &beta);
+
    std::ostream &operator<<(std::ostream &out, const PartialValue &v);
 
    PartialValue pv_negate(PartialValue pv);

lib/comp_hypothesis.cpp

@@ -208,7 +208,7 @@ SUBool::CompHypothesis::Safe() const
 }
 
 std::optional<SUBool::PartialAssignment>
-SUBool::CompHypothesis::PropagateUP(const PartialAssignment &alpha)
+SUBool::CompHypothesis::PropagateUP(const PartialAssignment &alpha) const
 {
    std::lock_guard<SharedMutex> lock(mMutex);
    return mOneProveHyp.Propagate(alpha);
@@ -221,12 +221,19 @@ SUBool::CompHypothesis::TheRightCNF() const
 }
 
 std::optional<SUBool::PartialAssignment>
-SUBool::CompHypothesis::PropagateAllSAT(const PartialAssignment &alpha) // const
+SUBool::CompHypothesis::PropagateAllSAT(const PartialAssignment &alpha) const
 {
    std::lock_guard lock(mMutex);
    return mSemPropagator.Propagate(alpha);
 }
 
+bool
+SUBool::CompHypothesis::UPClosed(const PartialAssignment &alpha) const
+{
+   std::lock_guard lock(mMutex);
+   return mOneProveHyp.Closed(alpha);
+}
+
 std::optional<SUBool::PartialAssignment>
 SUBool::CompHypothesis::Backbones()
 {
@@ -414,14 +421,14 @@ SUBool::CompHypothesis::PropagateUPBackbones()
 }
 
 std::optional<std::vector<SUBool::Literal>>
-SUBool::CompHypothesis::AllEmpoweredLiterals(const Clause &clause)
+SUBool::CompHypothesis::AllEmpoweredLiterals(const Clause &clause) const
 {
    std::lock_guard<SharedMutex> lock(mMutex);
    return mOneProveHyp.AllEmpoweredLiterals(clause);
 }
 
 std::optional<SUBool::Literal>
-SUBool::CompHypothesis::EmpoweredLiteral(const Clause &clause)
+SUBool::CompHypothesis::EmpoweredLiteral(const Clause &clause) const
 {
    std::lock_guard<SharedMutex> lock(mMutex);
    return mOneProveHyp.EmpoweredLiteral(clause);

lib/comp_hypothesis.h

@@ -125,19 +125,20 @@ namespace SUBool
       // Initializes mBacbone and mCompressor, return false if the formula is
       // unsatisfiable.
       bool PropagateBackbones();
-      // Like PropagaBackbones, but only propagates literals which can be
+      // Like PropagateBackbones, but only propagates literals which can be
       // derived by unit propagation
       bool PropagateUPBackbones();
       void SetSafe();
       bool Safe() const;
 
       std::optional<PartialAssignment> PropagateUP(
-          const PartialAssignment &alpha);
+          const PartialAssignment &alpha) const;
+      bool UPClosed(const PartialAssignment &alpha) const;
       std::optional<PartialAssignment> PropagateAllSAT(
-          const PartialAssignment &alpha); // const;
+          const PartialAssignment &alpha) const;
       std::optional<std::vector<Literal>> AllEmpoweredLiterals(
-          const Clause &clause);
-      std::optional<Literal> EmpoweredLiteral(const Clause &clause);
+          const Clause &clause) const;
+      std::optional<Literal> EmpoweredLiteral(const Clause &clause) const;
       bool MinimizeHypothesis();     // true if minimization executed
       bool MinimizeRepresentation(); // true if minimization executed
       std::vector<ClauseWithEmpowered> MinimizeReprWithCollectingEmpowered(

lib/empower2.h

@@ -35,7 +35,7 @@ namespace SUBool
       UnitPropagatorM mUP;
 
       void Reprocess(const unsigned clause_size,
-                     std::queue<UnitPropagatorM::const_iterator> &q);
+          std::queue<UnitPropagatorM::const_iterator> &q);
 
     public:
       OneProveM() : mUP() {}
@@ -69,24 +69,29 @@ namespace SUBool
       bool IsOneProvable(const Clause &clause) const;
       bool IsEmpowering(const Clause &clause) const;
       // Returns an empty clause if the clause is not 1-provable
-      Clause MinOneProvableSubClause(const Clause &clause,
-                                     unsigned ignore_var = 0) const;
-      std::optional<std::vector<Literal>>
-      AllEmpoweredLiterals(const Clause &clause) const;
+      Clause MinOneProvableSubClause(
+          const Clause &clause, unsigned ignore_var = 0) const;
+      std::optional<std::vector<Literal>> AllEmpoweredLiterals(
+          const Clause &clause) const;
       std::optional<Literal> EmpoweredLiteral(const Clause &clause) const;
-      std::optional<std::vector<Literal>>
-      CollectEmpoweredLiterals(const Clause &clause, bool collect_all) const;
+      std::optional<std::vector<Literal>> CollectEmpoweredLiterals(
+          const Clause &clause, bool collect_all) const;
       std::optional<PartialAssignment>
       Propagate(const PartialAssignment &alpha) const
       {
          return mUP.Propagate(alpha);
       }
+      bool
+      Closed(const PartialAssignment &alpha) const
+      {
+         return mUP.Closed(alpha);
+      }
 
       void MinimizeFull(size_t log_step = 0);
-      void AddWithIncrementalMinimization(CNF cnf, bool reprocessing,
-                                          size_t log_step = 0);
-      std::vector<ClauseWithEmpowered>
-      MinimizeWithCollectingEmpowered(bool collect_all, size_t log_step = 0);
+      void AddWithIncrementalMinimization(
+          CNF cnf, bool reprocessing, size_t log_step = 0);
+      std::vector<ClauseWithEmpowered> MinimizeWithCollectingEmpowered(
+          bool collect_all, size_t log_step = 0);
    };
 
 } // namespace SUBool

lib/pc_opt.cpp

@@ -87,7 +87,9 @@ SUBool::PCLearnCompOptions::PCLearnCompOptions()
 bool
 SUBool::PCLearnCompOptions::GetValues()
 {
-   return mInitialNegativesOption.GetValue(mInitialNegatives);
+   return mInitialNegativesOption.GetValue(mInitialNegatives)
+          && mCandidatesFromNegativePolicyOption.GetValue(
+              mCandidatesFromNegativePolicy);
 }
 
 SUBool::PCCompPreprocessOptions::PCCompPreprocessOptions()

lib/pclearncomp.cpp

@@ -858,6 +858,20 @@ SUBool::PCLearnComp::AddCandidateIfNegative(const LitImpl &candidate)
    return true;
 }
 
+bool
+SUBool::PCLearnComp::AddCandidateIfNotUPClosed(const std::vector<Literal> &body)
+{
+   auto closure = mNegatives.Closure(body);
+   assert(!Clause(closure).Trivial());
+   if (mHypothesis.UPClosed(
+           PartialAssignment(mHypothesis.MaxVariable(), closure)))
+   {
+      return false;
+   }
+   mCandidatesWithoutClosure.push(LitImpl(body, {}, true));
+   return true;
+}
+
 bool
 SUBool::PCLearnComp::Refine(const LitImpl &e)
 {
@@ -1000,8 +1014,23 @@ unsigned
 SUBool::PCLearnComp::AddCandidatesForAddedClauseUnitProp(
     const Clause &clause [[maybe_unused]])
 {
-   throw NotImplementedException(
-       "PCLearnComp::AddCandidatesForAddedClauseUnitProp", "");
+   logs.TLog(3) << "Adding candidates using unit propagation for clause "
+                << mHypothesis.Compressor().UncompressClause(clause)
+                << std::endl;
+   unsigned cnt = 0;
+   for (const auto &lit : clause)
+   {
+      std::vector<Literal> body;
+      std::remove_copy(
+          clause.begin(), clause.end(), std::back_inserter(body), lit);
+      std::for_each(
+          body.begin(), body.end(), [](Literal &lit) { lit.Negate(); });
+      if (AddCandidateIfNotUPClosed(body))
+      {
+         ++cnt;
+      }
+   }
+   return cnt;
 }
 
 void

lib/pclearncomp.h

@@ -181,6 +181,7 @@ namespace SUBool
       bool AddCandidateIfNegative(const LitImpl &candidate);
       unsigned AddCandidatesForAddedClause(const Clause &clause);
       unsigned AddCandidatesForAddedClauseUnitProp(const Clause &clause);
+      bool AddCandidateIfNotUPClosed(const std::vector<Literal> &body);
 
       NECache::const_iterator CachedClosure(
           const std::vector<Literal> &body) const;

lib/unitprop2.h

@@ -115,7 +115,7 @@ namespace SUBool
 
       void UpdateMaxVariable(unsigned max_var);
       static void MoveWatch(const Literal &lit, const_iterator_list &watch_list,
-                            size_t src, size_t target);
+          size_t src, size_t target);
 
     public:
       UnitPropagatorM()
@@ -165,6 +165,13 @@ namespace SUBool
       {
          return mContradictory;
       }
+
+      bool
+      Closed(const PartialAssignment &alpha) const
+      {
+         return Consistent(alpha) && pa_equal(mValues, alpha);
+      }
+
       unsigned
       MaxVariable() const
       {
@@ -210,8 +217,8 @@ namespace SUBool
       bool EnableClause(const_iterator i_clause);
    };
 
-   std::ostream &operator<<(std::ostream &out,
-                            const UnitPropagatorM::ClauseInfo &ci);
+   std::ostream &operator<<(
+       std::ostream &out, const UnitPropagatorM::ClauseInfo &ci);
 } // namespace SUBool
 
 #endif

lib/up_scc_unary.cpp

@@ -185,8 +185,8 @@ SUBool::UPSCCUnary::FireClauses(Context &ctx, const LitImpl &impl,
     unsigned impl_index, std::vector<Clause> &clauses) const
 {
    auto fv = InitFireVariables(ctx, impl, impl_index);
-   logs.TLog(3) << "Main scc index of implication " << impl << " is "
-                << fv.main_scc << std::endl;
+   // logs.TLog(3) << "Main scc index of implication " << impl << " is "
+   //<< fv.main_scc << std::endl;
    if (impl.Body().size() > 1)
    {
       FireVarDefinition(ctx, impl, fv, clauses);