Approximate weighted model integration on DNF structures
Weighted model counting consists of computing the weighted sum of all satisfying assignments of a propositional formula. Weighted model counting is well-known to be #P-hard for exact solving, but admits a fully polynomial randomized approximation scheme when restricted to DNF structures. In this wor...
| Main Authors: | , , |
|---|---|
| Format: | Journal article |
| Language: | English |
| Published: |
Elsevier
2022
|
| _version_ | 1826312536254840832 |
|---|---|
| author | Abboud, R Ceylan, İİ Dimitrov, R |
| author_facet | Abboud, R Ceylan, İİ Dimitrov, R |
| author_sort | Abboud, R |
| collection | OXFORD |
| description | Weighted model counting consists of computing the weighted sum of all satisfying assignments of a propositional formula. Weighted model counting is well-known to be #P-hard for exact solving, but admits a fully polynomial randomized approximation scheme when restricted to DNF structures. In this work, we study weighted model integration, a generalization of weighted model counting which involves real variables in addition to propositional variables, and pose the following question: Does weighted model integration on DNF structures admit a fully polynomial randomized approximation scheme? Building on classical results from approximate weighted model counting and approximate volume computation, we show that weighted model integration on DNF structures can indeed be approximated for a class of weight functions. Our approximation algorithm is based on three subroutines, each of which can be a weak (i.e., approximate), or a strong (i.e., exact) oracle, and in all cases, comes along with accuracy guarantees. We experimentally verify our approach over randomly generated DNF instances of varying sizes, and show that our algorithm scales to large problem instances, involving up to 1K variables, which are currently out of reach for existing, general-purpose weighted model integration solvers. |
| first_indexed | 2024-03-07T08:27:22Z |
| format | Journal article |
| id | oxford-uuid:3b540327-c8e1-4c1b-92cc-1ab139bf2fea |
| institution | University of Oxford |
| language | English |
| last_indexed | 2024-04-09T03:55:53Z |
| publishDate | 2022 |
| publisher | Elsevier |
| record_format | dspace |
| spelling | oxford-uuid:3b540327-c8e1-4c1b-92cc-1ab139bf2fea2024-03-14T14:16:15ZApproximate weighted model integration on DNF structuresJournal articlehttp://purl.org/coar/resource_type/c_dcae04bcuuid:3b540327-c8e1-4c1b-92cc-1ab139bf2feaEnglishSymplectic ElementsElsevier2022Abboud, RCeylan, İİDimitrov, RWeighted model counting consists of computing the weighted sum of all satisfying assignments of a propositional formula. Weighted model counting is well-known to be #P-hard for exact solving, but admits a fully polynomial randomized approximation scheme when restricted to DNF structures. In this work, we study weighted model integration, a generalization of weighted model counting which involves real variables in addition to propositional variables, and pose the following question: Does weighted model integration on DNF structures admit a fully polynomial randomized approximation scheme? Building on classical results from approximate weighted model counting and approximate volume computation, we show that weighted model integration on DNF structures can indeed be approximated for a class of weight functions. Our approximation algorithm is based on three subroutines, each of which can be a weak (i.e., approximate), or a strong (i.e., exact) oracle, and in all cases, comes along with accuracy guarantees. We experimentally verify our approach over randomly generated DNF instances of varying sizes, and show that our algorithm scales to large problem instances, involving up to 1K variables, which are currently out of reach for existing, general-purpose weighted model integration solvers. |
| spellingShingle | Abboud, R Ceylan, İİ Dimitrov, R Approximate weighted model integration on DNF structures |
| title | Approximate weighted model integration on DNF structures |
| title_full | Approximate weighted model integration on DNF structures |
| title_fullStr | Approximate weighted model integration on DNF structures |
| title_full_unstemmed | Approximate weighted model integration on DNF structures |
| title_short | Approximate weighted model integration on DNF structures |
| title_sort | approximate weighted model integration on dnf structures |
| work_keys_str_mv | AT abboudr approximateweightedmodelintegrationondnfstructures AT ceylanii approximateweightedmodelintegrationondnfstructures AT dimitrovr approximateweightedmodelintegrationondnfstructures |