Author name cluster

Florent Capelli

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.

7 papers

2 author rows

IJCAI Conference 2024 Conference Paper

A Top-Down Tree Model Counter for Quantified Boolean Formulas

Florent Capelli
Jean-Marie Lagniez
Andreas Plank
Martina Seidl

This paper addresses the challenge of solution counting for Quantified Boolean Formulas (QBFs), a task distinct from the well-established model counting problem for SAT (\#SAT). Unlike SAT, where models are straightforward assignments to Boolean variables, QBF solution counting involves tree models that capture dependencies among variables within different quantifier blocks. We present a comprehensive top-down tree model counter capable of handling diverse satisfiable QBF formulas. Emphasizing the critical role of the branching heuristic, which must consider variables in the correct order according to quantification blocks, we further demonstrate the importance of addressing connected components, free variables, and caching. Experimental results indicate that our proposed approach for counting tree models of QBF formulas is highly efficient in practice, surpassing existing state-of-the-art methods designed for this specific purpose.

PDF Details DOI

AAAI Conference 2021 Conference Paper

Certifying Top-Down Decision-DNNF Compilers

Florent Capelli
Jean-Marie Lagniez
Pierre Marquis

Certifying the output of tools solving complex problems so as to ensure the correctness of the results they provide is of tremendous importance. Despite being widespread for SATsolvers, this level of exigence has not yet percolated for tools solving more complex tasks, such as model counting or knowledge compilation. In this paper, the focus is laid on a general family of top-down Decision-DNNF compilers. We explain how those compilers can be tweaked so as to output certifiable Decision-DNNF circuits, which are mainly standard Decision-DNNF circuits decorated by annotations serving as certificates. We describe a polynomial-time checker for testing whether a given CNF formula is equivalent or not to a given certifiable Decision-DNNF circuit. Finally, leveraging a modified version of the compiler D4 for generating certifiable Decision-DNNF circuits and an implementation of the checker, we present the results of an empirical evaluation that has been conducted for assessing how large are the certifiable Decision-DNNF circuits that can be generated in practice, and how much time is needed to compute and to check such circuits.

PDF Details

SAT Conference 2019 Conference Paper

Knowledge Compilation Languages as Proof Systems

Florent Capelli

Abstract In this paper, we study proof systems in the sense of Cook-Reckhow for problems that are higher in the Polynomial Hierarchy than coNP, in particular, #SAT and maxSAT. We start by explaining how the notion of Cook-Reckhow proof systems can be apply to these problems and show how one can twist existing languages in knowledge compilation such as decision DNNF so that they can be seen as proof systems for problems such as #SAT and maxSAT.

Details

IJCAI 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.

PDF Details

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.

Details

Highlights Conference 2014 Conference Abstract

Hypergraph Acyclicities and Propositional Model Counting

Florent Capelli

We present in this talk structural restrictions of CNF-formulas to find tractable classes for the problem #SAT. We explain why α -acyclicity is not appropriate for this problem. We then introduce β -acyclicity and present a polynomial time algorithm for #SAT on β -acyclic CNF-formulas.

PDF Details

SAT Conference 2014 Conference Paper

Hypergraph Acyclicity and Propositional Model Counting

Florent Capelli
Arnaud Durand 0001
Stefan Mengel

Abstract We show that the propositional model counting problem #SAT for CNF-formulas with hypergraphs that allow a disjoint branches decomposition can be solved in polynomial time. We show that this class of hypergraphs is incomparable to hypergraphs of bounded incidence cliquewidth which were the biggest class of hypergraphs for which #SAT was known to be solvable in polynomial time so far. Furthermore, we present a polynomial time algorithm that computes a disjoint branches decomposition of a given hypergraph if it exists and rejects otherwise. Finally, we show that some slight extensions of the class of hypergraphs with disjoint branches decompositions lead to intractable #SAT, leaving open how to generalize the counting result of this paper.

Details