Document Open Access Logo

Approximate Model Counting: Is SAT Oracle More Powerful Than NP Oracle?

Authors Diptarka Chakraborty, Sourav Chakraborty, Gunjan Kumar, Kuldeep S. Meel

PDF
Thumbnail PDF

File

LIPIcs.ICALP.2023.123.pdf
  • Filesize: 0.68 MB
  • 17 pages

Document Identifiers

Author Details

Diptarka Chakraborty
  • National University of Singapore, Singapore
Sourav Chakraborty
  • Indian Statistical Institute, Kolkata, India
Gunjan Kumar
  • National University of Singapore, Singapore
Kuldeep S. Meel
  • National University of Singapore, Singapore

Funding

  • Chakraborty, Diptarka: Supported in part by an MoE AcRF Tier 2 grant (MOE-T2EP20221-0009) and Google South & South-East Asia Research Award.
  • Kumar, Gunjan: Supported in part by National Research Foundation Singapore under its NRF Fellowship Programme[NRF-NRFFAI1-2019-0004 ].
  • Meel, Kuldeep S.: Supported in part by National Research Foundation Singapore under its NRF Fellowship Programme[NRF-NRFFAI1-2019-0004 ] and Campus for Research Excellence and Technological Enterprise (CREATE) programme, Ministry of Education Singapore Tier 2 grant MOE-T2EP20121-0011, and Ministry of Education Singapore Tier 1 Grant [R-252-000-B59-114].

Cite AsGet BibTex

Diptarka Chakraborty, Sourav Chakraborty, Gunjan Kumar, and Kuldeep S. Meel. Approximate Model Counting: Is SAT Oracle More Powerful Than NP Oracle?. In 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 261, pp. 123:1-123:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.ICALP.2023.123

Abstract

Given a Boolean formula ϕ over n variables, the problem of model counting is to compute the number of solutions of ϕ. Model counting is a fundamental problem in computer science with wide-ranging applications in domains such as quantified information leakage, probabilistic reasoning, network reliability, neural network verification, and more. Owing to the #P-hardness of the problems, Stockmeyer initiated the study of the complexity of approximate counting. Stockmeyer showed that log n calls to an NP oracle are necessary and sufficient to achieve (ε,δ) guarantees. The hashing-based framework proposed by Stockmeyer has been very influential in designing practical counters over the past decade, wherein the SAT solver substitutes the NP oracle calls in practice. It is well known that an NP oracle does not fully capture the behavior of SAT solvers, as SAT solvers are also designed to provide satisfying assignments when a formula is satisfiable, without additional overhead. Accordingly, the notion of SAT oracle has been proposed to capture the behavior of SAT solver wherein given a Boolean formula, an SAT oracle returns a satisfying assignment if the formula is satisfiable or returns unsatisfiable otherwise. Since the practical state-of-the-art approximate counting techniques use SAT solvers, a natural question is whether an SAT oracle is more powerful than an NP oracle in the context of approximate model counting. The primary contribution of this work is to study the relative power of the NP oracle and SAT oracle in the context of approximate model counting. The previous techniques proposed in the context of an NP oracle are weak to provide strong bounds in the context of SAT oracle since, in contrast to an NP oracle that provides only one bit of information, a SAT oracle can provide n bits of information. We therefore develop a new methodology to achieve the main result: a SAT oracle is no more powerful than an NP oracle in the context of approximate model counting.

Subject Classification

ACM Subject Classification
  • Theory of computation → Oracles and decision trees
Keywords
  • Model counting
  • Approximation
  • Satisfiability
  • NP oracle
  • SAT oracle

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Teodora Baluta, Shiqi Shen, Shweta Shinde, Kuldeep S Meel, and Prateek Saxena. Quantitative verification of neural networks and its security applications. In Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security, pages 1249-1264, 2019. Google Scholar
  2. Mihir Bellare, Oded Goldreich, and Erez Petrank. Uniform generation of NP-witnesses using an NP-oracle. Information and Computation, 163(2):510-526, 2000. Google Scholar
  3. Sourav Chakraborty, Eldar Fischer, Yonatan Goldhirsh, and Arie Matsliah. On the power of conditional samples in distribution testing. SIAM J. Comput., 45(4):1261-1296, 2016. URL: https://doi.org/10.1137/140964199.
  4. Supratik Chakraborty, Kuldeep S Meel, and Moshe Y Vardi. Algorithmic improvements in approximate counting for probabilistic inference: From linear to logarithmic sat calls. Technical report, Rice University, 2016. Google Scholar
  5. Thomas H. Cormen, Charles E. Leiserson, and Ronald L. Rivest. Introduction to Algorithms. The MIT Press and McGraw-Hill Book Company, 1989. Google Scholar
  6. Thomas M. Cover and Joy A. Thomas. Elements of information theory (2. ed.). Wiley, 2006. Google Scholar
  7. Remi Delannoy and Kuldeep S Meel. On almost-uniform generation of SAT solutions: The power of 3-wise independent hashing. In Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science, pages 1-10, 2022. Google Scholar
  8. Leonardo Duenas-Osorio, Kuldeep Meel, Roger Paredes, and Moshe Vardi. Counting-based reliability estimation for power-transmission grids. In Proceedings of the AAAI Conference on Artificial Intelligence, volume 31(1), 2017. Google Scholar
  9. Matthew Fredrikson and Somesh Jha. Satisfiability modulo counting: A new approach for analyzing privacy properties. In Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1-10, 2014. Google Scholar
  10. Carla P Gomes, Ashish Sabharwal, and Bart Selman. Model counting: A new strategy for obtaining good bounds. In AAAI, volume 10, pages 1597538-1597548, 2006. Google Scholar
  11. Mark R Jerrum, Leslie G Valiant, and Vijay V Vazirani. Random generation of combinatorial structures from a uniform distribution. Theoretical computer science, 43:169-188, 1986. Google Scholar
  12. Dan Roth. On the hardness of approximate reasoning. Artificial Intelligence, 82(1-2):273-302, 1996. Google Scholar
  13. Tian Sang, Paul Beame, and Henry A Kautz. Performing bayesian inference by weighted model counting. In AAAI, volume 5, pages 475-481, 2005. Google Scholar
  14. Jonathan Scarlett and Volkan Cevher. An introductory guide to Fano’s inequality with applications in statistical estimation. arXiv preprint, 2019. URL: https://arxiv.org/abs/1901.00555.
  15. Jeanette P Schmidt, Alan Siegel, and Aravind Srinivasan. Chernoff-Hoeffding bounds for applications with limited independence. SIAM Journal on Discrete Mathematics, 8(2):223-250, 1995. Google Scholar
  16. Larry Stockmeyer. The complexity of approximate counting. In Proceedings of the fifteenth annual ACM symposium on Theory of computing, pages 118-126, 1983. Google Scholar
  17. Leslie G Valiant. The complexity of enumeration and reliability problems. SIAM Journal on Computing, 8(3):410-421, 1979. Google Scholar
  18. Andrew Chi-Chin Yao. Probabilistic computations: Toward a unified measure of complexity. In 18th Annual Symposium on Foundations of Computer Science (SFCS 1977), pages 222-227. IEEE Computer Society, 1977. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact