SCC binary encoding of one-provability

lib/up_scc_binary.cpp

@@ -8,6 +8,7 @@
  */
 
 #include "up_scc_binary.h"
+#include "up_levels.h"
 
 void
 SUBool::UPSCCBinary::Encode(unsigned max_level, std::vector<unsigned> *inputs,
@@ -25,7 +26,7 @@ SUBool::UPSCCBinary::Encode(unsigned max_level, std::vector<unsigned> *inputs,
 
    Context ctx{max_level, VarInfoList(2 * mCnf.MaxVariable()),
        mVarStore.VarArray(mCnf.MaxVariable(), true, ":in(", ")"),
-       mVarStore.VarArray(mCnf.MaxVariable(), true, ":out(", ")"), {}};
+       mVarStore.VarArray(mCnf.MaxVariable(), true, ":out(", ")"), {}, {}};
    InitOutClauses(ctx);
 
    AddClauses(ctx, *clauses);
@@ -127,9 +128,25 @@ SUBool::UPSCCBinary::FireVariableInMainSCC(Context &ctx, const LitImpl &impl,
 {
    // Literal in the main SCC
    // - Init fire variable f[impl_index, lit]
+   mVarStore.NameStream() << "f[" << impl_index << ", " << lit << "]";
+   unsigned fv = mVarStore.NewVariable();
+   auto neg_fv = make_negative_literal(fv);
    // - Add implications to the output variables of the body
+   FireVariableImpliesBody(ctx, impl, fv, clauses);
    // - Add implications to the inequalities
+   for (const auto &b : impl.Body())
+   {
+      if (mSCCGraph.SCC(lit) != mSCCGraph.SCC(b))
+      {
+         continue;
+      }
+      // c represents B[lit]>B[b]
+      auto c = Comparison(ctx, lit, b, clauses);
+      // fv->B[lit]>B[b]
+      clauses.emplace_back(neg_fv, make_positive_literal(c));
+   }
    // - Add to the out clause
+   ctx.vars[lit.Index()].out_clause.push_back(make_positive_literal(fv));
 }
 
 unsigned
@@ -157,11 +174,61 @@ SUBool::UPSCCBinary::SimpleFireVar(const Context &ctx, const LitImpl &impl,
    }
    mVarStore.NameStream() << "f[" << impl_index << "]";
    unsigned fv = mVarStore.NewVariable();
+   FireVariableImpliesBody(ctx, impl, fv, clauses);
+   return fv;
+}
+
+void
+SUBool::UPSCCBinary::FireVariableImpliesBody(const Context &ctx,
+    const LitImpl &impl, unsigned fv, std::vector<Clause> &clauses) const
+{
    auto neg_fv = make_negative_literal(fv);
    for (const auto &lit : impl.Body())
    {
       clauses.emplace_back(
           neg_fv, make_positive_literal(ctx.outputs[lit.Index()]));
    }
-   return fv;
+}
+
+unsigned
+SUBool::UPSCCBinary::Comparison(Context &ctx, const Literal &cons_literal,
+    const Literal &body_literal, std::vector<Clause> &clauses) const
+{
+   auto cached_comp = ctx.comparisons.find({cons_literal, body_literal});
+   if (cached_comp != ctx.comparisons.end())
+   {
+      return cached_comp->second;
+   }
+   return NewComparison(ctx, cons_literal, body_literal, clauses);
+}
+
+unsigned
+SUBool::UPSCCBinary::NewComparison(Context &ctx, const Literal &cons_literal,
+    const Literal &body_literal, std::vector<Clause> &clauses) const
+{
+   InitLevelVars(ctx, cons_literal);
+   InitLevelVars(ctx, body_literal);
+   unsigned new_comp =
+       encode_bitvector_gt(ctx.vars[cons_literal.Index()].level_vars,
+           ctx.vars[body_literal.Index()].level_vars, mVarStore, &clauses, "g",
+           cons_literal.ToString(), body_literal.ToString());
+   return ctx.comparisons[{cons_literal, body_literal}] = new_comp;
+}
+
+void
+SUBool::UPSCCBinary::InitLevelVars(Context &ctx, const Literal &lit) const
+{
+   auto &level_vars = ctx.vars[lit.Index()].level_vars;
+   if (!level_vars.empty())
+   {
+      return;
+   }
+   unsigned bit_width =
+       BitSizeForLevel(std::min(ctx.max_level, mSCCGraph.EffSCCVarSize(lit)));
+   level_vars.reserve(bit_width);
+   for (unsigned bit = 0; bit < bit_width; ++bit)
+   {
+      mVarStore.NameStream() << "B[" << lit << ", " << bit << "]";
+      level_vars.push_back(mVarStore.NewVariable());
+   }
 }

lib/up_scc_binary.h

@@ -9,6 +9,9 @@
 #ifndef __UP_SCC_BINARY_H
 #define __UP_SCC_BINARY_H
 
+#include <map>
+#include <vector>
+
 #include "impl_system.h"
 #include "impl_system_graph.h"
 #include "upenc.h"
@@ -42,6 +45,7 @@ namespace SUBool
          std::vector<unsigned> inputs;
          std::vector<unsigned> outputs;
          std::vector<bool> scc_buffer;
+         std::map<std::pair<Literal, Literal>, unsigned> comparisons;
       };
 
     private:
@@ -63,6 +67,13 @@ namespace SUBool
           std::vector<Clause> &clauses) const;
       unsigned SimpleFireVar(const Context &ctx, const LitImpl &impl,
           unsigned impl_index, std::vector<Clause> &clauses) const;
+      void FireVariableImpliesBody(const Context &ctx, const LitImpl &impl,
+          unsigned fv, std::vector<Clause> &clauses) const;
+      unsigned Comparison(Context &ctx, const Literal &cons_literal,
+          const Literal &body_literal, std::vector<Clause> &clauses) const;
+      unsigned NewComparison(Context &ctx, const Literal &cons_literal,
+          const Literal &body_literal, std::vector<Clause> &clauses) const;
+      void InitLevelVars(Context &ctx, const Literal &lit) const;
 
     public:
       UPSCCBinary(const Config &conf, const CNF &cnf,