JavaBDD 在已知变量值时消除(并简化 BDD)(从图中)

Question

我是二元决策图 (BDD) 的新手，当我在已知变量值后尝试简化/重新计算 BDD 时，我陷入了困境。

编程语言是Java，使用的BDD包是JavaBDD。

代码如下。

import net.sf.javabdd.BDD;
import net.sf.javabdd.BDDFactory;

public class run {

    public static void main(String[] args) {

        print("A program to familize myself with BDD");
        runSimplifyBDD();
        print("Program ended");

    }

    private static void runSimplifyBDD() {
        BDDFactory B;
        B = BDDFactory.init(1000, 1000);
        B.setVarNum(8);
        BDD v1 = B.nithVar(1);
        BDD v2 = B.ithVar(2);
        BDD v3 = B.ithVar(3);
        BDD v4 = B.ithVar(4);
        BDD v5 = B.ithVar(5);
        BDD v6 = B.ithVar(6);
        BDD v7 = B.ithVar(7);

        BDD a = v1.xor(v2).not();
        BDD b = v2.xor(v3).not();
        BDD c = (a.xor(b)).not();
        BDD d = v4.xor(v5).not().xor(v6);
        BDD e = v6.xor(v7).not();
        BDD f = d.xor(e).not();

        BDD g = c.xor(f);

        g.printDot(); //first graph diagram
        /* At this point
         * let say we know the BDD variable v1 = One (true)
         * What is the code that should be inserted to simplify the BDD 
         * so that second graph is like the attached image
         */

        g.printDot(); //second graph diagram

    }

    private static void print(String string) {
        System.out.println(string);

    }

}

在注释中应该插入什么代码，以便 int 第二个图变量 v1 像图像中那样被消除。

graphviz 工具(1.02 版)用于通过复制/粘贴 g.printDot(); 的输出来生成图像

Answer 1

我不熟悉 JavaBDD，但熟悉许多其他 BDD 包。您需要的是 compose 功能: http://javabdd.sourceforge.net/apidocs/net/sf/javabdd/BDDFactoryIntImpl.IntBDD.html#compose%28net.sf.javabdd.BDD,%20int%29

public BDD compose(BDD g,
                   int var)

这替换了表达式 g 的变量 var。在你的例子中，变量是 v1，表达式是 True。所以

h = g.compose(One,1);

应该做你想做的事。(我不确定 JavaBDD 中常量 True BDD 的名称是什么，我假设是一个)。