Fixed size estimation in SCC unary encoding

lib/up_scc_unary.cpp

@@ -131,9 +131,9 @@ SUBool::UPSCCUnary::EstimateSize(unsigned max_level) const -> NFSize
       max_level = max_level_bound;
    }
    auto s = InitialContextSize(max_level);
-   // std::cout << "After InitialContextSize: " << s << std::endl;
+   std::cout << "After InitialContextSize: " << s << std::endl;
    s += FireClausesSize(max_level);
-   // std::cout << "After FireClausesSize: " << s << std::endl;
+   std::cout << "After FireClausesSize: " << s << std::endl;
    return s;
 }
 
@@ -187,7 +187,7 @@ SUBool::UPSCCUnary::FireClauses(Context &ctx, const LitImpl &impl,
    auto fv = InitFireVariables(ctx, impl, impl_index);
    // logs.TLog(3) << "Main scc index of implication " << impl << " is "
    //<< fv.main_scc << std::endl;
-   if (impl.Body().size() > 1)
+   if (impl.Body().size() != 1)
    {
       FireVarDefinition(ctx, impl, fv, clauses);
    }
@@ -201,7 +201,11 @@ SUBool::UPSCCUnary::FireClausesSize(unsigned max_level) const
    for (const auto &impl : mImplSystem)
    {
       auto scc_info = mSCCGraph.InspectImplSCC(impl);
-      if (impl.Body().size() != 1)
+      if (impl.EmptyBody())
+      {
+         s += NFSize{1, 1, 1};
+      }
+      else if (impl.Body().size() > 1)
       {
          unsigned fv_count = 0;
          if (scc_info.cons_out_main_scc_size > 0)
@@ -218,10 +222,14 @@ SUBool::UPSCCUnary::FireClausesSize(unsigned max_level) const
       }
       for (const auto &lit : impl.Cons())
       {
-         s.len += std::min(LPrime(lit), max_level);
+         if (mSCCGraph.SCC(lit) == scc_info.main_scc)
+         {
+            s.len += std::min(LPrime(lit), max_level);
+         }
       }
       s.len += scc_info.cons_out_main_scc_size;
    }
+   // s.len += mImplSystem.Size();
    return s;
 }
 
@@ -244,6 +252,11 @@ void
 SUBool::UPSCCUnary::SimpleFireVarDefinition(Context &ctx, const LitImpl &impl,
     unsigned fire_var, std::vector<Clause> &clauses) const
 {
+   if (impl.EmptyBody())
+   {
+      clauses.emplace_back(make_positive_literal(fire_var));
+      return;
+   }
    auto fire_lit = make_negative_literal(fire_var);
    for (const auto &lit : impl.Body())
    {

test/test_upenc.cpp

@@ -72,6 +72,7 @@ const std::string dimacs1 = "p cnf 20 48\n"
                             "-2 -3 16 0\n"
                             "1 0\n"
                             "-3 9 0\n";
+const std::string dimacs_units = "p cnf 1 1\n1 0\n";
 
 bool
 SUBool::TestUPEncoder::TestSizeEstimateOfEncoderWithLevel(
@@ -95,6 +96,7 @@ SUBool::TestUPEncoder::TestSizeEstimateOfEncoderWithLevel(
       std::cout << "Checking size estimator of an encoder (max variable "
                    "mismatch) [FAILED]"
                 << std::endl;
+      std::cout << "Encoding:\n" << enc_cnf << std::endl;
       return false;
    }
    if (sizes.size != enc_cnf.Size())
@@ -236,11 +238,15 @@ SUBool::TestUPEncoder::TestSizeEstimateSCCUnary(
    VarStore var_store(false);
    auto is = init_lit_impl_system(cnf, is_type);
    LitISGraph scc_graph(is);
-   // std::cout << "cnf:\n" << cnf << std::endl;
-   // std::cout << "impl system:\n" << is << std::endl;
-   // scc_graph.DumpImplSystem(3, is);
    UPSCCUnary enc(cnf, cl2lit, var_store, is, scc_graph);
-   return TestSizeEstimateOfEncoder(enc, var_store);
+   if (TestSizeEstimateOfEncoder(enc, var_store))
+   {
+      return true;
+   }
+   std::cout << "cnf:\n" << cnf << std::endl;
+   std::cout << "impl system:\n" << is << std::endl;
+   scc_graph.DumpImplSystem(3, is);
+   return false;
 }
 
 bool
@@ -253,12 +259,16 @@ SUBool::TestUPEncoder::TestSizeEstimateSCCBinary(
    VarStore var_store(false);
    auto is = init_lit_impl_system(cnf, is_type);
    LitISGraph scc_graph(is);
-   // std::cout << "cnf:\n" << cnf << std::endl;
-   // std::cout << "impl system:\n" << is << std::endl;
-   // scc_graph.DumpImplSystem(3, is);
    UPSCCBinary::Config conf{use_bit_level};
    UPSCCBinary enc(conf, cnf, cl2lit, var_store, is, scc_graph);
-   return TestSizeEstimateOfEncoder(enc, var_store);
+   if (TestSizeEstimateOfEncoder(enc, var_store))
+   {
+      return true;
+   }
+   std::cout << "cnf:\n" << cnf << std::endl;
+   std::cout << "impl system:\n" << is << std::endl;
+   scc_graph.DumpImplSystem(3, is);
+   return false;
 }
 
 bool
@@ -379,6 +389,8 @@ bool
 SUBool::TestUPEncoder::RunTests() const
 {
    return TestSizeEstimateForCNF(Dimacs::parse_cnf(dimacs1))
+          && TestSizeEstimateSCCUnary(
+              Dimacs::parse_cnf(dimacs_units), LIT_IMPL_SYSTEM::BODY_MINIMAL)
           && TestSizeEstimate(10, 20, 50);
 }