Olivier Fourdrinoy,

Université d’Artois –

Abstract:

Whereas computing a sat instance consists in checking whether the instance is consistent or not, computing kernels of an inconsistent sat instance consists in finding Minimally Unsatisfiable Subformulae (MUS). In this presentation, local search is used to locate the inconsistency of an instance and finally to locate MUS.

 

Date: 2006-Apr-11     Time: 16:00:00     Room: 217

For more information: