在已知变量值的情况下(从图中)消除(和简化JavaBDD )

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);

    }

}

在注释中，应该插入什么代码，以便在第二张图中消除变量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的名称是什么，我假设有一个)。

Answer 2

我发现一种解决方案是使用限制函数，如下所示。

   //..............omitted lines..........

            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.restrictWith(v1); //added line - use 'g.restrictWith(v1.not());' for negative restriction

            g.printDot(); //second graph diagram

//..............省略各行...............

再次感谢你，史蒂夫