Propositional model counting (#SAT) is the counting variant of the Boolean Satisfiability (SAT) problem. Development of #SAT solvers has seen a boom in recent years. These tools are complex and hard to debug. To address this, we propose a delta debugger that reduces fault-triggering unweighted model counting instances. Our delta debugger shows an improvement compared to state of the art in the related field of SAT solvers.

Model counting (#SAT) is a fundamental problem in theoretical computer science with applications in probabilistic reasoning, reliability analysis, and verification tasks. Despite advancements in solvers and #SAT instance generation, existing benchmarks fail to fully capture the diversity of structural features that influence solver performance. This paper introduces a feature-driven #SAT instance generator that systematically varies the fraction of Horn clauses across the full range (0% to 100%), enabling a rigorous evaluation of solver performance. Results reveal a “U-shaped” correlation between solve times and Horn-clause fractions and a strong relationship with model counts, exposing computational bottlenecks. Our contributions include the generator design, experimental validation across multiple solvers, and insights into improving solvers for challenging structural configurations, advancing #SAT research.

Model Counting solvers are critical in many domains. One way of validating them is through fuzzing. However, current fuzzing approaches lack systematic methods to evaluate how different test generators compare in bug-triggering behavior. This paper proposes three methods for evaluating fuzzer similarity: black-box analysis, differential testing, and white-box analysis.

A similarity metric was defined using differential testing, incorporating solver behavior, solve time, and count differences. A case study was conducted on three fuzzers across numerous configurations and four SOTA model counters, followed by an analysis of correlations between CNF feature distribution similarities and fuzzer behavioral similarities.

The results show moderate correlations between graph structure features (minimum variable node degrees) and fuzzer similarity, while clause balance features show negative correlations. However, the method proves inconclusive for selecting dissimilar fuzzers due to limited incorrect counts in our dataset, uncertainty about crash causes, and the similarity metric's inherent subjectivity. Further research is needed, either by expanding the scope of the experiment with more diverse fuzzers, CNF features, and counters, or by pursuing another method recommended by this study.

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.