Article

Maximum model counting

Authors:

Daniel J. Fremont,

Markus N. Rabe,

Sanjit A. SeshiaAuthors Info & Claims

AAAI'17: Proceedings of the Thirty-First AAAI Conference on Artificial Intelligence

Pages 3885 - 3892

Published: 04 February 2017 Publication History

Abstract

We introduce the problem Max#SAT, an extension of model counting (#SAT). Given a formula over sets of variables X, Y, and Z, the Max#SAT problem is to maximize over the variables X the number of assignments to Y that can be extended to a solution with some assignment to Z. We demonstrate that Max#SAT has applications in many areas, showing how it can be used to solve problems in probabilistic inference (marginal MAP), planning, program synthesis, and quantitative information flow analysis. We also give an algorithm which by making only polynomially many calls to an NP oracle can approximate the maximum count to within any desired multiplicative error. The NP queries needed are relatively simple, arising from recent practical approximate model counting and sampling algorithms, which allows our technique to be effectively implemented with a SAT solver. Through several experiments we show that our approach can be successfully applied to interesting problems.

References

[1]

Alur, R.; Bodik, R.; Juniwal, G.; Martin, M. M. K.; Raghothaman, M.; Seshia, S. A.; Singh, R.; Solar-Lezama, A.; Torlak, E.; and Udupa, A. 2013. Syntax-guided synthesis. In IEEE International Conference on Formal Methods in Computer-Aided Design, 1-17.

[2]

Argelich, J.; Li, C.-M.; Manya, F.; and Planes, J. 2008. The first and second Max-SAT evaluations. Journal on Satisfiability, Boolean Modeling and Computation 4:251-278.

[3]

Backes, M.; Köpf, B.; and Rybalchenko, A. 2009. Automatic discovery and quantification of information leaks. In 30th IEEE Symposium on Security and Privacy, 141-153. IEEE.

Digital Library

[4]

Chakraborty, S.; Fremont, D. J.; Meel, K. S.; Seshia, S. A.; and Vardi, M. Y. 2015. On parallel scalable uniform SAT witness generation. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems, 304-319. Springer.

Digital Library

[5]

Chakraborty, S.; Meel, K. S.; and Vardi, M. Y. 2013. A scalable approximate model counter. In Principles and Practice of Constraint Programming, 200-216. Springer.

Digital Library

[6]

Chakraborty, S.; Meel, K. S.; and Vardi, M. Y. 2014. Balancing scalability and uniformity in SAT witness generator. In 51st Design Automation Conference, 1-6. ACM.

Digital Library

[7]

Chakraborty, S.; Meel, K. S.; and Vardi, M. Y. 2016. Algorithmic improvements in approximate counting for probabilistic inference: From linear to logarithmic SAT calls. In Proceedings of the 25th International Joint Conference on Artificial Intelligence (IJCAI-16), 3569-3576.

Digital Library

[8]

Davies, J., and Bacchus, F. 2013. Exploiting the power of MIP solvers in MAXSAT. In Proceedings of Theory and Applications of Satisfiability Testing, 166-181. Springer.

Digital Library

[9]

Dechter, R. 1999. Bucket elimination: A unifying framework for reasoning. Artificial Intelligence 113(1):41-85.

Digital Library

[10]

Ermon, S.; Gomes, C. P.; Sabharwal, A.; and Selman, B. 2013. Taming the curse of dimensionality: Discrete integration by hashing and optimization. In Proceedings of the 30th International Conference on Machine Learning. JMLR: W&CP volume 28.

Digital Library

[11]

Fremont, D. J.; Rabe, M. N.; and Seshia, S. A. 2016. Maximum model counting. Technical Report UCB/EECS-2016-169, EECS Department, University of California, Berkeley.

[12]

Fu, Z., and Malik, S. 2006. On solving the partial MAX-SAT problem. In International Conference on Theory and Applications of Satisfiability Testing, 252-265. Springer.

Digital Library

[13]

Heusser, J., and Malacaria, P. 2010. Quantifying information leaks in software. In 26th Annual Computer Security Applications Conference. ACM.

Digital Library

[14]

Klebanov, V.; Manthey, N.; and Muise, C. J. 2013. SAT-based analysis and quantification of information flow in programs. In Quantitative Evaluation of Systems.

Digital Library

[15]

Köpf, B., and Basin, D. 2007. An information-theoretic model for adaptive side-channel attacks. In Proceedings of the ACM Conference on Computer and Communications Security (CCS 2007), 286-296. ACM.

Digital Library

[16]

Littman, M. L.; Goldsmith, J.; and Mundhenk, M. 1998. The computational complexity of probabilistic planning. Journal of Artificial Intelligence Research 9(1):1-36.

Digital Library

[17]

Marinescu, R.; Dechter, R.; and Ihler, A. 2014. AND/OR search for marginal MAP. In Uncertainty in Artificial Intelligence (UAI), 563-572. Citeseer.

Digital Library

[18]

Marques-Silva, J., and Planes, J. 2011. Algorithms for maximum satisfiability using unsatisfiable cores. In Advanced Techniques in Logic Synthesis, Optimizations and Applications. Springer New York. 171-182.

[19]

Mauá, D. D.; De Campos, C. P.; and Cozman, F. G. 2015. The complexity of map inference in bayesian networks specified through logical languages. Cancer 1:Y2.

[20]

Newsome, J.; McCamant, S.; and Song, D. 2009. Measuring channel capacity to distinguish undue influence. In ACM SIGPLAN Fourth Workshop on Programming Languages and Analysis for Security. ACM.

Digital Library

[21]

Pipatsrisawat, K., and Darwiche, A. 2009. A new d-DNNF-based bound computation algorithm for functional E-MAJSAT. In 21st international jont conference on Artifical intelligence (IJCAI), 590-595.

Digital Library

[22]

Safarpour, S.; Mangassarian, H.; Veneris, A.; Liffiton, M. H.; and Sakallah, K. A. 2007. Improved design debugging using maximum satisfiability. In Proceedigns of the International Conference on Formal Methods in Computer Aided Design (FMCAD), 13-19. IEEE.

Digital Library

[23]

Sang, T.; Beame, P.; and Kautz, H. 2005. Solving bayesian networks by weighted model counting. In Proceedings of the Twentieth National Conference on Artificial Intelligence (AAAI-05), volume 1, 475-482.

Digital Library

[24]

Solar-Lezama, A.; Tancau, L.; Bodík, R.; Seshia, S. A.; and Saraswat, V. A. 2006. Combinatorial sketching for finite programs. In 12th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), 404-415. ACM Press.

Digital Library

[25]

Toda, S. 1991. PP is as hard as the polynomial-time hierarchy. SIAM J. Comput. 20(5):865-877.

Digital Library

[26]

Xue, Y.; Li, Z.; Ermon, S.; Gomes, C. P.; and Selman, B. 2016. Solving marginal map problems with np oracles and parity constraints. In Lee, D. D.; Luxburg, U. V.; Guyon, I.; and Garnett, R., eds., Advances In Neural Information Processing Systems 29. Curran Associates, Inc. 1127-1135.

Digital Library

[27]

Zhang, N. L., and Tian, J., eds. 2014. Proceedings of the Thirtieth Conference on Uncertainty in Artificial Intelligence, UAI 2014, Quebec City, Quebec, Canada, July 23-27, 2014. AUAI Press.

Cited By

Capelli FLagniez JPlank ASeidl MLarson K(2024)A top-down tree model counter for quantified Boolean formulasProceedings of the Thirty-Third International Joint Conference on Artificial Intelligence10.24963/ijcai.2024/205(1853-1861)Online publication date: 3-Aug-2024
https://dl.acm.org/doi/10.24963/ijcai.2024/205
Gao PZhang JSong FWang C(2019)Verifying and Quantifying Side-channel Resistance of Masked Software ImplementationsACM Transactions on Software Engineering and Methodology (TOSEM)10.1145/333039228:3(1-32)Online publication date: 18-Jul-2019
https://dl.acm.org/doi/10.1145/3330392

Recommendations

Pseudorandomness for Approximate Counting and Sampling

We study computational procedures that use both randomness and nondeterminism. The goal of this paper is to derandomize such procedures under the weakest possible assumptions.

Our main technical contribution allows one to "boost" a given hardness ...
Counting Linear Extensions: Parameterizations by Treewidth

We consider the $$\#\hbox {P}$&#P-complete problem of counting the number of linear extensions of a poset $$(\textsc {\#LE})$$(#LE); a fundamental problem in order theory with applications in a variety of distinct areas. In particular, we study the ...
The Complexity of Planar Counting Problems

We prove the #P-hardness of the counting problems associated with various satisfiability, graph, and combinatorial problems, when restricted to planar instances. These problems include 3Sat, 1-3Sat, 1-Ex3Sat, Minimum Vertex Cover, Minimum Dominating Set,...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

AAAI'17: Proceedings of the Thirty-First AAAI Conference on Artificial Intelligence

February 2017

5106 pages

Program Chairs:
Satinder Singh
University of Michigan
,
Shaul Markovitch
Technion-Israel Institute of Technology

Sponsors

Association for the Advancement of Artificial Intelligence
amazon: amazon
Infosys
Facebook: Facebook
IBM: IBM

Publisher

AAAI Press

Publication History

Published: 04 February 2017

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

2
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 05 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

Capelli FLagniez JPlank ASeidl MLarson K(2024)A top-down tree model counter for quantified Boolean formulasProceedings of the Thirty-Third International Joint Conference on Artificial Intelligence10.24963/ijcai.2024/205(1853-1861)Online publication date: 3-Aug-2024
https://dl.acm.org/doi/10.24963/ijcai.2024/205
Gao PZhang JSong FWang C(2019)Verifying and Quantifying Side-channel Resistance of Masked Software ImplementationsACM Transactions on Software Engineering and Methodology (TOSEM)10.1145/333039228:3(1-32)Online publication date: 18-Jul-2019
https://dl.acm.org/doi/10.1145/3330392

View Options

View options

Figures

Tables

Media

View Table of Conten