Mostra el registre parcial de l'element
| dc.creator | Ansótegui Gil, Carlos José | |
| dc.creator | Bonet, Maria Luisa | |
| dc.creator | Levy, Jordi | |
| dc.date | 2023 | |
| dc.date.accessioned | 2025-11-03T12:17:07Z | |
| dc.date.available | 2025-11-03T12:17:07Z | |
| dc.identifier | https://doi.org/10.3233/FAIA230707 | |
| dc.identifier | 978-1-64368-449-9 | |
| dc.identifier | https://hdl.handle.net/10459.1/467372 | |
| dc.identifier.uri | http://fima-docencia.ub.edu:8080/xmlui/handle/123456789/24236 | |
| dc.description | 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. | |
| dc.description | This research is part of the projects PROOFS (PID2019-109137GB-C21) and PROOFS BEYOND (PID2022-138506NB-C21) funded by the AEI and MCIN | |
| dc.language | eng | |
| dc.publisher | IOS Press | |
| dc.relation | info:eu-repo/grantAgreement/AEI/Plan Estatal de Investigación Científica y Técnica y de Innovación 2017-2020/PID2019-109137GB-C21/ES/SISTEMAS DE DEMOSTRACION PRACTICOS MAS ALLA DE RESOLUCION/ | |
| dc.relation | info:eu-repo/grantAgreement/AEI/Plan Estatal de Investigación Científica y Técnica y de Innovación 2021-2023/PID2022-138506NB-C21/ES/SATISFACTIBILIDAD Y OPTIMIZACION CON CERTIFICADOS DE PRUEBA MAS ALLA DE RESOLUCION - APLICACIONES (PROOFS BEYOND-A)/ | |
| dc.relation | Reproducció del document publicat a https://doi.org/10.3233/FAIA230707 | |
| dc.relation | Artificial Intelligence Research and Development: Proceedings of the 25th International Conference of the Catalan Association for Artificial Intelligence. Ismael Sanz, Raquel Ros, Jordi Nin (eds.). Amsterdam, The Netherlands : IOS Press, 2023. p. 369-382 | |
| dc.rights | cc-by-nc (c) Carlos Ansótegui, María Luisa Bonet, Jordi Levy, 2023 | |
| dc.rights | Attribution-NonCommercial 4.0 International | |
| dc.rights | info:eu-repo/semantics/openAccess | |
| dc.rights | http://creativecommons.org/licenses/by-nc/4.0/ | |
| dc.subject | SAT | |
| dc.subject | #SAT | |
| dc.subject | Model Counting | |
| dc.subject | Density of States | |
| dc.title | On the Density of States of Boolean Formulas | |
| dc.type | info:eu-repo/semantics/conferenceObject | |
| dc.type | info:eu-repo/semantics/publishedVersion |
| Fitxers | Grandària | Format | Visualització |
|---|---|---|---|
|
No hi ha fitxers associats a aquest element. |
|||