Given a CNF formula with m clauses, and an integer k, where 0 ≤ k ≤ m, a density of states procedure will count the number of truth assignments that falsify exactly k clauses of the formula. We present the first approach to compute the density of states of Boolean formulas exactly. This is the first non-trivial result on this known hard problem. There are previous approaches for computing approximately the density of states of Boolean Formulas [1,2], where the authors point out they are not aware of any complete solver that is able to compute the exact density of states. The present work is the first step to fill this gap. The idea is, given a formula φ and a parameter c, construct a formula φc such that, the number of models of φc is the number of assignments that falsify exactly c clauses of φ. Then, a #SAT solver is used as a black box to count the models of φc. This approach can be also used to compute approximately the density of states by using an approximate #SAT solver. Finally, the method can be extended trivially to deal with Weighted Boolean formulas.

This research is part of the projects PROOFS (PID2019-109137GB-C21) and PROOFS BEYOND (PID2022-138506NB-C21) funded by the AEI and MCIN