Dear all,
This is a short reminder about the talk of Kuldeep Meel (NUS Singapore)https://www.unravel.rwth-aachen.de/cms/UnRAVeL/Das-Graduiertenkolleg/Gastwissenschaftlerinnen-und-wissenscha/Gaeste/~kfsjo/Kuldeep-Meel/ today at 10:30.
Title: Sparse Hashing for Scalable Approximate Model Counting: When Theory and Practice Finally Meet
Given a Boolean formula F, the problem of model counting, also referred to as #SAT, is to compute the number of solutions of F. The hashing-based techniques for approximatecounting have emerged as a dominant approach, promising achievement of both scalability and rigorous theoretical guarantees. The standard construction of strongly 2-universal hash functions employs dense XORs (i.e., involving half of the variables in expectation), which is widely known to cause degradation in the runtime performance of state of the art SAT solvers.
Consequently, the past few years have witnessed an intense activity in the design of sparse XORs as hash functions. In this talk, we will first survey the known results, and identify the crucial bottleneck contributing to their lack of ability to provide speedups. We will then formalize a relaxation of universal hashing, called concentrated hashing, and establish a novel and beautiful connection between concentration measures of these hash functions and isoperimetric inequalities on boolean hypercubes. This allows us to obtain tight bounds on variance as well as the dispersion index and show that logarithmically sized XORs suffices for the design of sparse hash functions belonging concentrated hash family. Finally, we use sparse hash functions belonging to this concentrated hash family to develop new approximate counting algorithms. Our comprehensive experimental evaluation of our algorithm on 1896 benchmarks with computational effort of over 20,000 computational hours demonstrates speedup compared to existing approaches. To the best of our knowledge, this work is the first study to demonstrate runtime improvement of approximate model counting algorithms through the usage of sparse hash functions, while still retaining strong theoretical guarantees.
(Based on Joint work with S. Akshay, D. Agarwal, and Bhavishya; The corresponding papers were published at SAT-20 and LICS-20)
Bio:
Kuldeep Meel is Sung Kah Kay Assistant Professor of Computer Science in School of Computing at the National University of Singapore. He received his Ph.D. (2017) and M.S. (2014) degree from Rice University, and B. Tech. (with Honors) degree (2012) in Computer Science and Engineering from Indian Institute of Technology, Bombay. He is a recipient of 2019 NRF Fellowship for AI. His research interests lie at the intersection of Artificial Intelligence and Formal Methods. His work received the 2018 Ralph Budd Award for Best PhD Thesis in Engineering, 2014 Outstanding Masters Thesis Award from Vienna Center of Logic and Algorithms and Best Student Paper Award at CP 201
Wednesday, 2.12.2020, 10:30 https://rwth.zoom.us/j/92047949381?pwd=LzIwUW96WEM0MkRjZ01FUmhwd1I3QT09https://www.google.com/url?q=https://rwth.zoom.us/j/92047949381?pwd%3DLzIwUW96WEM0MkRjZ01FUmhwd1I3QT09&sa=D&source=calendar&usd=2&usg=AOvVaw0iFckZC1okM60BGh22QEGz Meeting ID: 920 4794 9381 Password: unravel https://www.unravel.rwth-aachen.de/go/id/kfsgc
Best regards Helen Bolke-Hermanns
Helen Bolke-Hermanns RTG UnRAVeL - RWTH Aachen University Ahornstr. 55, D-52074 Aachen Building E3, 2nd floor, Room 9218 Telefon: +49 (241) 80-21 004 Fax: +49 (241) 80-22 215 E-Mail: Helen.Bolke-Hermanns@Informatik.RWTH-Aachen.demailto:Helen.Bolke-Hermanns@Informatik.RWTH-Aachen.de Web: www.unravel.rwth-aachen.dehttp://www.unravel.rwth-aachen.de/
[rwth_unravel_en_rgb]
