BDD 使用 PyEDA 测试表达式是否为真

Question

我正在尝试使用 PyEDA 包 BDD 实现，并提供“True/False”数据来构建功能性 BDD。然后测试我的数据更新时新表达式在构造的 BDD 中是否为“True”。

但是，我无法利用“等效”方法并得到“True”。 也许，表达结构是错误的，或者其他什么。

我没有电子背景，因此我无法完全理解文档中介绍的一些技术。

from pyeda.inter import *
import random

str_binary = [format(i, '04b') for i in range(1, 5)]

# 0001 = ~x4 & ~x3 & ~x2 & x1
def convert_binary_str_to_expr(str_binary):
    expr = ['~'*abs(int(str_binary[i])-1) + f'x{i}' for i in range(len(str_binary))]
    return ' & '.join(expr)

# ~x4 & ~x3 & ~x2 & x1 | ~x4 & ~x3 & x2 & ~x1
def join_exprs(str_binary):
    formulas = []

    for e in str_binary:
        formulas.append( convert_binary_str_to_expr(e) )

    return ' | '.join(formulas)

expression = join_exprs(str_binary)

# construct BDD
bdd_exprs = expr(expression)
bdd = expr2bdd(bdd_exprs)

# {x3: 1, x2: 0, x1: 0, x0: 0}
true_expr= bdd_exprs.satisfy_one()

# the idea is to construct like 'x3 & ~x2 & ~x1 & ~x0'
# where the x variables are read from BDD.inputs

# first attempt
test_true_1 = [inp if val==1 else ~inp for inp, val in  zip(bdd.inputs, true_expr.values())]

# False, should be True
bdd.equivalent(test_true_1)

# seconde attempt
# And(~x0, ~x1, ~x2, x3)
test_true_2 = expr('x3 & ~x2 & ~x1 & ~x0')

# False, should be True
bdd.equivalent(test_true_2)

Answer 1

我找到了一种解决方法，通过从测试表达式构造 BDD，然后测试它是否存在于原始 BDD 中。

test_bdd.satisfy_one() in src_bdd.satisfy_all()

Answer 2

前面的答案有效，但是，它线性检查表达式： 之前的回答

test_bdd.satisfy_one() in src_bdd.satisfy_all()

这是我的新方法，它检查联合表达式和提供的树是否到达终端节点零，这意味着该表达式未出现在树中： 完整示例：

# import
from pyeda.inter import *
from pyeda.boolalg.bdd import BDDZERO, BDDONE

# define BDD variables
x1, x2, x3 = map(bddvar, 'x1 x2 x3'.split())

# build the BDD
dd = BDDZERO # root

# add couple of expressions
f1 = x1 & ~x2 & x3
dd |= f1

f2 = ~x1 & x2 & x3
dd |= f2

# check expression (true = not found)
f3 = ~x1 & x2 & ~x3
(dd & f3) == BDDZERO

# check expression (false = found)
f4 = ~x1 & x2 & x3
(dd & f4) == BDDZERO