Computing the Density of States of Boolean Formulas

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.

• Type: Journal
• Year: 2010
• Where: CP
• Authors: Stefano Ermon, Carla P. Gomes, Bart Selman
• Keywords: Artificial Intelligence, Boolean Formula, CP 2010, Markov Chain Monte Carlo, flat Histogram