Author name cluster

Cédric Piette

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.

3 papers

1 author row

SAT Conference 2012 Conference Paper

Revisiting Clause Exchange in Parallel SAT Solving

Gilles Audemard
Benoît Hoessen
Saïd Jabbour
Jean-Marie Lagniez
Cédric Piette

Abstract Managing learnt clause database is known to be a tricky task in SAT solvers. In the portfolio framework, the collaboration between threads through learnt clause exchange makes this problem even more difficult to tackle. Several techniques have been proposed in the last few years, but practical results are still in favor of very limited collaboration, or even no collaboration at all. This is mainly due to the difficulty that each thread has to manage a large amount of learnt clauses generated by the other workers. In this paper, we propose new efficient techniques for clause exchanges within a parallel SAT solver. In contrast to most of the current clause exchange methods, our approach relies on both export and import policies, and makes use of recent techniques that proves very effective in the sequential case. Extensive experimentations show the practical interest of the proposed ideas.

Details

ECAI Conference 2008 Conference Paper

Vivifying Propositional Clausal Formulae

Cédric Piette
Youssef Hamadi
Lakhdar Saïs

In this paper, we present a new way to preprocess Boolean formulae in Conjunctive Normal Form (CNF). In contrast to most of the current pre-processing techniques, our approach aims at improving the filtering power of the original clauses while producing a small number of additional and relevant clauses. More precisely, an incomplete redundancy check is performed on each original clauses through unit propagation, leading to either a sub-clause or to a new relevant one generated by the clause learning scheme. This preprocessor is empirically compared to the best existing one in terms of size reduction and the ability to improve a state-of-the-art satisfiability solver.

Details

ECAI Conference 2006 Conference Paper

Extracting MUSes

Éric Grégoire
Bertrand Mazure
Cédric Piette

Minimally unsatisfiable subformulas (in short, MUSes) represent the smallest explanations for the inconsistency of SAT instances in terms of the number of involved clauses. Extracting MUSes can thus prove valuable because it circumscribes the sources of contradiction in an instance. In this paper, a new heuristic-based approach to approximate or compute MUSes is presented. It is shown that it often outperforms current competing ones.

Details