Biodivine/LibBDD

现在您也可以从 Python 访问 lib-bdd 的全部功能！该库作为 AEON.py 包的一部分提供。

此 crate 提供了 Rust 中二进制决策图（BDD）的基本实现——用于表示布尔函数或其他等效对象（如位向量集）的符号数据结构。

与其他流行实现相比，每个 BDD 都拥有自己的内存。因此，它既易于序列化，也易于在线程之间共享。这使得它在处理大量并发 BDD 的应用程序中非常有用，同时在 Rust 中也更符合惯例。

目前，我们支持许多 BDD 的标准操作

• 任何二进制逻辑运算（and、or、iff 等），当然也包括否定。
• 从字符串解析布尔表达式的评估。
• Rust 中构建 BDD 的更符合惯例的宏 bdd!。
• CNF/DNF 转换方法（BDD => CNF/DNF 和 CNF/DNF => BDD）。（我们不保证 CNF/DNF 的最小性）
• BDD 的二进制和文本序列化/反序列化。
• 估值/路径迭代器和其他 Bdd 内省方法（random_valuation、most_fixed_clause 等）。
• 将 Bdd 导出回布尔表达式。
• "关系"操作：投影（存在量化）、选择（限制）和唯一子集选择（请参阅教程以获取更多信息）。
• 各种“高级”应用算法：与变量反转（翻转）融合的二进制运算、强制节点限制、存在/全称投影；三元运算和三元运算与变量反转...
• 导出为 .dot 图。

所有功能的更详细描述可以在我们的 教程模块 中找到，当然也可以在 API 文档 中找到。

use biodivine_lib_bdd::*;

fn main() {
    let mut builder = BddVariableSetBuilder::new();
    let [a, b, c] = builder.make(&["a", "b", "c"]);
    let variables: BddVariableSet = builder.build();
    
    // String expressions:
    let x = variables.eval_expression_string("(a <=> !b) | c ^ a");
    // Macro:
    let y = bdd!(variables, (a <=> (!b)) | (c ^ a));
    // Logical operators:
    let z = variables.mk_literal(a, true)
        .iff(&variables.mk_literal(b, false))
        .or(&variables.mk_literal(c, true).xor(&variables.mk_literal(a, true)));

    assert!(!x.is_false());
    assert_eq!(6.0, x.cardinality());
    assert_eq!(x, y);
    assert_eq!(y, z);
    assert_eq!(z, x);

    for valuation in x.sat_valuations() {
        assert!(x.eval_in(&valuation));
    }   
}

正确性： 目前，该项目具有相当好的测试覆盖率（包括一个简单的公式模糊测试器），并在多个应用中使用。然而，如果出现任何意外行为，请在此处提交问题。有许多边缘情况，我们可能还没有考虑到。

完整性： 虽然库可以支持广泛的适用范围，但API仍然缺少其他BDD库提供的某些功能。此外，某些方法的表现力肯定可以改进。如果您发现某些内容缺失或实现速度异常缓慢/不切实际，请随时创建一个带有功能请求的问题，或者向我们发送拉取请求！

引用

如果您在学术研究中使用 lib-bdd，我们将非常感谢您的引用。尽管没有特定的 lib-bdd 出版物，但 lib-bdd 源于工具 AEON。因此，您可以引用 lib-bdd 为“工具 AEON 的 BDD 库”。

@inproceedings{aeon,
  title     = {{AEON}: {A}ttractor {B}ifurcation {A}nalysis of {P}arametrised {B}oolean {N}etworks},
  author    = {Bene{\v{s}}, Nikola
           and Brim, Lubo{\v{s}}
           and Kadlecaj, Jakub
           and Pastva, Samuel
           and {\v{S}}afr{\'a}nek, David},
  year      = {2020},
  month     = {07},
  booktitle = {Computer Aided Verification},
  editor    = {Lahiri, Shuvendu K.
           and Wang, Chao},
  pages     = {569 -- 581},
  numPages  = {13},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {12224},
  isbn      = {978-3-030-53288-8},
  doi       = {10.1007/978-3-030-53288-8\_28}
}

性能

此处展示的基准测试相当过时，但仍有一定相关性。目前正在进行一项工作，以提供更好的基准测试套件，但尚未完成。

每个 BDD 实现的关键部分是性能。目前，仓库中包含一个 benchmark 分支，其中包含几个可使用此包以及其他最先进的 BDD 库（bex、cudd 和 buddy）评估的基准问题。根据我们的经验，对于复杂问题实例，biodivine-lib-bdd 的性能与这些库相当。

基准测试通常包括逐步构建一个指数级大小的 BDD。对于节点重用至关重要的某些应用（非常相似的公式反复出现，或对单个 BDD 进行非常小的修改），lib-bdd 可能会较慢。然而，根据我们的经验，这类问题在验证/形式方法中很少出现。

请注意，尽管 buddy 获胜，但在实现这一级别的性能时，初始缓存大小的设置是关键的（每个基准测试都专门调整了缓存大小以避免垃圾收集和过度分配）。如果事先不知道问题的大小，buddy 的性能可能会显著下降。