96. matematické kolokvium KAM - Moshe Vardi (Rice University, USA): The SAT revolution: Solving, sampling, and counting

Abstract

For the past 40 years computer scientists generally believed that NP-complete problems are intractable. In particular, Boolean satisfiability (SAT), as a paradigmatic NP-complete problem, has been considered to be intractable. Over the past 20 years, however, there has been a quiet, but dramatic, revolution, and very large SAT instances are now being solved routinely as part of software and hardware design.
In this talk I will review this amazing development and show that we can leverage SAT solving to accomplish other Boolean reasoning tasks. Counting the the number of satisfying truth assignments of a given Boolean formula or sampling such assignments uniformly at random are fundamental computational problems in computer science with numerous applications. While the theory of these problems has been thoroughly investigated in the 1980s, approximation algorithms developed by theoreticians do not scale up to industrial-sized instances. Algorithms used by the industry offer better scalability, but give up certain correctness guarantees to achieve scalability. We describe a novel approach, based on universal hashing and Satisfiability Modulo Theory, that scales to formulas with hundreds of thousands of variable without giving up correctness guarantees.

CV

Moshe Y. Vardi získal Ph.D. na Hebrejské univerzitě v Jeruzalémě a po stážích na Stanfordu a v IBM je od roku 1993 profesorem na Rice University v Houstonu, kde zastával významné akademické funkce. Moshe Vardi je mezinárodně známým vědcem pracujícím na rozhraní matematické logiky a teoretické informatiky. Jeho činnost je mimořádně rozsáhlá a M. Vardi patří v několika oblastech k zakladatelským osobnostem. Jmenujme zde pouze logickou teorii databází, konečnou teorii modelů a teorii automatů v kontextu verifikace programů. Ve všech těchto oblastech publikoval řadu dnes již klasických prací. Mimořádná je i jeho organizační činnost. Životopis uvádí (do roku 2013) účast v 82 programových výborech konferencí a roli organizátora 39 mezinárodních konferencí. Je editorem řady sborníků a 11 mezinárodních časopisů, včetně role vedoucího redaktora Communications of ACM.
Za svou vědeckou činnost Moshe Vardi získal řadu ocenění. Zmiňme zde jen Gödelovu cenu (v r. 2000 spolu s P. Wolperem), tři čestné doktoráty (Saarbrücken, Orléans a UFRGS Brazílie), členství v několika akademiích včetně American Academy of Arts and Sciences (2010) a National Academy of Sciences (2015).
Je to jen malý vzorek jeho rozsáhlé činnosti a mnohostranného působení. Prof. Vardi přednese kolokvium v rámci konference Highlights 2015 a jeho přednáška je určena široké matematické a informatické veřejnosti. Týká se ústředních otázek jeho vědecké práce.

Jaroslav Nešetřil