Author name cluster

Florian Letombe

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.

4 papers

2 author rows

ECAI Conference 2008 Conference Paper

A MAX-SAT Algorithm Portfolio

Paulo J. Matos
Jordi Planes
Florian Letombe
João Marques-Silva 0001

The results of the last MaxSAT Evaluations suggest there is no universal best algorithm for solving MaxSAT, as the fastest solver often depends on the type of instance. Having an oracle able to predict the most suitable MaxSAT solver for a given instance would result in the most robust solver. Inspired by the success of SATzilla for SAT, this paper describes the first approach for a portfolio of algorithms for MaxSAT. Compared to existing solvers, the resulting portfolio can achieve significant performance improvements on a representative set of instances.

Details

SAT Conference 2008 Conference Paper

Improvements to Hybrid Incremental SAT Algorithms

Florian Letombe
João Marques-Silva 0001

Abstract Boolean Satisfiability (SAT) solvers have been successfully applied to a wide range of practical applications, including hardware model checking, software model finding, equivalence checking, and planning, among many others. SAT solvers are also the building block of more sophisticated decision procedures, including Satisfiability Modulo Theory (SMT) solvers. The large number of applications of SAT yields ever more challenging problem instances, and motivate the development of more efficient algorithms. Recent work studied hybrid approaches for SAT, which involves integrating incomplete and complete SAT solvers. This paper proposes a number of improvements to hybrid SAT solvers. Experimental results demonstrate that the proposed optimizations are effective. The resulting algorithms in general perform better and, more importantly, are significantly more robust.

Details

SAT Conference 2005 Conference Paper

A Branching Heuristics for Quantified Renamable Horn Formulas

Sylvie Coste-Marquis
Daniel Le Berre
Florian Letombe

Abstract Many solvers have been designed for \(\mathcal{QBF}\) s, the validity problem for Quantified Boolean Formulas for the past few years. In this paper, we describe a new branching heuristics whose purpose is to promote renamable Horn formulas. This heuristics is based on Hébrard’s algorithm for the recognition of such formulas. We present some experimental results obtained by our qbf solver Qbfl with the new branching heuristics and show how its performances are improved.

Details

AAAI Conference 2005 Conference Paper

Propositional Fragments for Knowledge Compilation and Quantified Boolean Formulae

Sylvie Coste-Marquis
Florian Letombe

Several propositional fragments have been considered so far as target languages for knowledge compilation and used for improving computational tasks from major AI areas (like inference, diagnosis and planning); among them are the (quite influential) ordered binary decision diagrams, prime implicates, prime implicants, “formulae” in decomposable negation normal form. On the other hand, the validity problem QBF for Quantified Boolean Formulae (QBF) has been acknowledged for the past few years as an important issue for AI, and many solvers have been designed for this purpose. In this paper, the complexity of restrictions of QBF obtained by imposing the matrix of the input QBF to belong to such propositional fragments is identified. Both tractability and intractability results (PSPACE-completeness) are obtained.

PDF Details