Breaking Weighted Model Counting Solvers Using EXTREMEgen

Generating WMC instances for fuzzing

Bachelor thesis (2025)

Authors

B.P. Snelten Electrical Engineering, Mathematics and Computer Science

Contributors

A.L.D. Latour Algorithmics (mentor)
M. Skrodzki Computer Graphics and Visualisation (graduation committee member)
Faculty
Electrical Engineering, Mathematics and Computer Science
More Info
expand_more

Published Date

31-01-2025

Language

English

Reuse Rights

Other than for strictly personal use, it is not permitted to download, forward or distribute the text or part of it, without the consent of the author(s) and/or copyright holder(s), unless the work is under an open content license such as Creative Commons.

Faculty

Electrical Engineering, Mathematics and Computer Science

Abstract

Weighted model counting (WMC) solvers play a key role in Bayesian inference applications, used for medical diagnosis [17] [16] and risk assessment [14]. Ongoing efforts to improve WMC solver developers aim to develop a fuzzer to identify bugs. This research is aimed at enhancing the quality of this fuzzer by developing an additional method to generate WMC instances, EXTREMEgen [21]. The functionality of this new approach relies on generating practical instances from Bayesian networks and breaking the solvers using extreme weights. Our empirical experiments show that EXTREMEgen exposes bugs in state-ofthe-art WMC solvers. The generated instances are solved fast enough to be usable in fuzzing. However, generation speed needs to be optimized to become practical for fuzzing. When optimized, EXTREMEgen could become the first generator of WMC instances specifically designed for fuzzing.

Files

Research_paper_breaking_a_solv... (pdf)
(pdf | 0.246 Mb)
Unknown license