Highlights Conference 2017 Conference Abstract
Herbrand Property, Finite Quasi-Herbrand Models, and a Chandra-Merlin Theorem for Quantified Conjunctive Queries
- Simone Bova
- Fabio Mogavero
Abstract available in PDF.
Author name cluster
Simone Bova
Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.
9 papers
2 author rows
Possible papers
9IJCAI Conference 2016 Conference Paper
Knowledge Compilation Meets Communication Complexity
- Simone Bova
- Florent Capelli
- Stefan Mengel
- Friedrich Slivovsky
Choosing a language for knowledge representation and reasoning involves a trade-off between two competing desiderata: succinctness (the encoding should be small) and tractability (the language should support efficient reasoning algorithms). The area of knowledge compilation is devoted to the systematic study of representation languages along these two dimensions - in particular, it aims to determine the relative succinctness of languages. Showing that one language is more succinct than another typically involves proving a nontrivial lower bound on the encoding size of a carefully chosen function, and the corresponding arguments increase in difficulty with the succinctness of the target language. In this paper, we introduce a general technique for obtaining lower bounds on Decomposable Negation Normal Form (DNNFs), one of the most widely studied and succinct representation languages, by relating the size of DNNFs to multi-partition communication complexity. This allows us to directly translate lower bounds from the communication complexity literature into lower bounds on the size of DNNF representations. We use this approach to prove exponential separations of DNNFs from deterministic DNNFs and of CNF formulas from DNNFs.
TCS Journal 2016 Journal Article
Quantified conjunctive queries on partially ordered sets
- Simone Bova
- Robert Ganian
- Stefan Szeider
We study the computational problem of checking whether a quantified conjunctive query (a first-order sentence built using only conjunction as Boolean connective) is true in a finite poset (a reflexive, antisymmetric, and transitive directed graph). We prove that the problem is already NP-hard on a certain fixed poset, and investigate structural properties of posets yielding fixed-parameter tractability when the problem is parameterized by the query. Our main algorithmic result is that model checking quantified conjunctive queries on posets is fixed-parameter tractable when parameterized by the sentence and the width of the poset (the maximum size of a subset of pairwise incomparable elements). We complement our algorithmic result by complexity results with respect to classes of finite posets in a hierarchy of natural poset invariants, establishing its tightness in this sense.
AAAI Conference 2016 Conference Paper
SDDs Are Exponentially More Succinct than OBDDs
- Simone Bova
Introduced by Darwiche (2011), sentential decision diagrams (SDDs) are essentially as tractable as ordered binary decision diagrams (OBDDs), but tend to be more succinct in practice. This makes SDDs a prominent representation language, with many applications in artificial intelligence and knowledge compilation. We prove that SDDs are more succinct than OBDDs also in theory, by constructing a family of boolean functions where each member has polynomial SDD size but exponential OBDD size. This exponential separation improves a quasipolynomial separation recently established by Razgon (2014a), and settles an open problem in knowledge compilation (Darwiche 2011).
CSL Conference 2015 Conference Paper
First-Order Queries on Finite Abelian Groups
- Simone Bova
- Barnaby Martin
We study the computational problem of checking whether a logical sentence is true in a finite abelian group. We prove that model checking first-order sentences on finite abelian groups is fixed-parameter tractable, when parameterized by the size of the sentence. We also prove that model checking monadic second-order sentences on finite abelian groups finitely presented by integer matrices is not fixed-parameter tractable (under standard assumptions in parameterized complexity).
SAT Conference 2015 Conference Paper
On Compiling CNFs into Structured Deterministic DNNFs
- Simone Bova
- Florent Capelli
- Stefan Mengel
- Friedrich Slivovsky
Abstract We show that the traces of recently introduced dynamic programming algorithms for #SAT can be used to construct structured deterministic DNNF (decomposable negation normal form) representations of propositional formulas in CNF (conjunctive normal form). This allows us prove new upper bounds on the complexity of compiling CNF formulas into structured deterministic DNNFs in terms of parameters such as the treewidth and the clique-width of the incidence graph.
I&C Journal 2013 Journal Article
Generic expression hardness results for primitive positive formula comparison
- Simone Bova
- Hubie Chen
- Matthew Valeriote
We study the expression complexity of two basic problems involving the comparison of primitive positive formulas: equivalence and containment. In particular, we study the complexity of these problems relative to finite relational structures. We present two generic hardness results for the studied problems, and discuss evidence that they are optimal and yield, for each of the problems, a complexity trichotomy.
TCS Journal 2013 Journal Article
Polynomial space hardness without disjunction property
- Simone Bova
- Franco Montagna
Horčík and Terui [8] show that, if a substructural logic enjoys the disjunction property, then its tautology problem is PSPACE-hard. We prove that all substructural logics in the interval between intuitionistic logic and generalized Hájek basic logic have a PSPACE-hard tautology problem, which implies that uncountably many substructural logics lacking the disjunction property have a PSPACE-hard tautology problem.
TCS Journal 2009 Journal Article
The consequence relation in the logic of commutative GBL-algebras is PSPACE-complete
- Simone Bova
- Franco Montagna
Commutative, integral and bounded G B L -algebras form a subvariety of residuated lattices which provides the algebraic semantics of an interesting common fragment of intuitionistic logic and of several fuzzy logics. It is known that both the equational theory and the quasiequational theory of commutative G B L -algebras are decidable (in contrast to the noncommutative case), but their complexity has not been studied yet. In this paper, we prove that both theories are in PSPACE, and that the quasiequational theory is PSPACE -hard.