This paper introduces a general framework for generate-and-test-based solvers for epistemic logic programs that can be instantiated with different generator and tester programs, and we prove sufficient conditions on those programs for the correctness of the solvers built using this framework. It also introduces a new generator program that incorporates the propagation of epistemic consequences and shows that this can exponentially reduce the number of candidates that need to be tested while only incurring a linear overhead. We implement a new solver based on these theoretical findings and experimentally show that it outperforms existing solvers by achieving a ~3.3x speed-up and solving 91% more instances on well-known benchmarks.

翻译：本文提出了一种通用的生成-测试求解框架，可用于认知逻辑程序，该框架可通过不同的生成器和测试器程序进行实例化。我们证明了在此框架下构建的求解器正确性的充分条件。同时，本文提出了一种新的生成器程序，该程序融合了认知推理的传播机制，并证明该机制可在仅引入线性开销的情况下，将待测试候选解的数量指数级减少。基于这些理论发现，我们实现了一种新的求解器，并通过实验证明其在经典基准测试中性能优于现有求解器，实现了约3.3倍的加速，并解决了多91%的问题实例。