Feature-Driven SAT Instance Generation
Benchmarking Model Counting Solvers Using Horn-Clause Variations
V. Jurišić (TU Delft - Electrical Engineering, Mathematics and Computer Science)
A.L.D. Latour – Mentor (TU Delft - Algorithmics)
More Info
expand_more
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.
Abstract
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.