fix issue #6 by adjusting the apparent model count differently

(depending on whether a not-yet-projected var is additive or disjunctive)
vardigroup · Jul 19, 2022 · 44096a5 · 44096a5
1 parent 190181d
commit 44096a5
Show file tree

Hide file tree

Showing 2 changed files with 10 additions and 3 deletions.
diff --git a/addmc/src/implementation/phase.cpp b/addmc/src/implementation/phase.cpp
@@ -159,7 +159,7 @@ Float Executor::computeModelCount(const Cnf &cnf) {
   Dd dd = countSubtree(static_cast<JoinNode *>(joinRoot), cnf, projectedCnfVars);
 
   Float modelCount = dd.countConstDdFloat();
-  modelCount = util::adjustModelCount(modelCount, projectedCnfVars, cnf.getLiteralWeights());
+  modelCount = util::adjustModelCount(modelCount, projectedCnfVars, cnf.getAdditiveVars(), cnf.getLiteralWeights());
   return modelCount;
 }
 

diff --git a/addmc/src/interface/util.hpp b/addmc/src/interface/util.hpp
@@ -320,7 +320,7 @@ namespace util {
     return true;
   }
 
-  template<typename T> Float adjustModelCount(Float apparentModelCount, const T &projectedCnfVars, const Map<Int, Float> &literalWeights) {
+  template<typename T> Float adjustModelCount(Float apparentModelCount, const T &projectedCnfVars, const T &additiveCnfVars, const Map<Int, Float> &literalWeights) {
     Float totalModelCount = apparentModelCount;
 
     Int totalLiteralCount = literalWeights.size();
@@ -331,7 +331,14 @@ namespace util {
 
     for (Int cnfVar = 1; cnfVar <= totalVarCount; cnfVar++) {
       if (!isFound(cnfVar, projectedCnfVars)) {
-        totalModelCount *= literalWeights.at(cnfVar) + literalWeights.at(-cnfVar);
+        Float hiWeight = literalWeights.at(cnfVar);
+        Float loWeight = literalWeights.at(-cnfVar);
+        if (isFound(cnfVar, additiveCnfVars)) {
+          totalModelCount *= hiWeight + loWeight;
+        }
+        else {
+          totalModelCount *= std::max(hiWeight, loWeight);
+        }
       }
     }