Centrality Heuristics for Exact Model Counting

Bernhard Bliem, Matti Järvisalo

Tutkimustuotos: Artikkeli kirjassa/raportissa/konferenssijulkaisussaKonferenssiartikkeliTieteellinenvertaisarvioitu

Abstrakti

Model counting is the archetypical #P-complete problem consisting of determining the number of satisfying truth assignments of a given propositional formula. In this short paper, we empirically investigate the potential of employing graph centrality measures as a basis of search heuristics in the context of exact model counting. In particular, we integrate centrality-based heuristics into the search-based exact model counter sharpSAT. Our experiments show that employing centrality information significantly improves the empirical performance of sharpSAT, and also allows for simplifying the search heuristics compared to the current default heuristics of the model counter. In particular, we show that the VSIDS heuristic, which is an integral search heuristic employed in essentially all state-of-the-art conflict-driven clause learning Boolean satisfiability solvers, appears to be of very limited use in the context of model counting.

Alkuperäiskielienglanti
OtsikkoIEEE 31st International Conference on Tools with Artificial Intelligence (ICTAI 2019)
Sivumäärä5
KustantajaIEEE Computer Society
Julkaisupäivä13 helmikuuta 2020
Sivut59-63
ISBN (painettu)978-1-7281-3799-5
ISBN (elektroninen)978-1-7281-3798-8
DOI - pysyväislinkit
TilaJulkaistu - 13 helmikuuta 2020
OKM-julkaisutyyppiA4 Artikkeli konferenssijulkaisuussa
Tapahtuma31st International Conference on Tools with Artificial Intelligence (ICTAI 2019) - Portland, OR, Yhdysvallat (USA)
Kesto: 4 marraskuuta 20196 marraskuuta 2019
https://ictai2019.org

Julkaisusarja

NimiProceedings-International Conference on Tools With Artificial Intelligence
KustantajaIEEE COMPUTER SOC
ISSN (painettu)1082-3409

Tieteenalat

  • 113 Tietojenkäsittely- ja informaatiotieteet

Siteeraa tätä