Flash Info
Publication du programme PAUSE – ANR Ukraine pour l’accueil de scientifiques ukrainiens et ukrainiennes dans des laboratoires français
BLANC - Blanc

Algorithmes Incomplets pour la réfutation – UNLOC

Résumé de soumission

Dans ce projet, nous proposons de définir des algorithmes cherchant à déterminer l'inconsistance de problèmes NP-Complets. Nous concentrerons particulièrement nos efforts sur le problème SAT, bien connu pour être l'archétype des problèmes NP-Complets. Les problèmes NP-Complets et leur dual, représenté parles problèmes Co-NP complets (la question de la non satisfaisabilité) ont beaucoup été étudiés par la communauté internationale, dans laquelle les chercheurs français y ont pris une part prépondérante. Ces travaux ont portés autant d'un point de vue théorique que pratique avec la mise au point d'algorithmes de plus en plus efficaces. Les aspects théoriques de SAT et UNSAT (et également des autres problèmes NP-Complets comme celui des CSP) sont d'une première importance et sont directement attachés à deux questions scientifiques encore ouvertes des plus cruciales, à savoir est ce que P=NP (Existe--il une méthode qui exhibe tout le temps en temps polynomial un certificat SAT), et est ce que NP=Co-NP (Est ce que un certificat (court) UNSAT peut être exhibé en temps polynomial). Malgré les limites théoriques très dures de ces problèmes, de nombreux progrès ont été réalisés d'un point de vue pratique. Par exemple, une méthode statistique très efficace a été proposée pour résoudre des problèmes aléatoires au seuil. Avec Chaff, proposé en 2001, un nouveau type de méthodes, basé sur l'apprentissage et des heuristiques dynamiques, a été introduit. Ces nouvelles méthodes ont permis de résoudre des problèmes très importants (autant du point de vue de la taille que de celui de l'intérêt) venant de l'industrie, amenant les entreprises a faire de plus en plus de recherche sur ce domaine. Néanmoins, Même si les solveurs incomplets sont une alternative intéressante à la recherche systématique pour la recherche de solutions, aucune d'entre elles n'a pu prouvée efficacement l'inconsistance des problèmes. Du fait de sa relation avec la question NP=Co-NP, ce problème est extrêmement difficile. Néanmoins, les solveurs incomplets pour l'inconsistance représentent une alternative élégante et probablement la prochaine génération de solveurs qui rechercheront des preuves courtes d'inconsistance. L'existence de ces algorithmes représentent l'un des challenges les plus importants et intéressant de la communauté, et nous pensons fermement que de bons résultats, théoriques sur certaines classes de problèmes, et pratiques sur des exemples industriels peuvent être atteint dans ces trois années.

Coordinateur du projet

Laurent SIMON (UNIVERSITE DE PARIS XI [PARIS- SUD])

L'auteur de ce résumé est le coordinateur du projet, qui est responsable du contenu de ce résumé. L'ANR décline par conséquent toute responsabilité quant à son contenu.

Partenaire

UNIVERSITE DE PICARDIE JULES VERNE
CNRS - DELEGATION REGIONALE PROVENCE
CNRS - DELEGATION REGIONALE NORD-PAS-DE-CALAIS ET PICARDIE
UNIVERSITE DE PARIS XI [PARIS- SUD]

Aide de l'ANR 287 000 euros
Début et durée du projet scientifique : - 36 Mois

Liens utiles

Explorez notre base de projets financés

 

 

L’ANR met à disposition ses jeux de données sur les projets, cliquez ici pour en savoir plus.

Inscrivez-vous à notre newsletter
pour recevoir nos actualités
S'inscrire à notre newsletter