96 KAM Mathematical Colloquium
Moshe Vardi
Rice University
THE SAT REVOLUTION: SOLVING, SAMPLING, AND COUNTING
Video and slides.
Wednesday September 16, 2015, 16:00, Modra poslucharna, 2nd floor
Karolinum
Celetna 20, Praha 1
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.
O přednášejícím
Moshe Y. Vardi ziskal Ph.D. na Hebrejske univerzite v Jeruzaleme a po
stazich na Stanfordu a v IBM je od roku 1993 profesorem na Rice University v
Houstonu, kde zastaval vyznamne akademicke funkce. Moshe Vardi je mezinarodne
znamym vedcem pracujicim na rozhrani matematicke logiky a teoreticke informatiky.
Jeho cinnost je mimoradne rozsahla a M. Vardi patri v nekolika oblastech k zakladatelskym osobnostem.
Jmenujme zde pouze logickou teorii databazi, konecnou teorii modelu a teorii automatu v kontextu verifikace programu.
Ve vsech techto oblastech publikoval radu dnes jiz klasickych praci. Mimoradna je i jeho organizacni cinnost.
Zivotopis uvadi (do roku 2013) ucast v 82 programovych vyborech konferenci a roli organizatora 39 mezinarodnich
konferenci. Je editorem rady sborniku a 11 mezinarodnich casopisu, vcetne role vedouciho redaktora Communications of ACM.
Za svou vedeckou cinnost Moshe Vardi ziskal radu oceneni.
Zminme zde jen Godelovu cenu (v r. 2000 spolu s P. Wolperem), tri cestne doktoraty
(Saarbrucken, Orleans a UFRGS Brazilie), clenstvi v nekolika akademiich vcetne American
Academy of Arts and Sciences (2010) a National Academy of Sciences (2015).
Je to jen maly vzorek jeho rozsahle cinnosti a mnohostranneho pusobeni. Prof. Vardi prednese
kolokvium v ramci konference Highlights 2015 a jeho prednaska je urcena siroke matematicke a
informaticke verejnosti. Tyka se ustrednich otazek jeho vedecke prace.