We present BAss (BDD-based ADF symbolic solver), a novel analysis tool for Abstract Dialectical Frameworks (ADFs) based on Binary Decision Diagrams (BDDs). It supports the fully symbolic computation of all admissible, complete, and preferred interpretations, as well as two-valued and stable models of an ADFs. Our approach is inspired by the recently discovered equivalence between Boolean Networks (BNs) and ADFs by Heyninck et al. (2024) and Azpeitia et al. (2024), significantly extending current BDD-based tools bioLQM, AEON, and adf-bdd. We conducted experiments on a large-scale collection of real-world models from both the BN and ADF communities. Our results show that BAss dramatically outperforms previous BDD-based tools and is competitive (even significantly better in some cases) with state-of-the-art SAT/ASP-based methods, particularly in scenarios involving large solution spaces. Notably, BAss is able to enumerate all fixed points or minimal trap spaces of certain biological networks beyond the reach of existing tools, thereby enabling new analysis and case studies in systems biology. These results highlight the practical relevance of symbolic reasoning for complex real-world applications, particularly in systems biology and formal argumentation.
翻译:我们提出BAss(基于BDD的抽象辩论框架符号求解器),这是一种基于二叉决策图(BDD)的新型抽象辩论框架(ADFs)分析工具。该工具支持对所有可接受、完全及优先解释,以及ADF的二值模型和稳定模型进行全符号计算。我们的方法受Heyninck等人(2024)与Azpeitia等人(2024)最新发现的布尔网络(BNs)与ADF间等价关系的启发,显著扩展了当前基于BDD的工具bioLQM、AEON和adf-bdd。我们在来自BN与ADF社区的大规模真实模型集合上进行了实验。结果表明,BAss的性能远超以往基于BDD的工具,并与基于SAT/ASP的最先进方法具有竞争力(在某些场景下甚至显著更优),特别是在涉及大解空间的情况下。值得注意的是,BAss能够枚举某些现有工具无法处理的生物网络的所有不动点或最小诱捕空间,从而为系统生物学领域的新分析方法和案例研究提供了可能。这些结果凸显了符号推理在复杂实际应用(尤其是系统生物学与形式论证)中的实践价值。