Binary Decision Diagrams (BDDs) and in particular ROBDDs (Reduced Ordered BDDs) are a common data structure for manipulating Boolean Expressions Integrated Circuit design, type inferencers, model checkers, and many other applications. Although a lightweight data structure to implement, the memory-wise behavior of ROBDDs may not be obvious to the program architect. We explore experimentally and theoretically the typical and worst-cases ROBDD sizes in terms of number of nodes and residual compression ratios as compared to un-reduced BDDs; in addition, we provide an algorithm to calculate the worst-case size. Finally, we present an algorithm for constructing a worst-case ROBDD of a given number of variables. Our approach may be useful to projects deciding whether the ROBDD is the appropriate data structure to use, and in building worst-case examples to test their code.
In this work we explore the connections between (linear) nested sequent calculi and ordinary sequent calculi for normal and non-normal modal logics. By proposing local versions to ordinary sequent rules we obtain linear nested sequent calculi for a number of logics, including to our knowledge the first nested sequent calculi for a large class of simply dependent multimodal logics, and for many standard non-normal modal logics. The resulting systems are modular and have separate left and right introduction rules for the modalities, which makes them amenable to specification as linear logic clauses. While this granulation of the sequent rules introduces more choices for proof search, we show how linear nested sequent calculi can be restricted to blocked derivations, which directly correspond to ordinary sequent derivations.
Let v(F) denote the number of vertices in a fixed connected pattern graph F. We show an infinite family of patterns F such that the existence of a subgraph isomorphic to F is expressible by a first-order sentence of quantifier depth (2/3)v(F)+1, assuming that the host graph is sufficiently large and connected. On the other hand, this is impossible for any F with using less than (2/3)v(F)-2 first-order variables.
We study the complexity of the inference problem for propositional circumscription (the minimal inference problem) over arbitrary finite domains. The problem is of fundamental importance in nonmonotonic logics and commonsense reasoning. The complexity of the problem for the two-element domain has been completely classified. In this paper, we classify the complexity of the problem over all conservative languages. We consider a version of the problem parameterized by a set of relations (a constraint language), from which we are allowed to build a knowledge base, and where a linear order used to compare models is a part of an input. We show that in this setting the problem is either P2-complete, coNP-complete, or in P. The classification is based on a coNP-hardness proof for a new class of languages, an analysis of languages that do not express any member of the class and a new general polynomial-time algorithm solving the minimal inference problem for a large class of languages.
Enhancing Datalog with existential quantification gives rise to Datalog^E, a powerful knowledge representation language widely used in ontology-based query answering. In this setting, a conjunctive query is evaluated over a Datalog^E program consisting of extensional data paired with so-called existential rules. Due to their high expressiveness, such rules make the evaluation of queries undecidable, even when the latter are atomic. Decidable Datalog^E fragments have been proposed in the literature (e.g., weakly-acyclic and weakly-guarded); but they pay the price of a higher computational complexity, hindering the implementation of effective systems. Conversely, the results in this paper demonstrate that it is definitely possible to enable fast yet powerful query answering over existential rules, ensuring decidability without any complexity overhead. On the theoretical side, we define the class of parsimonious programs which guarantees decidability of atomic queries. We then strengthen this class to strongly parsimonious programs ensuring decidability also for conjunctive queries. Since parsimony is an undecidable property, we single out Shy, an easily recognizable class of strongly parsimonious programs that generalizes Datalog while preserving its complexity even under conjunctive query evaluation. Shy generalizes also the class of linear existential programs, while it is uncomparable to the other main classes ensuring decidability. On the practical side, we exploit our results to implement DLV^E, an effective system for query answering over parsimonious existential rules. To asses its efficiency, we carry out an experimental analysis, comparing DLV^E against state-of-the-art systems for ontology-based query answering. The results confirm the effectiveness of DLV^E, which outperforms all other systems.