The SAT Revolution: Solving, Sampling, and Counting

Sep 16, 2015

Speakers

About

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.

Organizer

About MATHEMATICAL COLLOQUIUM

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: 31. V. Strassen 32. J. Chayes 33. B. Banaschewski 34. L. H. Kauffman 35. G. Pisier 36. A. Pe lczy ́nski 37. C. Berge 38. V. T. Sós 39. M. Grötschel 40. R. E. Burkard 41. H. S. Wilf 42. M. Waterman 43. M. Sharir 44. E. Specker 45. B. Eckmann 46. T. A. Slaman 47. X. G. Viennot 48. Ch. Praeger 49. K. Ball 50. A. M. Vershik 51. M. Aschbacher 52. M. Emmer 53. E. Friedgut 54. B. Green 55. M. Simonovits 56. K. Schmidt 57. N. Linial 58. G. Kalai 59. E. Szemerédi 60. M. Fiedler 61. D. Foata 62. H. Iwaniec 63. B. Reed 64. A. Louveau 65. V. Bergelson 66. J. Friedlander 67. A. Wigderson 68. V. Rödl 69. J. L. Vázquez 70. S. Solecki 71. R. McKenzie 72. A. Odlyzko 73. R. Graham 74. B. Szegedy 75. M. V. Sapir 76. B. Sudakov 77. M. Waldschmidt 78. V. Guruswami 79. T. Luczak 80. M. L. Balinski 81. G. L. Cherlin 82. B. Bollobás 83. M. Krivelevich 84. V. V. Vazirani 85. R. Williams 86. M. Aizenman 87. G. F. Lawler 88. D. Gaboriau 89. M. Mend`es France 90. I. Ekeland 91. D. Brydges 92. P. van Emde Boas 93. H. Helfgott 94. E. Cand`es 95. K. Ono 96. M. Vardi 97. R. J. Aumann 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.

Store presentation

Should this presentation be stored for 1000 years?

How do we store presentations

Total of 0 viewers voted for saving the presentation to eternal vault which is 0.0%

Sharing

Recommended Videos

Presentations on similar topic, category or speaker