Logo IRISA logo Inria

Prochain Exposé

Jeudi 28 juin, 14h en salle Markov

Kuldeep Meel (School of Computing, National University of Singapore)

Beyond NP Revolution

The paradigmatic NP-complete problem of Boolean satisfiability (SAT) solving is a central problem in Computer Science. While the mention of {\SAT} can be traced to early 19th century, efforts to develop practically successful SAT solvers go back to 1950s. The past 20 years have witnessed a "SAT revolution" with the development of conflict-driven clause-learning (CDCL) solvers. Such solvers combine a classical backtracking search with a rich set of effective heuristics. While 20 years ago SAT solvers were able to solve instances with at most a few hundred variables, modern SAT solvers solve instances with up to millions of variables in a reasonable time. The SAT-revolution opens up opportunities to design practical algorithms with rigorous guarantees for problems in complexity classes beyond NP by replacing a NP oracle with a SAT Solver. In this talk, we will discuss how we use SAT revolution to design practical algorithms for two fundamental problems in artificial intelligence and formal methods: Constrained Sampling and Counting.

Exposés des semaines suivantes

Vos propositions sont les bienvenues !

Séminaire autour des thèmes 68NQRT