We propose an end-to-end approach for Answer Set Programming (ASP) and linear algebraically compute stable models satisfying given constraints. The idea is to implement Lin-Zhao's theorem together with constraints directly in vector spaces as numerical minimization of a cost function constructed from a matricized normal logic program, loop formulas in Lin-Zhao's theorem and constraints, thereby no use of symbolic ASP or SAT solvers involved in our approach. We also propose precomputation that shrinks the program size and heuristics for loop formulas to reduce computational difficulty. We empirically test our approach with programming examples including the 3-coloring and Hamiltonian cycle problems.
翻译:我们提出了一种用于答案集编程(ASP)的端到端方法,通过线性代数计算满足给定约束的稳定模型。该方法的核心思想是将Lin-Zhao定理与约束条件直接在向量空间中实现,通过数值最小化由矩阵化的正规逻辑程序、Lin-Zhao定理中的循环公式以及约束条件构建的成本函数,从而无需在方法中使用符号化的ASP或SAT求解器。我们还提出了缩小程序规模的预计算方法以及用于降低计算难度的循环公式启发式策略。我们通过包括三着色问题和哈密顿回路问题在内的编程实例对方法进行了实证测试。