Stable model semantics for founded bounds

作     者：Aziz, Rehan Abdul Chu, Geoffrey Stuckey, Peter J. 

作者机构：Univ Melbourne Dept Comp & Informat Syst Victoria Lab Natl ICT Australia Melbourne Vic 3010 Australia 

出 版 物：《THEORY AND PRACTICE OF LOGIC PROGRAMMING》 (逻辑程序设计理论与实践)

年 卷 期：2013年第13卷第4-5期

页      面：517-532页

核心收录：

学科分类：08[工学] 0835[工学-软件工程] 0701[理学-数学] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

基　　金：Australian Government Australian Research Council through the ICT Centre of Excellence program 

主　　题：answer set programming stable model semantics finite domain solving 

摘      要：Answer Set Programming (ASP) is a powerful form of declarative programming used in areas such as planning or reasoning. ASP solvers enforce stable model semantics, which rule out solutions representing certain kinds of circular reasoning. Unfortunately, current ASP solvers are incapable of solving problems involving cyclic dependencies between multiple integer or continuous quantities effectively. In this paper, we generalize the notion of stable models to bound founded variables with arbitrary domains, where bounds on such variables need to be justified by some rule in the program in order for the model to be stable. We show how to handle significantly more general rule forms where bound founded variables can act as head or body variables, and where head and body variables can be related via complex constraints subject to certain monotonicity requirements. We describe a new unfounded set detection algorithm which allows us to enforce this generalization of the stable model semantics. We also show how these unfounded sets can be explained in order to allow effective conflict-directed clause learning. The new solver merges the best features of CP, SAT and ASP solvers and allows new types of problems to be solved very efficiently.