{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,14]],"date-time":"2025-05-14T09:48:41Z","timestamp":1747216121778,"version":"3.40.5"},"reference-count":0,"publisher":"IOS Press","isbn-type":[{"type":"print","value":"9781643684482"},{"type":"electronic","value":"9781643684499"}],"license":[{"start":{"date-parts":[[2023,10,19]],"date-time":"2023-10-19T00:00:00Z","timestamp":1697673600000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-nc\/4.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023,10,19]]},"abstract":"<jats:p>Given a CNF formula with m clauses, and an integer k, where 0 \u2264 k \u2264 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 \u03c6 and a parameter c, construct a formula \u03c6c such that, the number of models of \u03c6c is the number of assignments that falsify exactly c clauses of \u03c6. Then, a #SAT solver is used as a black box to count the models of \u03c6c. 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.<\/jats:p>","DOI":"10.3233\/faia230707","type":"book-chapter","created":{"date-parts":[[2023,10,23]],"date-time":"2023-10-23T08:15:24Z","timestamp":1698048924000},"source":"Crossref","is-referenced-by-count":0,"title":["On the Density of States of Boolean Formulas1"],"prefix":"10.3233","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7727-2766","authenticated-orcid":false,"given":"Carlos","family":"Ans\u00f3tegui","sequence":"first","affiliation":[{"name":"Universitat de Lleida (DIEI, UdL), Lleida, Spain"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1646-7177","authenticated-orcid":false,"given":"Mar\u00eda Luisa","family":"Bonet","sequence":"additional","affiliation":[{"name":"Universitat Polit\u00e8cnica de Catalunya (CS, UPC), Barcelona, Spain"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5883-5746","authenticated-orcid":false,"given":"Jordi","family":"Levy","sequence":"additional","affiliation":[{"name":"Artificial Intelligence Research Institute (IIIA, CSIC), Bellaterra, Spain"}]}],"member":"7437","container-title":["Frontiers in Artificial Intelligence and Applications","Artificial Intelligence Research and Development"],"original-title":[],"link":[{"URL":"https:\/\/ebooks.iospress.nl\/pdf\/doi\/10.3233\/FAIA230707","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,10,23]],"date-time":"2023-10-23T08:15:24Z","timestamp":1698048924000},"score":1,"resource":{"primary":{"URL":"https:\/\/ebooks.iospress.nl\/doi\/10.3233\/FAIA230707"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,10,19]]},"ISBN":["9781643684482","9781643684499"],"references-count":0,"URL":"https:\/\/doi.org\/10.3233\/faia230707","relation":{},"ISSN":["0922-6389","1879-8314"],"issn-type":[{"type":"print","value":"0922-6389"},{"type":"electronic","value":"1879-8314"}],"subject":[],"published":{"date-parts":[[2023,10,19]]}}}