Feature-Driven SAT Instance Generation

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.