能否在BuDDy中利用对应BDD（二元决策图）对布尔表达式求值？

安全阿岳

2026-8-27

回答

BuDDy完全支持你说的「给BDD对应表达式的变量手动指派真值，直接计算整个表达式结果」的需求，原生API就提供了对应能力，不需要自己手动遍历BDD节点实现。

核心实现方式

你直接用BuDDy自带的bdd_eval接口即可，这个接口的作用就是对给定的BDD根节点，按照传入的变量赋值表计算布尔结果，返回值为int类型，1代表表达式为真，0代表表达式为假。

针对你举的`(!a && b)`示例，可参考如下实现逻辑

初始化BDD运行环境，声明你需要用到的布尔变量，变量按创建顺序对应从0开始的索引值
按照布尔表达式的逻辑构建对应BDD结构
准备和变量总数等长的整型数组作为赋值表，数组下标对应变量索引，对应位置存0代表变量为假、1代表变量为真
调用bdd_eval传入表达式BDD和赋值表，即可拿到最终求值结果

对应简化可运行代码示例：

#include <bdd.h>
#include <iostream>

int main() {
    // 初始化BDD包，配置节点缓存、启用2个布尔变量
    bdd_init(1000, 100);
    bdd_setvarnum(2);
    bdd a = bdd_ithvar(0); // 索引0对应变量a
    bdd b = bdd_ithvar(1); // 索引1对应变量b

    // 构建 !a && b 对应的BDD
    bdd expr = bdd_not(a) & b;

    // 测试用例1：a为假、b为真，预期结果为真（输出1）
    int assign_case1[] = {0, 1};
    std::cout << "a=0, b=1 求值结果：" << bdd_eval(expr, assign_case1) << std::endl;

    // 测试用例2：a为真、b为真，预期结果为假（输出0）
    int assign_case2[] = {1, 1};
    std::cout << "a=1, b=1 求值结果：" << bdd_eval(expr, assign_case2) << std::endl;

    // 释放BDD资源
    bdd_done();
    return 0;
}