Democratizing SAT Solving
23/09/2022
Speaker
Abstract
Boolean satisfiability is a fundamental problem in computer science with a wide range of applications including planning, configuration management, design and verification of software/hardware systems. The annual SAT competition continues to witness impressive improvements in the performance of the winning SAT solvers largely thanks to the development of new heuristics arising out of intensive collaborative research in the SAT community. Modern SAT solvers achieve scalability and robustness with complex heuristics that are challenging to understand and explain. Consequently, the development of new algorithmic insights has been largely restricted to experts in the SAT community.I will describe our project that boldly aims to democratise the design of SAT solvers. In particular, our project, called CrystalBall, seeks to develop a framework to provide white-box access to the execution of SAT solver that can aid both SAT solver developers and users to synthesize algorithmic heuristics for modern SAT solvers? We view modern conflict-driven clause learning (CDCL) solvers as a composition of classifiers and regressors for different tasks such as branching, clause memory management, and restarting, and we aim to provide a data-driven automated heuristic design mechanism that can allow experts in domains outside SAT community to contribute to the development of SAT solvers.
Bio
Kuldeep Meel holds the NUS Presidential Young Professorship in the School of Computing at the National University of Singapore. His research interests lie at the intersection of Formal Methods and Artificial Intelligence. He is a recipient of the 2019 NRF Fellowship for AI and was named AI's 10 to Watch by IEEE Intelligent Systems in 2020. His research program's recent recognitions include the 2022 CACM Research Highlight Award, 2022 ACM SIGMOD Research Highlight, IJCAI-22 Early Career Spotlight, 2021 Amazon Research Award, "Best of PODS-21" invite from ACM TODS, "Best Papers of CAV-20" invite from FMSD journal, IJCAI-19 Sister conferences best paper award track invitation.