Sep 16, 2015
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 le-verage 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 com-puter 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 Satisfiabi-lity Modulo Theory, that scales to formulas with hundreds of thousands of variable without giving up correctness guarantees.
THE MATHEMATICAL COLLOQUIUM - Since 1987, Matematicko-fyzikální fakulta, Univerzita Karlova v Praze. Při této příležitosti stručně nastíníme poslání a historii těchto přednášek. První kolokvium se konalo v roce 1987. Základní myšlenkou byla snaha po uskutečnění serie „velkých přednášekÿ, které by byly určeny co nejširší matematické obci. Při frekvenci zhruba jedné až dvou přednášek za semestr byla přednesena tato kolokvia: 121. E. Hrushovski 120. M. Arbib 119. R. Paturi 118. Z. Dvořák 117. M. Abért 116. A. Schrijver 115. - 114. S. Lando 113. Ch. Krattenthaler, E. Viklický 112. M. Noy 111. M. Szegedy 110. U.Feige 109. M. Thorup 108. R. J. Auman 107. V. Svěrák 106. Ch. H. Papadimitriou 105. M. Naor 104. B. Zilber 103. V. Vu 102. J.-B. Lasserre 101. A. Jung 100. J. Nešetřil 99. J. Fox 98. C. Pomerance 97. B. Weiss 96. M. Vardi 95. K. Ono 94. E. Candès 93. H. Helfgott 92. P. van Emde Boas 91. D. Brydges 90. I. Ekeland 89. M. Mendès France 88. D. Gaboriau 87. G. F. Lawler 86. M. Aizenman 85. R. Williams 84. V. V. Vazirani 83. M. Krivelevich 82. B. Bollobás 81. G. L. Cherlin 80. M. L. Balinski 79. T. Luczak 78. V. Guruswami 77. M. Waldschmidt 76. B. Sudakov 75. M. V. Sapir 74. B. Szegedy 73. R. Graham 72. A. Odlyzko 71. R. McKenzie 70. S. Solecki 69. J. L. Vázquez 68. V. Rödl 67. A. Wigderson 66. J. Friedlander 65. V. Bergelson 64. A. Louveau 63. B. Reed 62. H. Iwaniec 61. D. Foata 60. M. Fiedler 59. E. Szemerédi 58. G. Kalai 57. N. Linial 56. K. Schmidt 55. M. Simonovits 54. B. Green 53. E. Friedgut 52. M. Emmer 51. M. Aschbacher 50. A. M. Vershik 49. K. Ball 48. Ch. Praeger 47. X. G. Viennot 46. T. A. Slaman 45. B. Eckmann 44. E. Specker 43. M. Sharir 42. M. Waterman 41. H. S. Wilf 40. R. E. Burkard 39. M. Grötschel 38. V. T. Sós 37. C. Berge 36. A. Pełczyński 35. G. Pisier 34. L. H. Kauffman 33. B. Banaschewski 32. J. Chayes 31. V. Strassen 30. J. Nekovář 29. D. Preiss 28. B. Mandelbrot 27. M. Laczkovich 26. P. L. Cameron 25. A. Schnitzel 24. J. Lindenstrauss 23. J. Spencer 22. V. Klee 21. N. Alon 20. A. Borel 19. C. Thomassen 18. J. J. Kohn 17. S. Todorčevič 16. K. Mehlhorn 15. S. Cook 14. H. Fürstenberg 13. J. G. Thompson 12. D. J. A. Welsh 11. G. Choquet 10. V. G. Kac 9. J. Seidel 8. B. Korte 7. V. Chvátal 6. H. Bauer 5. F. Hirzebruch 4. A. Ambrosetti 3. R. Tijdeman 2. P. Erdös 1. L. Lovász Témata přednášek zahrnovala většinu matematických oborů od matematické analýzy a aplikované matematiky přes algebru, až po teoretickou informatiku a diskrétní matematiku. Podle mínění mnoha zúčastněných měly některé přednášky mimořádnou úroveň. KAM, ITI a IUUK jsou otevřeny individuálním návrhům na kandidáty pro budoucí kolokvia. Jak vidno z dosavadní historie, základním kritériem je úroveň přednášejícího.
Professional recording and live streaming, delivered globally.
Presentations on similar topic, category or speaker