BAss: Symbolic Reasoning in Abstract Dialectical Frameworks

TL;DR

BAss is a symbolic reasoning tool for Abstract Dialectical Frameworks that uses BDDs to efficiently compute various interpretations and models, outperforming previous tools and enabling new biological analyses.

Contribution

Introduces BAss, a BDD-based symbolic solver for ADFs, extending existing tools and demonstrating superior performance on large-scale real-world models.

Findings

BAss dramatically outperforms previous BDD-based tools.

BAss is competitive with state-of-the-art SAT/ASP methods.

Enables enumeration of fixed points in biological networks beyond current capabilities.

Abstract

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.