Abstract
In this paper we consider the problem of computing the density of states of a Boolean formula in CNF, a generalization of both MAX-SAT and model counting. Given a Boolean formula F, its density of states counts the number of configurations that violate exactly E clauses, for all values of E. We propose a novel Markov Chain Monte Carlo algorithm based on flat histogram methods that, despite the hardness of the problem, converges quickly to a very accurate solution. Using this method, we show the first known results on the density of states of several widely used formulas and we provide novel insights about the behavior of random 3-SAT formulas around the phase transition.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Gogate, V., Dechter, R.: Approximate counting by sampling the backtrack-free search space. In: Proc. of AAAI-2007, pp. 198–203 (2007)
Gomes, C., Hoffmann, J., Sabharwal, A., Selman, B.: From sampling to model counting. In: Proceedings of the 20th International Joint Conference on Artificial Intelligence, IJCAI 2007 (2007)
Gomes, C., Sabharwal, A., Selman, B.: Model counting: a new strategy for obtaining good bounds. In: Proceedings of AAAI 2006, pp. 54–61. AAAI Press, Menlo Park (2006)
Littman, M., Majercik, S., Pitassi, T.: Stochastic boolean satisfiability. Journal of Automated Reasoning 27(3), 251–296 (2001)
Sang, T., Beame, P., Kautz, H.: Solving Bayesian networks by weighted model counting. In: Proc. of AAAI 2005, pp. 475–481 (2005)
Hansen, P., Jaumard, B.: Algorithms for the maximum satisfiability problem. Computing 44(4), 279–303 (1990)
Wang, F., Landau, D.: Efficient, multiple-range random walk algorithm to calculate the density of states. Physical Review Letters 86(10), 2050–2053 (2001)
Belaidouni, M., Hao, J.K.: Sat, local search dynamics and density of states. In: Selected Papers from the 5th European Conference on Artificial Evolution, pp. 192–204. Springer, Heidelberg (2002)
Rosé, H., Ebeling, W., Asselmeyer, T.: The density of states - a measure of the difficulty of optimisation problems. In: Ebeling, W., Rechenberg, I., Voigt, H.-M., Schwefel, H.-P. (eds.) PPSN 1996. LNCS, vol. 1141, pp. 208–217. Springer, Heidelberg (1996)
Wei, W., Erenrich, J., Selman, B.: Towards efficient sampling: Exploiting random walk strategies. In: Proceedings of the 19th National Conference on Artifical Intelligence, pp. 670–676. AAAI Press, Menlo Park (2004)
Kamath, A., Motwani, R., Palem, K., Spirakis, P.: Tail bounds for occupancy and the satisfiability threshold conjecture. In: Proc. of the 35th Annual Symposium on the Foundations of Computer Science, pp. 592–603 (1994)
Monasson, R., Zecchina, R.: Entropy of the K-satisfiability problem. Physical review letters 76(21), 3881–3885 (1996)
Montanari, A., Shah, D.: Counting good truth assignments of random k-SAT formulae. In: Proc. of the 18th ACM Symposium on Discrete Algorithms (2007)
Sang, T., Bacchus, F., Beame, P., Kautz, H., Pitassi, T.: Combining component caching and clause learning for effective model counting. In: Proc. of SAT 2004 (2004)
Hoos, H., Stiitzle, T.: SATLlB: An Online Resource for Research on SAT. In: Sat 2000: Highlights of Satisfiability Research in the Year, p. 283 (2000)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ermon, S., Gomes, C.P., Selman, B. (2010). Computing the Density of States of Boolean Formulas. In: Cohen, D. (eds) Principles and Practice of Constraint Programming – CP 2010. CP 2010. Lecture Notes in Computer Science, vol 6308. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-15396-9_6
Download citation
DOI: https://doi.org/10.1007/978-3-642-15396-9_6
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-15395-2
Online ISBN: 978-3-642-15396-9
eBook Packages: Computer ScienceComputer Science (R0)