The compilation of feature models into binary decision diagrams (BDDs) is a major challenge in the area of configurable systems analysis. For many large-scale feature models such as the variants of the prominent Linux product line, BDDs could not yet be obtained due to exceeding state-of-the-art compilation capabilities. Until now, BDD compilation has been mainly considered on standard settings of existing BDD tools, barely exploiting advanced techniques or tuning parameters. In this article, we conduct a comprehensive study on how to configure various techniques from the literature and thus improve compilation performance for feature models given in conjunctive normal form. Specifically, we evaluate preprocessing for satisfiability solving (SAT), variable and clause ordering heuristics, as well as non-standard and multi-threaded BDD construction schemes. Our experiments on recent feature models demonstrate that BDD compilation of feature models greatly benefits from these techniques. We show that our methods enable BDD compilations of many large-scale feature models within seconds, including the whole ECOS feature model collection for which a compilation was previously infeasible.

Abstract argumentation is a prominent reasoning framework. It comes with a variety of semantics and has lately been enhanced by probabilities to enable a quantitative treatment of argumentation. While admissibility is a fundamental notion for classical reasoning in abstract argumentation frameworks, it has barely been reflected so far in the probabilistic setting. In this paper, we address the quantitative treatment of abstract argumentation based on probabilistic notions of admissibility. Our approach follows the natural idea of defining probabilistic semantics for abstract argumentation by systematically imposing constraints on the joint probability distribution on the sets of arguments, rather than on probabilities of single arguments. As a result, there might be either a uniquely defined distribution satisfying the constraints, but also none, many, or even an infinite number of satisfying distributions are possible. We provide probabilistic semantics corresponding to the classical complete and stable semantics and show how labeling schemes provide a bridge from distributions back to argument labelings. In relation to existing work on probabilistic argumentation, we present a taxonomy of semantic notions. Enabled by the constraint-based approach, standard reasoning problems for probabilistic semantics can be tackled by SMT solvers, as we demonstrate by a proof-of-concept implementation.

Abstract argumentation is a prominent reasoning framework. It comes with a variety of semantics, and has lately been enhanced by probabilities to enable a quantitative treatment of argumentation. While admissibility is a fundamental notion in the classical setting, it has been merely reflected so far in the probabilistic setting. In this paper, we address the quantitative treatment of argumentation based on probabilistic notions of admissibility in a way that they form fully conservative extensions of classical notions. In particular, our building blocks are not the beliefs regarding single arguments. Instead we start from the fairly natural idea that whatever argumentation semantics is to be considered, semantics systematically induces constraints on the joint probability distribution on the sets of arguments. In some cases there might be many such distributions, even infinitely many ones, in other cases there may be one or none. Standard semantic notions are shown to induce such sets of constraints, and so do their probabilistic extensions. This allows them to be tackled by SMT solvers, as we demonstrate by a proof-of-concept implementation. We present a taxonomy of semantic notions, also in relation to published work, together with a running example illustrating our achievements.