As a guest user you are not logged in or recognized by your IP address. You have
access to the Front Matter, Abstracts, Author Index, Subject Index and the full
text of Open Access publications.
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 website uses cookies
We use cookies to provide you with the best possible experience. They also allow us to analyze user behavior in order to constantly improve the website for you. Info about the privacy policy of IOS Press.
This website uses cookies
We use cookies to provide you with the best possible experience. They also allow us to analyze user behavior in order to constantly improve the website for you. Info about the privacy policy of IOS Press.