AutoTW-ASP: Automatic Low-Treewidth Encoding Synthesis and Backend Routing for Neurosymbolic ASP
Current neurosymbolic ASP pipelines require manual encoding redesign (for example carry-based formulations) to unlock treewidth-aware compilation gains. This project extends the dual-backend framework by automatically rewriting ASP constraints into semantically equivalent, lower-treewidth forms and dynamically routing each training instance to enumeration or compilation. The core idea is to combine static graph analysis of grounded programs with a semantics-preserving rewrite library and a learned crossover predictor based on treewidth, model-count proxies, and circuit reuse ratio. The expected impact is to remove expert-dependent encoding effort, broaden exact inference to more tasks, and improve training efficiency without sacrificing correctness.
2 paper variants
Problem Workspace
Problem Statement
Scope: Build an automated optimization layer on top of a NeurASP-style training loop with two exact backends (stable-model enumeration and d-DNNF compilation). The system will (1) analyze grounded ASP programs and observations, (2) generate candidate rewrites that preserve stable-model semantics, (3) estimate post-rewrite treewidth and reuse potential, and (4) select the backend per observation or program family using a calibrated crossover policy. Constraints: Rewrites must be semantics-preserving under stable-model semantics and must not change task labels or supervision signals. The method must support programs with default negation, integrity constraints, and common arithmetic/relational patterns used in neurosymbolic datasets. Compilation overhead must be controlled through caching and amortization; when reuse is low or structure varies heavily, the system should fall back to enumeration. Success criteria: Compared with a strong manual baseline (naive…Read more
Read less
Execution plan
Metrics: task accuracy (sum accuracy, symbol accuracy, puzzle/constraint satisfaction rate), exactness (agreement with exact reference inference), compile success rate, compilation time per circuit, circuit size, measured treewidth, cache hit rate, and total wall-clock training time. Baselines: (1) enumeration-only NeurASP-style inference, (2) compilation-only without rewriting, (3) manual carry-style encoding with fixed backend, and (4) heuristic backend switch without rewriting. Data/splits: use standard train/test splits for MNIST and HWF; fixed-seed splits for Sudoku/ordering/counting/shortest-path; report multi-seed means and confidence intervals. Acceptance criteria: at least 20% reduction in end-to-end training time versus the best fixed-backend baseline on at least three benchmark families, no statistically significant drop in primary task accuracy, and exact inference agreement >=99.9% with reference computations on held-out checks.