1

我正在使用 JavaBDD 对 BDD 进行一些计算。我有一个非常大的 BDD，其中包含许多变量，我想计算有多少种方法可以满足这些变量的一小部分。

我目前的尝试如下所示：

// var 1,2,3 are BDDVarSets with 1 variable.
BDDVarSet union = var1;
union = union.union(var2);
union = union.union(var3);

BDD varSet restOfVars = allVars.minus(union);
BDD result = largeBdd.exist(restOfVars);

double sats = result.satCount(); // Returns a very large number (way too large).
double partSats = result.satCount(union) // Returns an inccorrect number. It is documented that this should not work.

存在（）的用法不正确吗？

4

1 回答 1

0

玩了一会儿后，我明白了我的问题所在。

double partSats = result.satCount(union);

是否返回正确答案。它所做的是计算有多少可能的解决方案，并将解决方案除以 2^(#vars in set)。

我认为satCount(union)不起作用的原因是由于exist()代码中其他地方的使用不正确。

以下是 satCound(varSet) 的实现供参考：

  /**
   * <p>Calculates the number of satisfying variable assignments to the variables
   * in the given varset.  ASSUMES THAT THE BDD DOES NOT HAVE ANY ASSIGNMENTS TO
   * VARIABLES THAT ARE NOT IN VARSET.  You will need to quantify out the other
   * variables first.</p>
   * 
   * <p>Compare to bdd_satcountset.</p>
   * 
   * @return the number of satisfying variable assignments
   */
  public double satCount(BDDVarSet varset) {
    BDDFactory factory = getFactory();

    if (varset.isEmpty() || isZero()) /* empty set */
      return 0.;

    double unused = factory.varNum();
    unused -= varset.size();
    unused = satCount() / Math.pow(2.0, unused);

    return unused >= 1.0 ? unused : 1.0;
  }
于 2020-04-24T13:30:47.197 回答