Document Open Access Logo

Scalable Precise Computation of Shannon Entropy

Authors Yong Lai , Haolong Tong , Zhenghang Xu , Minghao Yin

PDF HTML 5

Files

Thumbnail PDF
PDF
LIPIcs.SAT.2025.20.pdf
  • Filesize: 1.2 MB
  • 19 pages
HTML5 Logo HTML (experimental)
LIPIcs.SAT.2025.20.html

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Constraint and logic programming
Keywords
  • Knowledge Compilation
  • Algebraic Decision Diagrams
  • Quantitative Information Flow
  • Shannon Entropy

Metrics

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

Abstract

Quantitative information flow analyses (QIF) are a class of techniques for measuring the amount of confidential information leaked by a program to its public outputs. Shannon entropy is an important method to quantify the amount of leakage in QIF. This paper focuses on the programs modeled in Boolean constraints and optimizes the two stages of the Shannon entropy computation to implement a scalable precise tool PSE. In the first stage, we design a knowledge compilation language called ADD[∧] that combines Algebraic Decision Diagrams and conjunctive decomposition. ADD[∧] avoids enumerating possible outputs of a program and supports tractable entropy computation. In the second stage, we optimize the model counting queries that are used to compute the probabilities of outputs. We compare PSE with the state-of-the-art probabilistic approximately correct tool EntropyEstimation, which was shown to significantly outperform the previous precise tools. The experimental results demonstrate that PSE solved 56 more benchmarks compared to EntropyEstimation in a total of 459. For 98% of the benchmarks that both PSE and EntropyEstimation solved, PSE is at least 10× as efficient as EntropyEstimation.

Cite As Get BibTex

Yong Lai, Haolong Tong, Zhenghang Xu, and Minghao Yin. Scalable Precise Computation of Shannon Entropy. In 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 341, pp. 20:1-20:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.SAT.2025.20

Author Details

Yong Lai
  • Key Laboratory of Symbolic Computation and Knowledge Engineering Ministry of Education, Jilin University, Changchun, China
Haolong Tong
  • College of Computer Science and Technology, Jilin University, Changchun, China
Zhenghang Xu
  • School of Computer Science and Information Technology, Northeast Normal University, Changchun, China
Minghao Yin
  • School of Computer Science and Information Technology, Northeast Normal University, Changchun, China

Funding

This work was supported in part by Jilin Provincial Natural Science Foundation [20240101378JC], Jilin Provincial Education Department Research Project [JJKH20241286KJ], and the National Natural Science Foundation of China [U22A2098, 62172185, and 61976050].

Acknowledgements

The authors thank the anonymous reviewers for their constructive feedback.

Supplementary Materials

References

  1. Michael Backes, Matthias Berg, and Boris Köpf. Non-uniform distributions in quantitative information-flow. In Proceedings of the 6th ACM Symposium on Information, Computer and Communications Security, pages 367-375, 2011. URL: https://doi.org/10.1145/1966913.1966960.
  2. Michael Backes, Boris Köpf, and Andrey Rybalchenko. Automatic discovery and quantification of information leaks. In 2009 30th IEEE Symposium on Security and Privacy, pages 141-153. IEEE, 2009. URL: https://doi.org/10.1109/SP.2009.18.
  3. R Iris Bahar, Erica A Frohm, Charles M Gaona, Gary D Hachtel, Enrico Macii, Abelardo Pardo, and Fabio Somenzi. Algebric decision diagrams and their applications. Formal methods in system design, 10:171-206, 1997. URL: https://doi.org/10.1023/A:1008699807402.
  4. Randal E Bryant. Graph-based algorithms for boolean function manipulation. Computers, IEEE Transactions on, 100(8):677-691, 1986. URL: https://doi.org/10.1109/TC.1986.1676819.
  5. Pavol Cernỳ, Krishnendu Chatterjee, and Thomas A Henzinger. The complexity of quantitative information flow problems. In 2011 IEEE 24th Computer Security Foundations Symposium, pages 205-217. IEEE, 2011. Google Scholar
  6. Mark Chavira, Adnan Darwiche, and Manfred Jaeger. Compiling relational Bayesian networks for exact inference. International Journal of Approximate Reasoning, 42(1-2):4-20, 2006. URL: https://doi.org/10.1016/J.IJAR.2005.10.001.
  7. Arthur Choi, Doga Kisa, and Adnan Darwiche. Compiling probabilistic graphical models using sentential decision diagrams. In Symbolic and Quantitative Approaches to Reasoning with Uncertainty: 12th European Conference, ECSQARU 2013, Utrecht, The Netherlands, July 8-10, 2013. Proceedings 12, pages 121-132. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-39091-3_11.
  8. Adnan Darwiche. New advances in compiling CNF to decomposable negation normal form. In Proc. of ECAI, pages 328-332. Citeseer, 2004. Google Scholar
  9. Adnan Darwiche. Modeling and reasoning with Bayesian networks. Cambridge university press, 2009. Google Scholar
  10. Adnan Darwiche and Pierre Marquis. A knowledge compilation map. Journal of Artificial Intelligence Research, 17:229-264, 2002. URL: https://doi.org/10.1613/JAIR.989.
  11. Dorothy Elizabeth Robling Denning. Cryptography and data security, volume 112. Addison-Wesley Reading, 1982. Google Scholar
  12. Jeffrey Dudek, Vu Phan, and Moshe Vardi. ADDMC: weighted model counting with algebraic decision diagrams. In Proceedings of the AAAI Conference on Artificial Intelligence, volume 34, pages 1468-1476, 2020. URL: https://doi.org/10.1609/AAAI.V34I02.5505.
  13. Hélène Fargier, Pierre Marquis, Alexandre Niveau, and Nicolas Schmidt. A knowledge compilation map for ordered real-valued decision diagrams. In Proceedings of the AAAI Conference on Artificial Intelligence, volume 28, 2014. Google Scholar
  14. Daniel Fremont, Markus Rabe, and Sanjit Seshia. Maximum model counting. In Proceedings of the AAAI Conference on Artificial Intelligence, volume 31, 2017. Google Scholar
  15. Priyanka Golia, Brendan Juba, and Kuldeep S Meel. A scalable Shannon entropy estimator. In International Conference on Computer Aided Verification, pages 363-384. Springer, 2022. URL: https://doi.org/10.1007/978-3-031-13185-1_18.
  16. James W Gray III. Toward a mathematical foundation for information flow security. Journal of Computer Security, 1(3-4):255-294, 1992. Google Scholar
  17. Jesse Hoey, Robert St-Aubin, Alan Hu, and Craig Boutilier. SPUDD: Stochastic planning using decision diagrams. arXiv preprint, 2013. URL: https://arxiv.org/abs/1301.6704.
  18. Manfred Jaeger. Probabilistic decision graphs - Combining verification and AI techniques for probabilistic inference. International Journal of Uncertainty, Fuzziness and Knowledge-Based Systems, 12(supp01):19-42, 2004. URL: https://doi.org/10.1142/S0218488504002564.
  19. Vladimir Klebanov, Norbert Manthey, and Christian Muise. SAT-based analysis and quantification of information flow in programs. In International Conference on Quantitative Evaluation of Systems, pages 177-192. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-40196-1_16.
  20. Tuukka Korhonen and Matti Järvisalo. Integrating tree decompositions into decision heuristics of propositional model counters. In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021), pages 8:1-8:11. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.CP.2021.8.
  21. Marta Kwiatkowska, Gethin Norman, and David Parker. Stochastic model checking. Formal Methods for Performance Evaluation: 7th International School on Formal Methods for the Design of Computer, Communication, and Software Systems, SFM 2007, Bertinoro, Italy, May 28-June 2, 2007, Advanced Lectures 7, pages 220-270, 2007. URL: https://doi.org/10.1007/978-3-540-72522-0_6.
  22. Jean-Marie Lagniez and Pierre Marquis. On preprocessing techniques and their impact on propositional model counting. Journal of Automated Reasoning, 58:413-481, 2017. URL: https://doi.org/10.1007/S10817-016-9370-8.
  23. Yong Lai, Dayou Liu, and Shengsheng Wang. Reduced ordered binary decision diagram with implied literals: A new knowledge compilation approach. Knowledge and Information Systems, 35:665-712, 2013. URL: https://doi.org/10.1007/S10115-012-0525-6.
  24. Yong Lai, Dayou Liu, and Minghao Yin. New canonical representations by augmenting obdds with conjunctive decomposition. Journal of Artificial Intelligence Research, 58:453-521, 2017. URL: https://doi.org/10.1613/JAIR.5271.
  25. Yong Lai, Kuldeep S Meel, and Roland HC Yap. The power of literal equivalence in model counting. In Proceedings of the AAAI Conference on Artificial Intelligence, volume 35, pages 3851-3859, 2021. Google Scholar
  26. Yong Lai, Zhenghang Xu, and Minghao Yin. Pbcounter: weighted model counting on pseudo-boolean formulas. Frontiers of Computer Science, 19(3):193402, 2025. URL: https://doi.org/10.1007/S11704-024-3631-1.
  27. Nian-Ze Lee, Yen-Shi Wang, and Jie-Hong R Jiang. Solving exist-random quantified stochastic boolean satisfiability via clause selection.c. In IJCAI, pages 1339-1345, 2018. URL: https://doi.org/10.24963/IJCAI.2018/186.
  28. Enrico Macii and Massimo Poncino. Exact computation of the entropy of a logic circuit. In Proceedings of the Sixth Great Lakes Symposium on VLSI, pages 162-167. IEEE, 1996. URL: https://doi.org/10.1109/GLSV.1996.497613.
  29. Ziyuan Meng and Geoffrey Smith. Calculating bounds on information leakage using two-bit patterns. In Proceedings of the ACM SIGPLAN 6th Workshop on Programming Languages and Analysis for Security, pages 1-12, 2011. Google Scholar
  30. Quoc-Sang Phan, Pasquale Malacaria, Oksana Tkachuk, and Corina S Păsăreanu. Symbolic quantitative information flow. ACM SIGSOFT Software Engineering Notes, 37(6):1-5, 2012. URL: https://doi.org/10.1145/2382756.2382791.
  31. Tian Sang, Paul Beame, and Henry Kautz. Heuristics for fast exact model counting. In Theory and Applications of Satisfiability Testing: 8th International Conference, SAT 2005, St Andrews, UK, June 19-23, 2005. Proceedings 8, pages 226-240. Springer, 2005. URL: https://doi.org/10.1007/11499107_17.
  32. Shubham Sharma, Subhajit Roy, Mate Soos, and Kuldeep S Meel. GANAK: A Scalable Probabilistic Exact Model Counter. In IJCAI, volume 19, pages 1169-1176, 2019. URL: https://doi.org/10.24963/IJCAI.2019/163.
  33. Geoffrey Smith. On the foundations of quantitative information flow. In International Conference on Foundations of Software Science and Computational Structures, pages 288-302. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-00596-1_21.
  34. Ziqiao Zhou, Zhiyun Qian, Michael K Reiter, and Yinqian Zhang. Static evaluation of noninterference using approximate model counting. In 2018 IEEE Symposium on Security and Privacy (SP), pages 514-528. IEEE, 2018. URL: https://doi.org/10.1109/SP.2018.00052.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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