Marco Benedetti

IJCAI Conference 2007 Conference Paper

• Marco Benedetti
• Arnaud Lallouet
• J
• eacute; r
• eacute; mie Vautard

The QCSP+ language we introduce extends the framework of Quantified Constraint Satisfaction Problems (QCSPs) by enabling us to neatly express restricted quantifications via a chain of nested CSPs to be interpreted as alternately conjuncted and disjuncted. Restricted quantifiers turn out to be a convenient solution to the crippling modeling issues we encounter in QCSP and - surprisingly - they help to reuse propagation technology and to prune the search space. Our QCSP+ solver - which also handles arithmetic and global constraints - exhibits state-of-the-art performances.

AAAI Conference 2006 Conference Paper

Abstract Branching for Quantified Formulas

• Marco Benedetti

We introduce a novel search-based decision procedure for Quantified Boolean Formulas (QBFs), called Abstract Branching. As opposed to standard search-based procedures, it escapes the burdensome need for branching on both children of every universal node in the search tree. This is achieved by branching on existential variables only, while admissible universal assignments are inferred. Running examples and experimental results are reported.

SAT Conference 2005 Conference Paper

Quantifier Trees for QBFs

• Marco Benedetti

Abstract We present a method—called quantifier tree reconstruction—that allows to efficiently recover ex-post a portion of the internal structure of QBF instances which was hidden as a consequence of the cast to prenex normal form. Means to profit from a quantifier tree are presented for all the main families of QBF solvers. Experiments on QBFLIB instances are also reported.

LPAR Conference 2004 Conference Paper

Evaluating QBFs via Symbolic Skolemization

• Marco Benedetti

Abstract We describe a novel decision procedure for Quantified Boolean Formulas (QBFs) which aims to unleash the hidden potential of quantified reasoning in applications. The Skolem theorem acts like a glue holding several ingredients together: BDD-based representations for boolean functions, search-based QBF decision procedure, and compilation-to-SAT techniques, among the others. To leverage all these techniques at once we show how to evaluate QBFs by symbolically reasoning on a compact representation for the propositional expansion of the skolemized problem. We also report about a first implementation of the procedure, which yields very interesting experimental results.

SAT Conference 2004 Conference Paper

Incremental Compilation-to-SAT Procedures

• Marco Benedetti
• Sara Bernardini

We focus on incremental compilation-to-SAT procedures (iCTS), a promising way to push the standard CTS approaches beyond their limits. We propose the first comprehensive framework that encompasses all the aspects of an incremental decision procedure, from the encoding to the incremental solver. We apply our guidelines to a real-world CTS approach (Bounded Model Checking) and show how to modify both the generation mechanism of a real BMC tool (NuSMV) and the solving engine of a public-domain SAT solver (SIM). Related approaches and experimental results are discussed as well.