Algorithmes Incomplets pour la réfutation – UNLOC

In this project, we propose to define incomplete algorithms that will determine the lack of solutions of NP-Complete problems. We will particularly focus our effort on the Satisfiability (SAT) question, which is the canonical NP-Complete problem. With its dual problem, the Co-NP Complete 'Unsatisfiability' question, they have been widely studied from both a theoretical and practical point of view, by an active international community in which the French researchers have always been very prolific. The theoretical aspects of SAT and UNSAT (and other widely studied NP-Complete problems like CSP) are of first importance, and are directly related to some of the most crucial questions of the complexity hierarchy, yet still opened: does NP=P ? (there exists a method that always exhibits a SAT certificate in polynomial time), does NP=Co-NP ? (the UNSAT certificate is 'short', i.e. It can be checked in polynomial time). Despite the very hard theoretical limits of those problems, a lot of impressive progress was made. For instance, the in-depth structure of random problems has allowed to exhibit a statistical method to efficiently solve SAT random problems, just before the SAT/UNSAT threshold. With Chaff, in 2001, a new paradigm has emerged, based on efficient clause learning. This formalism allowed huge problems, coming from industry, to be efficiently solved by the SAT/UNSAT approach, and pushed forward the interest of the industry for efficient SAT/UNSAT solvers. However, if incomplete solvers have been shown to be a powerful alternative to a systematic search for solutions, no incomplete framework has yet been proposed to efficiently prove the inconsistency of problems. With its relationship to the NP=Co-NP question, this problem is extremely hard. However, incomplete solvers for inconsistency represent an elegant alternative and probably the next generation of solvers that will look for short proofs. If they tackle one of the main challenging questions that face the whole community, good theoretical results on particular classes of problems and very good practical results can be reached in a relatively short time.