WASP: A Native ASP Solver Based on Constraint Learning
WASP: A Native ASP Solver Based on Constraint Learning
复制标题
WASP：基于约束学习的原生 ASP 求解器
DOI：
--
复制
发表时间：
2013
期刊：
影响因子：
--
通讯作者：
F. Ricca
中科院分区：
文献类型：
--
作者：
Mario Alviano;Carmine Dodaro;Wolfgang Faber;N. Leone;F. Ricca
本文介绍了WASP，一个ASP求解器处理析取逻辑程序下的稳定模型语义。WASP实现了最初用于SAT求解的技术，这些技术已经扩展到科普程序。其中包括重新启动，冲突驱动的约束学习和backjumping。此外，WASP将这些基于SAT的技术与专门为ASP计算设计的优化方法相结合，例如源指针增强无基集计算，基于原子支持的向前和向后推理运算符以及稳定模型检查技术。在分支算法方面，WASP采用BerkMin准则与前瞻技术相结合的方法。本文还报道了WASP在第三届ASP竞赛系统轨道上运行的实验结果。
This paper introduces WASP, an ASP solver handling disjunctive logic programs under the stable model semantics. WASP implements techniques originally introduced for SAT solving that have been extended to cope with ASP programs. Among them are restarts, conflict-driven constraint learning and backjumping. Moreover, WASP combines these SAT-based techniques with optimization methods that have been specifically designed for ASP computation, such as source pointers enhancing unfounded-sets computation, forward and backward inference operators based on atom support, and techniques for stable model checking. Concerning the branching heuristics, WASP adopts the BerkMin criterion hybridized with look-ahead techniques. The paper also reports on the results of experiments, in which WASP has been run on the system track of the third ASP Competition.