The Rise of Model Counting: A Child of SAT Revolution

摘要

The paradigmatic NP-complete problem of Boolean satisfiability (SAT) is a central problem in Computer Science. The past 20 years have witnessed a SAT revolution with the development of conflict-driven clause-learning (CDCL) SAT solvers. Such solvers combine a classical backtracking search with a rich set of effective heuristics. While 20 years ago SAT solvers were able to solve instances with at most a few hundred variables, modern SAT solvers solve instances with up to millions of variables in a reasonable time. The SAT revolution opens up opportunities to design practical algorithms with rigorous guarantees for problems in complexity classes beyond NP by replacing a NP oracle with a SAT Solver. In this talk, we will discuss how we use SAT revolution to design practical algorithms for one of the fundamental problems in formal methods and artificial intelligence: model counting. Model counting is a fundamental computational problem with applications in diverse areas spanning neural network verification, reliability estimation, explainable AI, probabilistic inference, security vulnerability analysis, and the like. While counting has been studied extensively by theoreticians for the past three decades. Yet, in spite of this extensive study, it has been extremely difficult to reduce this theory to practice. We examine how the process of revisiting and refining the theory to leverage the SAT revolution has led to the development of the first scalable framework for model counting: ApproxMC 11-4]. ApproxMC1 can handle industrial-scale problem instances involving hundreds of thousands of variables, while providing provably strong approximation guarantees.