Started UPSCCBinary encoding of one-provability

lib/up_impl_level.cpp

@@ -11,8 +11,7 @@
 #include "up_levels.h"
 
 SUBool::UPEncImplLevel::UPEncImplLevel(const Config &conf, const CNF &cnf,
-                                       const ClausesToLiterals &cl2lit,
-                                       VarStore &var_store,
+    const ClausesToLiterals &cl2lit, VarStore &var_store,
     const LitImplSystem &is)
     : UPEncoder(cnf, cl2lit, var_store), mImplSystem(is), mConf(conf)
 {
@@ -24,16 +23,6 @@ SUBool::UPEncImplLevel::MaxLevelBound() const
    return (mConf.use_bit_level ? BitSizeForLevel(0) : mCnf.MaxVariable());
 }
 
-unsigned
-SUBool::UPEncImplLevel::BitSizeForLevel(unsigned level) const
-{
-   if (level == 0)
-   {
-      level = mCnf.MaxVariable();
-   }
-   return static_cast<unsigned>(ceil(log2(static_cast<double>(level + 1))));
-}
-
 unsigned
 SUBool::UPEncImplLevel::NextLevelBound(unsigned level) const
 {
@@ -59,19 +48,18 @@ SUBool::UPEncImplLevel::NextLevelBound(unsigned level) const
 
 void
 SUBool::UPEncImplLevel::Encode(unsigned max_level,
-                               std::vector<unsigned> *inputs,
-                               std::vector<unsigned> *outputs,
+    std::vector<unsigned> *inputs, std::vector<unsigned> *outputs,
     std::vector<Clause> *clauses) const
 {
    if (inputs == nullptr)
    {
-      throw NullPointerException("UPEncLogarithmic::Encode",
-                                 "inputs == nullptr");
+      throw NullPointerException(
+          "UPEncLogarithmic::Encode", "inputs == nullptr");
    }
    if (outputs == nullptr)
    {
-      throw NullPointerException("UPEncLogarithmic::Encoder",
-                                 "outputs == nullptr");
+      throw NullPointerException(
+          "UPEncLogarithmic::Encoder", "outputs == nullptr");
    }
    unsigned max_level_bound = MaxLevelBound();
    if (max_level == 0 || max_level > max_level_bound)
@@ -133,8 +121,7 @@ SUBool::UPEncImplLevel::CountAddUnitsForEmptyBodies() const
 }
 
 std::vector<SUBool::Clause>
-SUBool::UPEncImplLevel::InitLitClauses(
-    const std::vector<unsigned> &inputs,
+SUBool::UPEncImplLevel::InitLitClauses(const std::vector<unsigned> &inputs,
     const std::vector<unsigned> &outputs) const
 {
    std::vector<Clause> lit_clauses(2 * mCnf.MaxVariable());
@@ -149,10 +136,8 @@ SUBool::UPEncImplLevel::InitLitClauses(
 void
 SUBool::UPEncImplLevel::AddImplication(unsigned impl_index,
     // const std::vector<unsigned> &inputs,
-                                       const std::vector<unsigned> &outputs,
-                                       UPLevels &level_vars,
-                                       std::vector<Clause> &lit_clauses,
-                                       bool &new_var,
+    const std::vector<unsigned> &outputs, UPLevels &level_vars,
+    std::vector<Clause> &lit_clauses, bool &new_var,
     std::vector<Clause> *clauses) const
 {
    const auto &impl = mImplSystem[impl_index];
@@ -180,8 +165,8 @@ SUBool::UPEncImplLevel::AddImplication(unsigned impl_index,
 
 SUBool::UPEncImplLevel::impl_var_t
 SUBool::UPEncImplLevel::InitImplVar(unsigned impl_index,
-                                    const std::vector<unsigned> &outputs,
-                                    UPLevels &level_vars, bool &new_var) const
+    const std::vector<unsigned> &outputs, UPLevels &level_vars,
+    bool &new_var) const
 {
    const auto &impl = mImplSystem[impl_index];
    if (impl.Body().size() == 1)
@@ -207,11 +192,8 @@ SUBool::UPEncImplLevel::InitImplVar(unsigned impl_index,
 
 void
 SUBool::UPEncImplLevel::AddImplToLitClause(const Literal &cons_lit,
-                                           unsigned impl_index,
-                                           impl_var_t impl_var,
-                                           UPLevels &level_vars,
-                                           Clause &lit_clause,
-                                           std::vector<Clause> *clauses) const
+    unsigned impl_index, impl_var_t impl_var, UPLevels &level_vars,
+    Clause &lit_clause, std::vector<Clause> *clauses) const
 {
    // In case of single literal in a body when the bodies are not merged and the
    // implications are not right irredundant, this could lead to repeating
@@ -243,26 +225,24 @@ SUBool::UPEncImplLevel::AddImplToLitClause(const Literal &cons_lit,
        level_vars.EncodeGT(cons_lit, impl_var.level_literal, clauses);
    mVarStore.NameStream() << "z_{" << impl_index << "}^{" << cons_lit << "}";
    auto and_var = mVarStore.NewVariable();
-   clauses->emplace_back(Literal(and_var, false),
-                         Literal(impl_var.aux_var, true));
+   clauses->emplace_back(
+       Literal(and_var, false), Literal(impl_var.aux_var, true));
    clauses->emplace_back(Literal(and_var, false), Literal(out_var, true));
    lit_clause.PushBack(Literal(and_var, true));
 }
 
 void
 SUBool::UPEncImplLevel::AddBodyLitClauses(impl_var_t impl_var,
-                                          const Literal &body_literal,
-                                          UPLevels &level_vars,
-                                          const std::vector<unsigned> &outputs,
-                                          std::vector<Clause> *clauses) const
+    const Literal &body_literal, UPLevels &level_vars,
+    const std::vector<unsigned> &outputs, std::vector<Clause> *clauses) const
 {
    clauses->emplace_back(Literal(impl_var.aux_var, false),
        Literal(outputs[body_literal.Index()], true));
    // TODO: Encode directly LE
    auto out_var =
        level_vars.EncodeGT(body_literal, impl_var.level_literal, clauses);
-   clauses->emplace_back(Literal(impl_var.aux_var, false),
-                         Literal(out_var, false));
+   clauses->emplace_back(
+       Literal(impl_var.aux_var, false), Literal(out_var, false));
 }
 
 void
@@ -272,8 +252,8 @@ SUBool::UPEncImplLevel::AssumptionsImplyConsequences(
 {
    for (unsigned lit_index = 0; lit_index < inputs.size(); ++lit_index)
    {
-      clauses->emplace_back(Literal(inputs[lit_index], false),
-                            Literal(outputs[lit_index], true));
+      clauses->emplace_back(
+          Literal(inputs[lit_index], false), Literal(outputs[lit_index], true));
    }
 }
 
@@ -304,8 +284,8 @@ SUBool::UPEncImplLevel::CountAssumptionsImplyConsequences() const
 SUBool::NFSize
 SUBool::UPEncImplLevel::CountAssumptionsHaveZeroLevel(unsigned bit_size) const
 {
-   return {0, 2 * mCnf.MaxVariable() * bit_size,
-           4 * bit_size * mCnf.MaxVariable()};
+   return {
+       0, 2 * mCnf.MaxVariable() * bit_size, 4 * bit_size * mCnf.MaxVariable()};
 }
 
 SUBool::NFSize
@@ -337,9 +317,8 @@ SUBool::UPEncImplLevel::EstimateSize(unsigned max_level) const
 }
 
 SUBool::NFSize
-SUBool::UPEncImplLevel::CountAddImplication(unsigned impl_index,
-                                            unsigned bit_size,
-                                            bool &new_var) const
+SUBool::UPEncImplLevel::CountAddImplication(
+    unsigned impl_index, unsigned bit_size, bool &new_var) const
 {
    NFSize s;
    const auto &impl = mImplSystem[impl_index];
@@ -359,8 +338,8 @@ SUBool::UPEncImplLevel::CountAddImplication(unsigned impl_index,
 }
 
 SUBool::NFSize
-SUBool::UPEncImplLevel::CountInitImplVar(unsigned impl_index, unsigned bit_size,
-                                         bool &new_var) const
+SUBool::UPEncImplLevel::CountInitImplVar(
+    unsigned impl_index, unsigned bit_size, bool &new_var) const
 {
    NFSize s;
    const auto &impl = mImplSystem[impl_index];

lib/up_impl_level.h

@@ -45,37 +45,32 @@ namespace SUBool
           std::vector<Clause> *clauses) const;
       void AddImplication(unsigned impl_index,
           // const std::vector<unsigned> &inputs,
-                          const std::vector<unsigned> &outputs,
-                          UPLevels &level_vars,
+          const std::vector<unsigned> &outputs, UPLevels &level_vars,
           std::vector<Clause> &lit_clauses, bool &new_var,
           std::vector<Clause> *clauses) const;
-      std::vector<Clause>
-      InitLitClauses(const std::vector<unsigned> &inputs,
+      std::vector<Clause> InitLitClauses(const std::vector<unsigned> &inputs,
           const std::vector<unsigned> &outputs) const;
       void AssumptionsImplyConsequences(const std::vector<unsigned> &inputs,
           const std::vector<unsigned> &outputs,
           std::vector<Clause> *clauses) const;
       void AssumptionsHaveZeroLevel(const std::vector<unsigned> &inputs,
-                                    const UPLevels &level_vars,
-                                    std::vector<Clause> *clauses) const;
+          const UPLevels &level_vars, std::vector<Clause> *clauses) const;
       void AddImplToLitClause(const Literal &cons_lit, unsigned impl_index,
-                              impl_var_t impl_var, UPLevels &level_vars,
-                              Clause &lit_clause,
+          impl_var_t impl_var, UPLevels &level_vars, Clause &lit_clause,
           std::vector<Clause> *clauses) const;
       impl_var_t InitImplVar(unsigned impl_index,
-                             const std::vector<unsigned> &outputs,
-                             UPLevels &level_vars, bool &new_var) const;
+          const std::vector<unsigned> &outputs, UPLevels &level_vars,
+          bool &new_var) const;
       void AddBodyLitClauses(impl_var_t impl_var, const Literal &body_literal,
-                             UPLevels &level_vars,
-                             const std::vector<unsigned> &outputs,
+          UPLevels &level_vars, const std::vector<unsigned> &outputs,
           std::vector<Clause> *clauses) const;
       NFSize CountAddUnitsForEmptyBodies() const;
-      NFSize CountAddImplication(unsigned impl_index, unsigned bit_size,
-                                 bool &new_var) const;
+      NFSize CountAddImplication(
+          unsigned impl_index, unsigned bit_size, bool &new_var) const;
       NFSize CountAssumptionsImplyConsequences() const;
       NFSize CountAssumptionsHaveZeroLevel(unsigned bit_size) const;
-      NFSize CountInitImplVar(unsigned impl_index, unsigned bit_size,
-                              bool &new_var) const;
+      NFSize CountInitImplVar(
+          unsigned impl_index, unsigned bit_size, bool &new_var) const;
 
     public:
       UPEncImplLevel(const Config &conf, const CNF &cnf,
@@ -89,5 +84,12 @@ namespace SUBool
       virtual unsigned NextLevelBound(unsigned level) const override;
    };
 } // namespace SUBool
+
+inline unsigned
+SUBool::UPEncImplLevel::BitSizeForLevel(unsigned level) const
+{
+   return bit_size_for_level(level, mCnf.MaxVariable());
+}
+
 #endif
 

lib/up_scc_binary.cpp

+/*
+ * Project SUBool
+ * Petr Kucera, 2021
+ */
+/**@file up_scc_binary.cpp
+ * Encoding based on SCCs of the graph of the implication system with levels
+ * encoded in binary.
+ */
+
+#include "up_scc_binary.h"
+
+void
+SUBool::UPSCCBinary::Encode(unsigned max_level, std::vector<unsigned> *inputs,
+    std::vector<unsigned> *outputs, std::vector<Clause> *clauses) const
+{
+   throw NotImplementedException("UPSCCBinary::Encode", "Not yet implemented");
+}
+
+auto
+SUBool::UPSCCBinary::EstimateSize(unsigned max_level) const -> NFSize
+{
+   throw NotImplementedException(
+       "UPSCCBinary::EstimateSize", "Not yet implemented");
+}
+
+unsigned
+SUBool::UPSCCBinary::MaxLevelBound() const
+{
+   return mSCCGraph.MaxEffSCCVarSize();
+   throw NotImplementedException(
+       "UPSCCBinary::MaxLevelBound", "Not yet implemented");
+}
+
+unsigned
+SUBool::UPSCCBinary::NextLevelBound(unsigned level) const
+{
+   throw NotImplementedException(
+       "UPSCCBinary::NextLevelBound", "Not yet implemented");
+}

lib/up_scc_binary.h

+/*
+ * Project SUBool
+ * Petr Kucera, 2021
+ */
+/**@file up_scc_binary.h
+ * Encoding based on SCCs of the graph of the implication system with levels
+ * encoded in binary.
+ */
+#ifndef __UP_SCC_BINARY_H
+#define __UP_SCC_BINARY_H
+
+#include "impl_system.h"
+#include "impl_system_graph.h"
+#include "upenc.h"
+
+namespace SUBool
+{
+   class UPSCCBinary : public UPEncoder
+   {
+    public:
+      struct Config
+      {
+         bool use_bit_level{true};
+
+         Config() {}
+
+         Config(bool ubl) : use_bit_level(ubl) {}
+
+         void Dump(const std::string &line_prefix, unsigned level) const;
+      };
+
+    private:
+      const LitImplSystem &mImplSystem;
+      const LitISGraph &mSCCGraph;
+      Config mConf;
+
+      unsigned BitSizeForLevel(unsigned level) const;
+
+    public:
+      UPSCCBinary(const Config &conf, const CNF &cnf,
+          const ClausesToLiterals &cl2lit, VarStore &var_store,
+          const LitImplSystem &is, const LitISGraph &scc_graph)
+          : UPEncoder(cnf, cl2lit, var_store), mImplSystem(is),
+            mSCCGraph(scc_graph), mConf(conf)
+      {
+      }
+
+      virtual void Encode(unsigned max_level, std::vector<unsigned> *inputs,
+          std::vector<unsigned> *outputs,
+          std::vector<Clause> *clauses) const override;
+      virtual NFSize EstimateSize(unsigned max_level) const override;
+      virtual unsigned MaxLevelBound() const override;
+      virtual unsigned NextLevelBound(unsigned level) const override;
+   };
+} // namespace SUBool
+
+inline unsigned
+SUBool::UPSCCBinary::BitSizeForLevel(unsigned level) const
+{
+   return bit_size_for_level(level, mCnf.MaxVariable());
+}
+
+#endif

lib/up_scc_unary.cpp

@@ -12,8 +12,7 @@
 
 void
 SUBool::UPSCCUnary::Encode(unsigned max_level, std::vector<unsigned> *inputs,
-                           std::vector<unsigned> *outputs,
-                           std::vector<Clause> *clauses) const
+    std::vector<unsigned> *outputs, std::vector<Clause> *clauses) const
 {
    if (inputs == nullptr)
    {
@@ -65,11 +64,9 @@ SUBool::UPSCCUnary::Encode(unsigned max_level, std::vector<unsigned> *inputs,
    }
 #endif
 
-   Context ctx{max_level,
-               InitVarInfo(max_level),
+   Context ctx{max_level, InitVarInfo(max_level),
        mVarStore.VarArray(mCnf.MaxVariable(), true, ":in(", ")"),
-               mVarStore.VarArray(mCnf.MaxVariable(), true, ":out(", ")"),
-               {}};
+       mVarStore.VarArray(mCnf.MaxVariable(), true, ":out(", ")"), {}};
    // std::cout << "After InitVarInfo" << std::endl;
    InitLevelClauses(ctx);
    /*for (const auto &lvars : ctx.vars)
@@ -130,8 +127,8 @@ auto
 SUBool::UPSCCUnary::EstimateSize(unsigned max_level [[maybe_unused]]) const
     -> NFSize
 {
-   throw NotImplementedException("UPSCCUnary::EstimateSize",
-                                 "Not yet implemented");
+   throw NotImplementedException(
+       "UPSCCUnary::EstimateSize", "Not yet implemented");
 }
 
 unsigned
@@ -163,8 +160,8 @@ SUBool::UPSCCUnary::AddClauses(Context &ctx, std::vector<Clause> &clauses) const
 }
 
 void
-SUBool::UPSCCUnary::MoveLevelClauses(Context &ctx,
-                                     std::vector<Clause> &clauses) const
+SUBool::UPSCCUnary::MoveLevelClauses(
+    Context &ctx, std::vector<Clause> &clauses) const
 {
    for (auto &var_info : ctx.vars)
    {
@@ -178,8 +175,7 @@ SUBool::UPSCCUnary::MoveLevelClauses(Context &ctx,
 
 void
 SUBool::UPSCCUnary::FireClauses(Context &ctx, const LitImpl &impl,
-                                unsigned impl_index,
-                                std::vector<Clause> &clauses) const
+    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 " <<
@@ -193,8 +189,7 @@ SUBool::UPSCCUnary::FireClauses(Context &ctx, const LitImpl &impl,
 
 void
 SUBool::UPSCCUnary::FireVarDefinition(Context &ctx, const LitImpl &impl,
-                                      const FireVariables &fv,
-                                      std::vector<Clause> &clauses) const
+    const FireVariables &fv, std::vector<Clause> &clauses) const
 {
    if (fv.simple_fire_var > 0)
    {
@@ -202,28 +197,26 @@ SUBool::UPSCCUnary::FireVarDefinition(Context &ctx, const LitImpl &impl,
    }
    for (unsigned l = 0; l < fv.level_fire_vars.size(); ++l)
    {
-      LevelFireVarDefinition(ctx, impl, fv.level_fire_vars[l], l, fv.main_scc,
-                             clauses);
+      LevelFireVarDefinition(
+          ctx, impl, fv.level_fire_vars[l], l, fv.main_scc, clauses);
    }
 }
 
 void
 SUBool::UPSCCUnary::SimpleFireVarDefinition(Context &ctx, const LitImpl &impl,
-                                            unsigned fire_var,
-                                            std::vector<Clause> &clauses) const
+    unsigned fire_var, std::vector<Clause> &clauses) const
 {
    auto fire_lit = make_negative_literal(fire_var);
    for (const auto &lit : impl.Body())
    {
-      clauses.emplace_back(fire_lit,
-                           make_positive_literal(ctx.outputs[lit.Index()]));
+      clauses.emplace_back(
+          fire_lit, make_positive_literal(ctx.outputs[lit.Index()]));
    }
 }
 
 void
 SUBool::UPSCCUnary::LevelFireVarDefinition(Context &ctx, const LitImpl &impl,
-                                           unsigned fire_var, unsigned level,
-                                           unsigned main_scc,
+    unsigned fire_var, unsigned level, unsigned main_scc,
     std::vector<Clause> &clauses) const
 {
    auto fire_lit = make_negative_literal(fire_var);
@@ -231,19 +224,18 @@ SUBool::UPSCCUnary::LevelFireVarDefinition(Context &ctx, const LitImpl &impl,
    {
       if (mSCCGraph.SCC(lit) == main_scc)
       {
-         clauses.emplace_back(
-             fire_lit,
+         clauses.emplace_back(fire_lit,
              make_positive_literal(ctx.vars[lit.Index()].level_vars[level]));
          continue;
       }
-      clauses.emplace_back(fire_lit,
-                           make_positive_literal(ctx.outputs[lit.Index()]));
+      clauses.emplace_back(
+          fire_lit, make_positive_literal(ctx.outputs[lit.Index()]));
    }
 }
 
 void
-SUBool::UPSCCUnary::AddFireVarsToLevelClauses(Context &ctx, const LitImpl &impl,
-                                              const FireVariables &fv) const
+SUBool::UPSCCUnary::AddFireVarsToLevelClauses(
+    Context &ctx, const LitImpl &impl, const FireVariables &fv) const
 {
    for (const auto &lit : impl.Cons())
    {
@@ -265,13 +257,12 @@ SUBool::UPSCCUnary::AddFireVarsToLevelClauses(Context &ctx, const LitImpl &impl,
 }
 
 void
-SUBool::UPSCCUnary::AddOutImplications(const Context &ctx,
-                                       std::vector<Clause> &clauses) const
+SUBool::UPSCCUnary::AddOutImplications(
+    const Context &ctx, std::vector<Clause> &clauses) const
 {
    for (unsigned lit_index = 0; lit_index < ctx.vars.size(); ++lit_index)
    {
-      clauses.emplace_back(
-          make_negative_literal(ctx.outputs[lit_index]),
+      clauses.emplace_back(make_negative_literal(ctx.outputs[lit_index]),
           make_positive_literal(ctx.vars[lit_index].level_vars.back()));
    }
 }
@@ -302,22 +293,20 @@ SUBool::UPSCCUnary::InspectImplSCC(Context &ctx, const LitImpl &impl) const
 
 auto
 SUBool::UPSCCUnary::InitFireVariables(Context &ctx, const LitImpl &impl,
-                                      unsigned impl_index) const
-    -> FireVariables
+    unsigned impl_index) const -> FireVariables
 {
    auto [main_scc, cons_out_of_main_scc] = InspectImplSCC(ctx, impl);
    if (impl.Body().size() == 1)
    {
       return UnifiedFireVariables(ctx, impl, main_scc, cons_out_of_main_scc);
    }
-   return NewFireVariables(impl_index, main_scc, cons_out_of_main_scc,
-                           ctx.max_level);
+   return NewFireVariables(
+       impl_index, main_scc, cons_out_of_main_scc, ctx.max_level);
 }
 
 auto
 SUBool::UPSCCUnary::NewFireVariables(unsigned impl_index, unsigned main_scc,
-                                     bool cons_out_of_main_scc,
-                                     unsigned max_level) const -> FireVariables
+    bool cons_out_of_main_scc, unsigned max_level) const -> FireVariables
 {
    FireVariables fv{main_scc, 0, {}};
    if (cons_out_of_main_scc)
@@ -339,9 +328,7 @@ SUBool::UPSCCUnary::NewFireVariables(unsigned impl_index, unsigned main_scc,
 
 auto
 SUBool::UPSCCUnary::UnifiedFireVariables(Context &ctx, const LitImpl &impl,
-                                         unsigned main_scc,
-                                         bool cons_out_of_main_scc) const
-    -> FireVariables
+    unsigned main_scc, bool cons_out_of_main_scc) const -> FireVariables
 {
    FireVariables fv{main_scc, 0, {}};
    unsigned lit_index = impl.Body().front().Index();

lib/upenc.h

@@ -26,8 +26,8 @@ namespace SUBool
       VarStore &mVarStore;
 
     public:
-      UPEncoder(const CNF &cnf, const ClausesToLiterals &cl2lit,
-                VarStore &var_store)
+      UPEncoder(
+          const CNF &cnf, const ClausesToLiterals &cl2lit, VarStore &var_store)
           : mCnf(cnf), mCl2Lit(cl2lit), mVarStore(var_store)
       {
       }
@@ -43,6 +43,17 @@ namespace SUBool
       // Returns 0 if there is no level beyond the given one
       virtual unsigned NextLevelBound(unsigned level) const = 0;
    };
+
+   inline unsigned
+   bit_size_for_level(unsigned level, unsigned max_level)
+   {
+      if (level == 0)
+      {
+         level = max_level;
+      }
+      return static_cast<unsigned>(ceil(log2(static_cast<double>(level + 1))));
+   }
+
 }; // namespace SUBool
 
 #endif