JavaBDD подсчет с подмножеством переменных

Question

Я использую 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.

Является ли использование there () некорректным?

Answer 1

После небольшой игры я понял, в чем моя проблема.

double partSats = result.satCount(union);

Возвращает ли правильный ответ. Он рассчитывает, сколько существует возможных решений, и делит решение на 2 ^ (# наборов в наборе).

Причина, по которой я подумал, что 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;
  }