Research map / Learning theory and algorithms / Combinatorial and search optimization
Solving Epistemic Logic Programs Using Generate-and-Test with Propagation
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.
Introduces a general generate-and-test framework for epistemic logic programs with formal correctness conditions, plus a generator that propagates epistemic consequences, implemented in eclingo, which outperforms existing ELP solvers on Eligibility, Yale and Bomb benchmarks.
Problem
Solving epistemic logic programs (ELPs) efficiently; existing generate-and-test solvers lack a general framework and the tester checks on every candidate stable model are costly.
Approach
A general generator/tester framework with sufficient correctness conditions, and a new generator G1 that propagates epistemic consequences (via fresh atoms and rules) so that many non-worldview candidates are pruned inside the generator, with only linear overhead.
Key results
- The new solver solves 283 of 326 instances versus 148 for eclingo, a 91% increase, with a 3.3x average speed-up over eclingo.
- The propagation-based generator G1 solves 283 instances against 166 for the baseline generator G0 (Table of generator comparison), with average time 139s vs 306s.
- On Bomb, the new solver solves about 7.7x more instances than EP-ASP and is 1.5x faster and solves 50% more instances than EP-ASP-se.
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| add epistemic propagation to the generator (G0 → G1) (ablation) | eclingo generate-and-test solver · All benchmarks | instances solved: 166 -> 283 | Helped |
| add epistemic propagation to the generator (G0 → G1) (ablation) | eclingo generate-and-test solver · All benchmarks | time (s): 306.350 -> 139.328 | Helped |
| add epistemic propagation to the generator (G0 → G1) (ablation) | eclingo generate-and-test solver · Eligibility | instances solved: 145 -> 145 | No clear effect |
| add epistemic propagation to the generator (G0 → G1) (ablation) | eclingo generate-and-test solver · Eligibility | time (s): 18.621 -> 17.982 | Helped |
| add epistemic propagation to the generator (G0 → G1) (ablation) | eclingo generate-and-test solver · Yale | instances solved: 7 -> 7 | No clear effect |
| add epistemic propagation to the generator (G0 → G1) (ablation) | eclingo generate-and-test solver · Yale | time (s): 0.469 -> 0.377 | Helped |
| add epistemic propagation to the generator (G0 → G1) (ablation) | eclingo generate-and-test solver · Bomb | instances solved: 15 -> 131 | Helped |
| add epistemic propagation to the generator (G0 → G1) (ablation) | eclingo generate-and-test solver · Bomb | time (s): 556.396 -> 246.039 | Helped |
| use G1 instead of eclingo | epistemic logic program solver · All benchmarks | instances solved: 148 -> 283 | Helped |
| use G1 instead of eclingo | epistemic logic program solver · All benchmarks | speedup: 3.3x | Helped |
| use G1 instead of EP-ASP | epistemic logic program solver · All benchmarks | speedup: 3.8x | Helped |
| use G1 instead of G0 (ablation) | eclingo generate-and-test solver · easy instances under 0.546 seconds | instances solved: 49 | Mixed |
Surprising findings
- Existing generate-and-test solvers outperform translational solvers on the benchmarks, and the authors' experiments show the same ordering across the evaluated solvers.
- The original paper's theorem statements claim exponential candidate reduction, but on the benchmarks the gain is mainly on Bomb rather than Eligibility, where eclingo and G0 perform similarly.
Limitations
- Tester check is still a Sigma^P_2 oracle call per candidate that is not propagated away.
- Evaluated only on three benchmark families, mostly conformant planning and Eligibility.
- Domain-specific heuristics of EP-ASP-se not integrated; future work needed for heuristics and splitting.
Experimental setup
Datasets: Eligibility benchmark Yale Shooting benchmark Bomb in the Toilet benchmark
Benchmarks: Eligibility Yale Shooting Bomb in the Toilet
Metrics: number of instances solved average solving time speed-up
Baselines: eclingo EP-ASP selp elp2qasp EP-ASP-se
Builds on: eclingo EP-ASP G94 semantics clingo
Closest papers by meaning
- Large Language Models Meet Symbolic Provers for Logical Reasoning Evaluation (ICLR 2025 · similarity 0.84)
- V1: Unifying Generation and Self-Verification for Parallel Reasoners (ICML 2026 · similarity 0.84)
- Can Transformers Reason Logically? A Study in SAT Solving (ICML 2025 · similarity 0.83)
- Are Language Models Efficient Reasoners? A Perspective from Logic Programming (NeurIPS 2025 · similarity 0.83)
- MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data (ICLR 2024 · similarity 0.83)
- Magnushammer: A Transformer-Based Approach to Premise Selection (ICLR 2024 · similarity 0.83)
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.