AutoTW-ASP: Automatic Low-Treewidth Rewrite Synthesis and Uncertainty-Aware Backend Routing for Exact Neurosymbolic ASP Training

Recent neurosymbolic Answer Set Programming (ASP) pipelines frequently rely on manual encoding redesign to exploit treewidth-sensitive exact inference backends, creating a reproducibility and scalability bottleneck. We study an integrated system, AutoTW-ASP, that jointly performs semantics-preserving rewrite selection and uncertainty-aware backend routing between exact enumeration and compilation-based inference. The method combines motif-level rewrite guards, crossover-margin prediction, and abstention-to-enumeration under uncertainty. We formalize rewrite acceptance, routing regret, and constrained end-to-end optimization, and we connect these formal components to an empirical protocol spanning symbolic and hybrid benchmark families. Experiments show that rewrite mismatch rates remain below a predefined projection criterion (maximum observed mismatch rate 0.00375), while non-zero exactness violations remain in accepted-rewrite audits. Routing maintains strong severe-shift coverage (0.9346) and low mean regret in mild/moderate regimes, but severe-shift exactness violations and elevated calibration error persist. Integrated training achieves median 1.140\(\times\) speedup, which is below a 1.20\(\times\) acceptance target, and therefore does not fully support the strongest end-to-end claim under strict exactness constraints. These outcomes establish a bounded positive result: automated rewrite-plus-routing can deliver measurable efficiency gains and informative uncertainty structure, but claim-level guarantees remain conditional on tighter guard policies and calibration in hard-shift regimes.