Research map / Large language models / Agents, code and math
Exact ASP Counting with Compact Encodings
Read the paperCheck your idea against 108,967 papers
AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.
Proposes sharpASP, an exact ASP (normal logic program) answer set counter that lifts component-caching propositional model counting via a copy-variable encoding of loop atoms, avoiding blowup of CNF size, and a hybrid with clingo enumeration.
Problem
Exact answer set counting for normal logic programs is #P-complete and existing counters scale poorly, especially for non-tight programs where translations to CNF blow up due to circular dependencies.
Approach
Define answer sets via Clark's completion plus a copy operation applied only to loop atoms, checked by unit propagation; this lets decomposability and determinism of component-caching model counters be lifted directly to ASP counting without enlarging the formula.
Key results
- sharpASP hybrid (clingo enumeration up to 10^5 answer sets then sharpASP STD) solves 1062 of 1470 benchmarks with PAR2 3082, versus 895 with PAR2 4205 for the best prior hybrid lp2sat+STD.
- Standalone sharpASP(STD) solves 1023 instances (PAR2 3372) vs. 869 for clingo and 840 for aspmc+STD.
- sharpASP strongly reduces BCP time on instances where it wins, since it avoids auxiliary-variable blowup, but struggles on hard-to-decompose instances due to more decisions and cache misses.
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| Use sharpASP(STD) instead of clingo enumeration | ASP exact counting · 1470 graph instances | solved instances: 869 -> 1023 | Helped |
| Use sharpASP(STD) instead of clingo enumeration | ASP exact counting · 1470 graph instances | PAR2: 4285 -> 3372 | Helped |
| Combine clingo enumeration with sharpASP(STD), switching after 10^5 answer sets | Hybrid ASP counter · 1470 graph instances | solved instances: 895 -> 1062 | Helped |
| Combine clingo enumeration with sharpASP(STD), switching after 10^5 answer sets | Hybrid ASP counter · 1470 graph instances | PAR2: 4205 -> 3082 | Helped |
| Use sharpASP(STD) instead of clingo enumeration | ASP exact counting · aspben | solved instances: 321 -> 260 | Hurt |
| Use the compact sharpASP(STD) encoding instead of aspmc+STD or lp2sat+STD (ablation) | ASP counting, Group 1 benchmarks · Group 1 instances | BCP time | Helped |
| Use sharpASP(STD)'s original-variable branching instead of auxiliary-variable branching (ablation) | ASP counting, Group 2 benchmarks · Group 2 instances | number of decisions | Hurt |
| Use sharpASP(STD)'s original-variable branching instead of auxiliary-variable branching (ablation) | ASP counting, Group 2 benchmarks · Group 2 instances | cache performance | Hurt |
Surprising findings
- Clingo enumeration outperforms all non-enumeration counters on aspben instances, and the hybrid of enumeration followed by counting is needed to beat all competitors.
- Standalone sharpASP(D) (1-3 solved counts) is not uniformly better: sharpASP(STD) underperforms lp2sat and aspmc on Group 2 instances because it branches only on original variables.
Limitations
- Performance depends on decomposability of the input and the branching heuristic; hard-to-decompose instances cause many decisions and cache misses.
- Restricted to normal logic programs; disjunctive programs left for future work.
- Hybrid threshold of 10^5 answer sets chosen empirically from clingo runs on the benchmarks.
Experimental setup
Datasets: Hamiltonian cycle benchmarks graph reachability benchmarks aspben benchmark set
Benchmarks: Hamiltonian cycle (405) graph reachability (600) aspben (465)
Metrics: number of solved instances PAR2 score BCP time number of decisions cache hit rate
Baselines: clingo ASProblog DynASP aspmc lp2sat
Builds on: Clark's completion loop formula ASProblog GANAK D4 SharpSAT-TD
Closest papers by meaning
- ApproxASP – a Scalable Approximate Answer Set Counter (AAAI 2022 · similarity 0.93)
- On the Computation of Paracoherent Answer Sets (AAAI 2017 · similarity 0.88)
- Rushing and Strolling among Answer Sets – Navigation Made Easy (AAAI 2022 · similarity 0.87)
- On the Structural Hardness of Answer Set Programming: Can Structure Efficiently Confine the Power of Disjunctions? (AAAI 2024 · similarity 0.87)
- Externally Supported Models for Efficient Computation of Paracoherent Answer Sets (AAAI 2018 · similarity 0.86)
- A Unified View on Forgetting and Strong Equivalence Notions in Answer Set Programming (AAAI 2024 · similarity 0.85)
Writing a paper in this area? scime draft is a free LaTeX editor with AI included, real-time co-authors and a check of your references and venue rules before you submit. It also imports OpenAI Prism projects.