基于BDD的符号推理工具，高效求解抽象辩证框架所有稳定解。
BAss: Symbolic Reasoning in Abstract Dialectical Frameworks
- 用二进制决策图实现全符号化计算，支持多种语义模型
- 在大规模解空间中性能远超已有BDD工具，部分场景优于SAT/ASP方法
- 首次实现某些生物网络全部固定点枚举，推动系统生物学分析
我们提出BAss（基于二叉决策图的ADFs符号求解器），一种新型分析工具，用于抽象辩证框架（ADFs）的符号计算。该方法支持所有可接受、完整、偏好解释及二值化、稳定模型的完全符号化求解。其灵感源于近期发现的布尔网络与ADFs之间的等价关系。我们在来自布尔网络和ADFs领域的大量真实世界模型上进行了实验。结果表明，BAss显著优于现有基于BDD的工具，在包含大解空间的场景下甚至比最先进的SAT/ASP方法更具优势。特别地，BAss能够枚举某些生物网络的所有固定点或最小陷阱空间，这些任务超出现有工具的能力范围，从而为系统生物学中的新分析与案例研究提供了可能。这些成果凸显了符号推理在复杂现实应用中的实际价值，尤其在系统生物学与形式论证领域。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。