Abstract Solvers for Computing Cautious Consequences of ASP programs
University of Calabria(卡拉布里亚大学);University of Genoa(热那亚大学);dibris.unige.it(dibris.unige.it(此处为邮箱域名,非机构名,按要求不应提取,实际应为前两个大学))
抽象求解器是一种形式化分析算法的方法,这些算法已被有效地用于描述、比较和组合各种领域的求解技术,例如命题可满足性(SAT)、量化SAT、可满足性模理论、答案集编程(ASP)和约束ASP。在本文中,我们设计,实现和测试新的谨慎推理任务的抽象解决方案,在ASP。我们展示了如何改进目前的抽象求解器谨慎推理ASP借用新技术在SAT骨干计算,以设计新的求解算法。通过这样做,我们也正式表明,在ASP中解决谨慎推理任务的算法是密切相关的计算布尔公式的骨干。我们实现了一些新的解决方案,在ASP求解器WASP,并表明他们的性能是比较先进的解决方案的基准问题,从过去的ASP比赛。正在考虑接受TPLP。
2019-07-22 cs.AI cs.LO
Improving DPLL Solver Performance with Domain-Specific Heuristics: the ASP Case
Eastman Kodak Company(伊士曼柯达公司)
尽管基于DPLL过程的求解器的性能最近有所改进,但搜索算法仍然可能集中在搜索空间的错误区域上,从而阻止求解器在可接受的时间量内返回解。这种前景是一个真正的问题,例如在工业环境中,用户通常期望一致的性能。为了克服这个问题,我们提出了一个框架,允许学习和使用特定领域的算法在求解器的基础上的DPLL程序。学习是离线完成的,在目标域的代表性实例上,然后将学习到的算法用于选择点选择。在本文中,我们专注于答案集编程(ASP)求解器。在我们的实验中,引入特定于域的算法将硬实例的性能提高了3个数量级(平均2个数量级),几乎完全消除了由于等待答案变得不可接受而必须终止求解器的情况。
2011-02-10 cs.AI cs.LO
ASP: Learn a Universal Neural Solver!
the Chinese University of Hongkong, Shenzhen(香港中文大学(深圳));Carnegie Mellon University(卡内基梅隆大学);Peking University(北京大学)
将机器学习应用于组合优化问题具有提高效率和准确性的潜力。然而,现有的基于学习的求解器在面对问题分布和规模的变化时,往往难以泛化。在本文中,我们提出了一种名为ASP:Adaptive Staircase Policy Space Response Oracle的新方法来解决这些泛化问题并学习通用神经求解器。ASP由两个组件组成:分布式探索,它增强了求解器使用策略空间响应Oracle处理未知分布的能力,以及持久规模适应,它通过课程学习提高了可伸缩性。我们已经在几个具有挑战性的COP上测试了ASP,包括旅行推销员问题,车辆路径问题和奖品收集TSP,以及来自TSPLib和CVRPLib的真实实例。我们的研究结果表明,即使模型大小相同,训练信号较弱,ASP也可以帮助神经求解器探索和适应未知的分布和不同的尺度,从而实现卓越的性能。特别是,与标准训练管道下的相同神经求解器相比,ASP在TSP的生成实例和真实实例上的最优性差距显著降低,分别为90.9%和47.43%,CVRP降低了19%和45.57%。
2023-03-01 cs.AI cs.LG math.OC
Bound Founded Answer Set Programming
National ICT Australia(澳大利亚国家信息与通信技术公司);The University of Melbourne(墨尔本大学)
答案集编程(ASP)是一个强大的建模形式主义,是非常有效的解决组合问题。ASP求解器实现了稳定的模型语义,消除了逻辑程序的解决方案中布尔变量之间的循环推导。由于这一点,ASP求解器比命题可满足性(SAT)和约束编程(CP)求解器更适合解决一类特定的问题,其规范包括归纳定义,如图中的可达性。另一方面,ASP求解器由于无法对有限域变量进行建模而受到基础瓶颈的影响。此外,现有的稳定模型语义不足以禁止循环推理的数值变量的界限。需要这样做的一个例子是对图中节点之间的最短路径进行建模。正如可达性可以被编码为具有一个或多个基本情况和递归规则的归纳定义一样,节点之间的最短路径也可以用类似的基本情况和递归规则来建模。这种稳定模型语义的缺陷在ASP系统中引入了另一种类型的基础瓶颈,这种瓶颈不能通过简单地将ASP与CP求解器合并来消除,而是需要将语义从布尔和正常规则扩展到数值变量和更一般的规则。在这项工作中,我们提出了边界建立的答案集编程(BFASP),解决了这个问题,从而消除了ASP系统中固有的所有类型的接地瓶颈。
2014-05-14 cs.AI
claspfolio 2: Advances in Algorithm Selection for Answer Set Programming
University of British Columbia(不列颠哥伦比亚大学);University of Freiburg(弗莱堡大学);University of Potsdam(波茨坦大学)
出现在逻辑编程理论与实践(TPLP)中。在屡获殊荣的,基于投资组合的ASP求解器clasplem的基础上,我们提出了clasplem 2,一个模块化和开放的求解器架构,集成了几种不同的基于投资组合的算法选择方法和技术。clasple2求解器框架支持各种特征生成器、求解器选择方法、求解器组合以及基于求解器调度的预求解技术。clasp 2的默认配置依赖于ASP求解器clasp的轻量级版本来生成静态和动态实例特性。clasp 2灵活的开放式设计是一个区别于ASP的因素。因此,它提供了一个独特的框架,用于比较和组合现有的基于组合的算法选择方法和技术在一个单一的,统一的框架。利用这一点,我们进行了广泛的实验研究,以评估不同的功能集,选择方法和基本求解器组合的影响。除了获得对各种方法和技术的实用性的实质性见解之外,我们还确定了clasple2的默认配置,该配置不仅在clasp的默认配置和clasple2的早期版本上实现了实质性的性能增益,而且还超过了clasp的手动调整配置。
2014-05-07 cs.AI
selp: A Single-Shot Epistemic Logic Program Solver
TU Wien(维也纳工业大学)
认知逻辑程序(英语:Epistemic Logic Programs,ELP)是答案集编程(英语:Answer Set Programming,ASP)的一个扩展,它具有认知算子,允许一种形式的元推理,即在多个可能世界上进行推理。现有的ELP求解方法通常依赖于对ASP求解器进行多次调用以评估ELP。然而,在本文中,我们表明,也存在一个直接的翻译从ELP到非地面ASP有界arity。由此产生的ASP程序可以在Single Shot中求解。然后,我们实现这种编码方法,使用最近提出的技术来处理大型,非地面ASP规则,到原型ELP解决系统“selp”,我们在本文中提出。该求解器在一组ELP基准实例上表现出具有竞争力的性能。逻辑程序设计理论与实践(TPLP)
2020-01-04 cs.AI cs.LO
A Multi-Engine Approach to Answer Set Programming
Università degli Studi di Genova(热那亚大学);Università degli Studi di Sassari(萨萨里大学);Università della Calabria(卡拉布里亚大学)
答案集编程(ASP)是一种真正的声明式编程范式,在非单调推理和逻辑编程领域提出,最近已在许多应用中使用。因此,开发高效的ASP系统至关重要。考虑到改进ASP的求解方法的任务,有两种常用的方法来实现这一目标:$(i)$扩展最先进的技术和ASP求解器,或$(ii)$从头开始设计一个新的ASP求解器。这些趋势的替代方案是建立在最先进的求解器之上,并应用机器学习技术来自动选择“最好的”可用求解器。在本文中,我们追求这后一个方向。我们首先定义了一组便宜的计算句法功能,表征ASP程序的几个方面。然后,我们应用分类方法,给定{ \sl training}集中的实例的特征和求解器在这些实例上的性能,归纳学习算法选择策略以应用于{ \sl test}集。我们报告了一些实验的结果,考虑到求解器和不同的训练和测试集的情况下,从提交给“系统跟踪”的第三届ASP竞赛。我们的分析表明,通过将机器学习技术应用于ASP求解,可以获得非常稳健的性能:与第三届ASP竞赛的任何求解器相比,我们的方法可以解决更多的实例。(To逻辑程序设计理论与实践(Theory and Practice of Logic Programming,TPLP)
2013-06-20 cs.AI cs.LO
LP2PB: Translating Answer Set Programs into Pseudo-Boolean Theories
Vrije Universiteit Brussel(布鲁塞尔自由大学)
回答集编程(ASP)是一种成熟的知识表示形式。大多数ASP求解器都是基于布尔可满足性求解技术的(扩展)。虽然这些求解器在许多实际应用中非常成功,但它们的强度受到其底层证明系统分辨率的限制。在本文中,我们提出了一个新的工具LP2PB,ASP程序转换为伪布尔理论,求解器的基础上(更强)切割平面证明系统存在。我们评估我们的工具,和潜在的切割平面为基础的解决ASP对传统的ASP基准以及基准从伪布尔求解。我们的结果好坏参半:总的来说,传统的ASP求解器仍然优于我们的翻译方法,但几个基准家庭被确定的平衡转移的其他方式,从而表明,进一步调查到一个更强大的证明系统的ASP是有价值的。
2020-09-22 cs.AI cs.LO
Unfounded Sets for Disjunctive Hybrid MKNF Knowledge Bases
University of Alberta(阿尔伯塔大学)
将回答集编程(ASP)的封闭世界推理与本体论的开放世界推理相结合,拓宽了推理机的应用空间。析取混合MKNF知识库简洁地扩展了ASP,并且在某些情况下不会增加推理任务的复杂性。然而,在许多情况下,求解器的开发是滞后的。因此,解决析取混合MKNF知识库的唯一已知方法是基于猜测和验证,如Motik和Rosati在其原始工作中所制定的。一个主要的障碍是理解如何约束传播可以由求解器执行,其中,在ASP的上下文中,围绕着\textit{unfounded atoms}的计算,原子是假的部分解释。在这项工作中,我们建立了改进求解器的混合MKNF知识库与析取规则:我们正式的概念,这些知识库的无根据集,确定较低的复杂性界限,并演示了我们如何将这些发展集成到一个求解器。我们讨论了本体论所带来的挑战,这些挑战不存在于析取逻辑程序的求解器的开发中,这保证了与传统的无根据集定义的一些偏差。我们比较我们的工作与事先定义的无根据集。
2021-02-25 cs.AI
A Solver-in-the-Loop Framework for Improving LLMs on Answer Set Programming for Logic Puzzle Solving
本文提出了一种求解器循环框架,通过引导求解器进行指令微调,提升LLM在Answer Set Programming中生成逻辑谜题解答的性能。
2025-12-18 cs.AI cs.CL
On the generalization of learned constraints for ASP solving in temporal domains
University of Potsdam(波茨坦大学)
本文研究 ASP 求解时序问题时学习约束跨时间步复用的条件,提出逻辑程序转换及可泛化全部约束的时序性质,并通过实验验证其对求解性能的影响。
2024-10-15 cs.AI
Conflict-driven ASP Solving with External Sources
Institut für Informationssysteme(信息系统研究所);Technische Universität Wien(维也纳技术大学)
答案集编程(ASP)是一种基于非单调逻辑程序和高效求解器的著名问题求解方法。为了能够访问外部信息,HEX程序扩展具有外部原子的程序,其允许逻辑程序和外部计算源(例如,描述逻辑推理机和Web资源)。目前的求解器评估HEX程序的翻译ASP本身,其中外部原子的值猜测和验证后,普通的答案集计算。这种优雅的方法一般不会随着外部访问的数量而扩展,特别是在存在非确定性的情况下(这对ASP很有用)。在本文中,我们提出了一种新的,本地的算法评估HEX程序,使用学习技术。特别是,我们扩展了冲突驱动的ASP解决技术,它可以防止求解器再次遇到相同的冲突,从普通的十六进制程序。我们展示了如何从外部源评估中获得额外的知识,以及如何在冲突驱动的算法中使用它。我们首先针对不知情的情况,即,当我们没有额外的信息外部来源,然后扩展我们的方法的情况下,额外的元信息是可用的。实验表明,从外部源学习可以显着减少运行时间和考虑候选兼容集的数量。
2012-10-05 cs.AI
Multi-shot ASP solving with clingo
University of Potsdam(波茨坦大学);INRIA Rennes(雷恩国家信息与自动化研究所);School of Computing Science at Simon Fraser University(西蒙弗雷泽大学计算科学学院);Institute for Integrated and Intelligent Systems at Griffith University(格里菲斯大学集成与智能系统研究所)
我们介绍了一种新的灵活的范式的基础和解决的答案集编程(ASP),我们称之为多拍ASP解决,并提出其实现的ASP系统clingo。多镜头ASP解决功能接地和解决过程中,处理不断变化的逻辑程序。在这样做的过程中,它们仍然有效,并以无缝的方式适应变化。例如,这样的过程允许高级形式的搜索,如优化或理论求解,或与环境的交互,如机器人或问答。它们的共同之处在于,问题规范在推理过程中不断演变,这可能是因为数据或约束被添加、删除或替换。这个进化的方面为ASP增加了另一个维度,因为它带来了状态改变操作。我们解决这个问题,提供了一个操作语义,特点接地和解决过程中的多拍ASP解决。此特征化提供了接地和求解器状态以及操纵它们的操作的语义说明。多杆求解的操作性质避免了重新启动地滚球和求解程序的冗余,并受益于求解器的学习能力。clingo通过用控制能力补充ASP的声明性输入语言来实现这一点。在声明方面,一个新的指令允许将逻辑程序结构化为命名的和可参数化的子程序。将这些子程序接地并集成到求解过程中是完全模块化的,并且从程序方面完全可控。为此,clingo提供了一个新的应用程序编程接口,可以方便地通过脚本语言访问。
2018-03-20 cs.AI
Computing LPMLN Using ASP and MLN Solvers
Arizona State University(亚利桑那州立大学)
LPMLN是概率逻辑程序设计语言的新成员。它的主要思想是通过以类似于马尔可夫逻辑定义的方式为每个规则分配权重来克服稳定模型语义的刚性。我们提出了两个实现的LPMLN,$\text{LPMLN2ASP}$和$\text{LPMLN2MLN}$。系统$\text{LPMLN2ASP}$将LPMLN程序转换为答案集求解器$\text{CLINGO}$的输入语言,并利用弱约束和稳定模型枚举,计算最可能的稳定模型以及精确的条件概率和边际概率。系统$\text{LPMLN2MLN}$将LPMLN程序翻译成马尔可夫逻辑解算器的输入语言,诸如$\text{ALCHEMY}$、$\text{TUFFY}$和$\text{ROCKIT}$,并且允许对LPMLN程序执行近似概率推断。我们还证明了有用的LPMLN系统计算其他语言,如ProbLog和珍珠的因果模型,被证明是可翻译成LPMLN。(正在考虑接受TPLP)
2017-11-30 cs.AI cs.LO
Query Answering in Object Oriented Knowledge Bases in Logic Programming: Description and Challenge for ASP
SRI International(斯坦福国际研究院);New Mexico State University(新墨西哥州立大学)
本文介绍ASP中大规模知识库KB_Bio_101及其查询程序,并解释这些查询对当前ASP求解器构成重大实际挑战的原因。
2013-12-20 cs.AI
An efficient solver for ASP(Q)
Alpen-Adria Universität Klagenfurt(克拉根福阿尔卑斯-亚德里亚大学);University of Calabria(卡拉布里亚大学)
本文提出了一种针对带量词的回答集编程 ASP(Q) 的高效求解器,通过优化 QBF 编码过程和采用算法选择策略结合多个求解后端,生成更小公式并显著提升了评估性能,实验证明其优于现有 qasp 系统。
2023-05-17 cs.AI cs.LO
Inconsistency Proofs for ASP: The ASP-DRUPE Format
University of Calabria(卡拉布里亚大学);TU Dresden(德累斯顿工业大学);TU Wien(维也纳工业大学);secunet Security Networks AG(secunet安全网络股份公司)
答案集编程(ASP)求解器是高度调优的复杂过程,其隐式地解决一致性问题,即,决定逻辑程序是否允许答案集。对于(正常的)程序,可以在多项式时间内判定一个要求的答案集在形式上是否是程序的正确答案集.然而,要验证一个声称不一致的程序是否确实不承认任何答案集,还远没有那么快。在本文中,我们解决了这个问题,并开发了新的证明格式ASP-德鲁普命题,析取逻辑程序,包括重量和选择规则。ASP-DRUPE基于反向单元传播(RUP)格式,旨在实现布尔可满足性。我们建立了ASP-DRUPE的正确性,并讨论了如何将其集成到现代ASP解决方案。随后,我们提供了一个实现的ASP-德鲁巴到黄蜂求解器正常逻辑程序。这项工作正在考虑接受在TPLP。
2019-07-24 cs.AI cs.LO
Combining Answer Set Programming and Domain Heuristics for Solving Hard Industrial Problems (Application Paper)
University of Calabria(卡拉布里亚大学);Alpen-Adria-Universität Klagenfurt(阿尔卑斯-亚德里亚大学克拉根福分校)
答案集编程(ASP)是一种流行的逻辑编程范式,已被应用于解决各种复杂的问题。在ASP最具挑战性的实际应用中,有两个由西门子定义的工业问题:伙伴单元问题(PUP)和组合配置问题(CCP)。PUP和CCP的最困难的实例是最先进的ASP求解器无法达到的。实验表明,ASP求解器的性能可以显着提高嵌入特定领域的算法,但在现成的ASP实现这样的标准是不明显的一个适当的有效集成。本文研究了ASP与特定领域启发式算法的结合,目标是有效地解决PUP和CCP的现实问题实例。作为此活动的副产品,ASP求解器WASP扩展了一个接口,该接口可以轻松地在求解器中嵌入新的外部算法。评估结果表明,我们的领域启发式驱动的ASP求解器发现解决方案的所有现实世界的实例PUP和CCP曾经提供的西门子。本文件正在考虑被TPLP接受。
2016-08-02 cs.AI cs.LO cs.PL
DynASP2.5: Dynamic Programming on Tree Decompositions in Action
TU Wien(维也纳工业大学)
一个活跃的理论研究领域是有效的精确参数化算法。最近的求解竞赛,如PACE挑战赛表明,参数化算法社区的实际兴趣也越来越大。一个重要的研究问题是,专用的参数化精确算法是否具有一定的实际意义,甚至可以击败成熟的问题解决者。我们认为基于逻辑的声明式建模语言和问题解决框架答案集编程(ASP)。最先进的ASP求解器在很大程度上依赖于基于SAT的算法。ASP求解器(DynASP 2),这是基于一个经典的动态规划的树分解,最近已经出版。不幸的是,DynASP 2可以优于现代ASP解决方案的程序,小的树宽度,只有当感兴趣的问题是计数的解决方案的数量。在本文中,我们描述了我们的新的实现(DynASP 2.5),显示竞争行为,以国家的最先进的ASP求解器,即使只找到一个解决方案时,解决问题的斯坦纳树的问题,已建模在ASP的低树宽的图。我们的实现是基于一种新的方法,我们称之为多通动态规划(M-DPSINC)。
2017-06-28 cs.AI cs.CC cs.LO
Driving CDCL Search
Università della Calabria(卡拉布里亚大学);Alpen-Adria-Universität Klagenfurt(克拉根福阿尔卑斯-亚得里亚大学)
CDCL算法是最先进的SAT、SMT、ASP等求解器采用的领先解决方案。实验表明,嵌入特定领域的算法可以显着提高CDCL求解器的性能,特别是在大型现实世界的问题。然而,在现成的CDCL实现中适当地集成这样的标准并不明显。在本文中,我们提取的关键成分,驱动搜索的CDCL求解器,并提出了一个通用的框架,设计和实施新的算法。我们在ASP求解器中实现了我们的策略,并在两个工业领域进行了实验。在困难的问题实例中,最先进的实现无法在可接受的时间内找到任何解决方案,而我们的实现非常成功,可以找到所有解决方案。
2016-11-16 cs.AI
Aspartix-V21
TU Wien(维也纳工业大学);Graz University of Technology(格拉茨工业大学)
在此求解器描述中,我们介绍了2021年版的ASPARTIX-V,该版本参加了2021年国际辩论计算模型竞赛(ICCMA)。ASPARTIX-V能够解决ICCMA'21中所有经典(静态)推理任务的一部分,并通过将最新的ASP语言结构(例如条件文字),ASP中的域解析和多镜头方法合并来扩展ASPARTIX系统套件。在这种情况下,ASPARTIX-V偏离了ASPARTIX对单片方法的传统关注(即,通过单个ASP编码的单次求解)以进一步增强性能。
2021-09-07 cs.AI
GPU-based parallelism for ASP-solving
Università di Udine(乌迪内大学);Università di Perugia(佩鲁贾大学);Libera Università di Bolzano(波尔扎诺自由大学)
答案集编程(ASP)已成为逻辑编程和非单调推理领域的首选范式。由于有效的求解器的可用性,ASP已成功地应用于大量的应用领域。术语GPU计算表示旨在使现代并行图形处理单元(GPU)用于通用计算的最近编程范例。在本文中,我们描述了一种利用GPU并行性解决ASP问题的方法。基于GPU的求解器的设计提出了各种挑战,由于GPU的软件和硬件架构的特殊性和可满足性问题的内在性质。
2019-09-04 cs.AI cs.DC
Clingcon: The Next Generation
Kobe University(神户大学);University of Potsdam(波茨坦大学);Simon Fraser University(西蒙弗雷泽大学);Griffith University(格里菲斯大学);INRIA Rennes(法国国家信息与自动化研究所雷恩分部)
我们提出了第三代的约束答案集系统clingcon,结合答案集编程(ASP)和有限域约束处理(CP)。虽然它的前辈依靠黑盒方法通过集成CP求解器gecode来混合求解,但新的clingcon系统采用了一种懒惰的方法,使用专用的约束传播器来扩展底层ASP求解器clasp中的传播。不需要对clingcon的混合建模语言进行解析和基础扩展,因为ASP grounder gringo的新通用理论处理能力可以容纳这两种语言。作为一个整体,clingcon 3是ASP系统clingo 5的扩展,clingo 5本身依赖于grounder gringo和solver clasp。clingcon的新方法提供了CP传播到ASP求解的无缝集成,这得益于卡环推理模式的整个频谱,包括例如多镜头求解和高级优化技术。这是通过一种惰性方法来实现的,该方法展开约束的表示,并仅在需要时将其添加到逻辑程序的表示中。虽然展开通常由求解过程中的约束传播器决定,但它可以在预处理过程中部分(甚至全部)完成。此外,clingcon的约束预处理和传播结合了几种成熟的CP技术,大大提高了其性能。我们证明了这一点,通过一个广泛的实证评估对比,第一,CSP解决方案的背景下,第二,新的clingcon系统与其他混合ASP系统的各种技术。逻辑程序设计理论与实践(Theory and Practice of Logic Programmin…
2017-05-12 cs.AI
Hybrid Answer Set Programming: Foundations and Applications
University of Potsdam(波茨坦大学)
针对标准回答集编程(ASP)求解器无法处理数值及复杂约束的问题,提出带约束的此处与彼处逻辑(HT_c)作为理论基础,为混合ASP提供支持,同时探讨其理论特征与应用价值。
2025-02-13 cs.AI cs.LO
Bounded Combinatorial Reconfiguration with Answer Set Programming
Nagoya University(名古屋大学);National Institute of Informatics(国立信息学研究所);Universität Potsdam(波茨坦大学)
本文提出基于回答集编程的有界组合重构方法,开发的recongo求解器在CoRe Challenge 2022单引擎赛道最短路径项夺冠,还给出了独立集重构问题的ASP编码及全算例实证分析。
2023-07-20 cs.AI
Solver Scheduling via Answer Set Programming
University of British Columbia(不列颠哥伦比亚大学);University of Potsdam(波茨坦大学)
虽然布尔约束技术在过去十年中取得了巨大的进步,但已知最先进的求解器的功效在不同类型的问题实例中变化很大,并且强烈依赖于算法参数。这个问题是通过一个简单而有效的方法来解决的,该方法使用手工制作的,统一的和无序的多个求解器的时间表,在2011年SAT比赛中表现出非常令人印象深刻的表现。受此启发,我们利用的建模和求解能力的答案集编程(ASP),自动确定更完善的,也就是说,非均匀和有序的求解器的时间表,从现有的基准测试数据。我们首先制定多标准优化问题,并提供相应的ASP编码等时间表的确定。由此产生的编码可以很容易地针对不同的设置进行自定义,并且最佳时间表的计算大多可以在眨眼之间完成,即使在处理来自数百到数千个实例的许多求解器的大型运行时数据集时也是如此。此外,我们的方法可以很容易地定制,这使我们能够迅速调整它,为多处理器机器生成并行调度。
2014-01-06 cs.AI cs.LO
Counting Answer Sets via Dynamic Programming
TU Wien(维也纳工业大学)
虽然近年来命题可满足性(#SAT)的解决方案计数问题重新受到关注,但这一研究趋势并没有影响其他AI解决范式,如答案集编程(ASP)。虽然ASP求解器被设计为枚举所有解决方案,因此计数可以很容易地完成,但所有解决方案的具体化是ASP(#ASP)计数问题的明显瓶颈。在本文中,我们提出了基于动态规划的#ASP算法,利用底层(地面)ASP程序的结构。一个原型实现的实验结果表明,与现有的求解器相比,承诺。
2016-12-22 cs.AI cs.CC cs.LO
Modelling Multi-Agent Epistemic Planning in ASP
University of Udine(乌迪内大学);New Mexico State University(新墨西哥州立大学)
设计能够对世界进行推理和行动的智能体一直是人工智能社区的主要目标之一。虽然对于在“简单”域中的规划,智能体可以仅依赖于关于世界的事实,但在几个上下文中,例如,在经济、安全、司法和政治方面,仅仅对世界的了解可能不足以实现预期目标。在这些情况下,认知推理,即,推理代理人对自己的信念和其他代理人的信念,是设计获胜策略的关键。本文利用声明性编程技术解决了多智能体认知环境中的推理问题。特别是,本文提出了一个实际的实现多杆答案集编程为基础的规划,可以在多智能体认知设置,称为PLATO(ePistemic多智能体答案集编程sOlver)的原因。ASP范例使规划器的设计简洁而优雅,w.r.t.其他必要的实现,促进正确性的形式化验证的开发。本文展示了如何规划者,利用一个特设的认知状态表示和效率的ASP求解器,有竞争力的性能结果从文献中收集的基准。目前正在考虑让TPLP接受。
2020-08-07 cs.AI
Finding Similar/Diverse Solutions in Answer Set Programming
Vienna University of Technology(维也纳工业大学);Sabanci University(萨班哲大学)
对于某些计算问题(例如,产品配置、规划、诊断、查询应答、遗传学重构)计算一组相似/不同的解决方案对于更好的决策可能是期望的。基于这一动机,我们在答案集编程(ASP)的背景下研究了该问题的几个决策/优化版本,分析了它们的计算复杂性,并引入了离线/在线方法来计算给定距离函数下此类计算问题的相似/不同解.所有这些方法都依赖于通过为描述问题的ASP程序找到答案集来计算问题的解决方案的想法。离线方法使用ASP求解器(如Clasp)使用问题的ASP公式提前计算所有解决方案,然后使用聚类方法识别相似/不同的解决方案。在线方法计算类似/不同的解决方案以下三种方法之一:通过重新制定的ASP表示的问题,以计算类似/不同的解决方案一次使用ASP求解器;通过计算类似/不同的解决方案迭代(一个接一个)使用ASP求解器;通过修改搜索算法的ASP求解器计算类似/不同的解决方案增量。我们修改了Clasp来实现最后一个在线方法,并将其称为Clasp-NK。在前两种在线方法中,给定的距离函数用ASP表示;在最后一种方法中,它是用C++实现的。我们展示了这些方法在印欧语言相似/不同的同源性重建上的适用性和有效性,以及在Blocks World中的几个规划问题上的适用性和有效性。我们观察到,在计算效率方面,最后一个在线方法优于其他方法;当距离函数不能在ASP中表示时,它还允许我们计算类似/不同的解决方案。
2011-08-16 cs.AI cs.LO cs.PL
Advancing Lazy-Grounding ASP Solving Techniques -- Restarts, Phase Saving, Heuristics, and More
TU Wien (Vienna University of Technology)(维也纳工业大学);Siemens AG Österreich(奥地利西门子公司)
集合编程(ASP)是一种功能强大、表达能力强的知识表示范式,在基于逻辑的人工智能中有大量的应用。然而,传统的接地和解决方法要求ASP程序预先接地,因此遭受所谓的接地瓶颈(即,ASP程序很容易耗尽所有可用内存,从而变得无法解决)。作为一种补救措施,懒惰接地ASP求解器已经开发出来,但许多国家的最先进的技术接地ASP解决还没有提供给他们。在这项工作中,我们提出,第一次,适应惰性接地设置的许多重要的技术,如重新启动,阶段保存,域独立的算法,和学习子句删除。此外,我们调查他们的影响,并在一般情况下观察到解决能力的大幅度提高,也发现在某些情况下的负面影响,表明需要从其他求解器的组合解决。正在考虑接受TPLP。
2020-08-08 cs.AI cs.LO
Abstract Answer Set Solvers with Learning
University of Texas at Austin(德克萨斯大学奥斯汀分校);Department of Computer Science(计算机科学系)
Nieuwenhuis,Oliveras和Tinelli(2006)展示了如何使用转换系统而不是伪代码来描述Davis-Putnam-Logemann-Loveland算法的增强。我们设计了一个类似的框架,几个算法,生成答案集的逻辑程序:Smodels,Smodels-CC,Asp-Sat与学习(Cmodels),和一个新设计和实现的算法Sup。这种描述答案集求解器的方法使得证明它们的正确性、比较它们以及设计新系统变得更加容易。
2010-01-06 cs.AI cs.LO
A System for Explainable Answer Set Programming
University of Corunna(拉科鲁尼亚大学);University of Potsdam(波茨坦大学)
我们提出xclingo,一个工具,用于生成解释的ASP程序注释的文本和标签。这些注释允许跟踪规则的应用或由它们派生的原子。xclingo的输入是一种以ASP注释行形式编写的置标语言,因此以这种方式注释的程序仍然可以被标准ASP求解器接受。xclingo将注释转换为附加的谓词和规则,并使用ASP solver clingo来获得这些辅助谓词的扩展。这些信息随后用于构建包含文本解释的派生树。该语言允许选择解释哪些原子,并依次选择在这些解释中包含哪些原子或规则。我们通过文献中的一个诊断问题来说明其基本特征。
2020-09-22 cs.AI cs.PL
ASPeRiX, a First Order Forward Chaining Approach for Answer Set Computing
University of Angers(昂热大学)
在人工智能中使用回答集编程(ASP)来表示知识或解决组合问题的自然方式是精心设计具有默认否定的一阶逻辑程序。在第一步中,这个带有变量的程序被第一个工具翻译成一个等价的命题:地球仪。然后,命题程序被交给第二个工具:求解器。最后一个计算(如果存在)程序的一个或多个答案集(稳定模型),每个答案集编码初始问题的一个解。直到今天,几乎所有的ASP系统都采用这两步计算。在这篇文章中,ASPeRiX项目是作为一个一阶前向链接方法的答案集计算。这个项目是第一个引入答案集计算方法的项目之一,该方法通过将其集成到搜索过程中来避免规则实例化的初始阶段。该方法适用于一阶规则的前向链接,这些规则通过先前产生的原子在飞行中接地。该方法的理论基础,ASP求解器ASPeRiX的主要算法进行了详细说明,并提供了一些实验和与现有系统的比较。
2016-11-16 cs.AI cs.LO
Annotating Answer-Set Programs in LANA?
University of Bath(巴斯大学);Sabanci University(萨班哲大学);Technische Universität Wien(维也纳工业大学)
虽然过去的研究在回答集编程(ASP)主要集中在理论,ASP求解器技术,和应用程序,目前的工作本身的背景下,一个相当最近的研究趋势:开发支持ASP。特别是,我们建议增加答案集程序与额外的元信息制定一个专用的注释语言,称为LANA。这种语言允许将规则分组为连贯的块,并指定语言签名、类型、前置和后置条件,以及这些块的单元测试。虽然这些注释对ASP求解器是不可见的,因为它们采取程序注释的形式,但它们可以被工具解释为文档,测试和验证目的,以及通过实现语法检查或代码完成功能来消除常见编程错误的来源。为了证明它的多功能性,我们介绍了两个这样的工具,即(一)ASPDOC,用于生成一个HTML文档的基础上的注释信息的程序,和(二)ASPUNIT,用于运行和监控程序块上的单元测试。在基于Eclipse的ASP集成开发环境SeaLion系统中,也对LANA进行了开发。逻辑程序设计理论与实践Theory and Practice of Logic Programming
2012-10-08 cs.AI cs.SE
ASP-Core-2 Input Language Format
Università della Calabria(卡拉布里亚大学);Alpen-Adria-Universität Klagenfurt(阿尔卑斯-亚德里亚大学克拉根福分校);University of Potsdam(波茨坦大学);XIMES GmbH(XIMES有限责任公司);University of Genova(热那亚大学)
求解器输入语言的标准化已经成为知识表示和推理中几个领域发展的主要驱动力,促进了实际应用中的开发。在本文档中,我们介绍了用于答案集编程的ASP-Core-2标准输入语言,该语言自2013年以来一直被ASP竞赛活动采用。
2019-11-11 cs.AI cs.LO
KAYROS: An Anytime and Exact Open-Source Solver for Duration-Minimization Time-Dependent Vehicle Routing. A Technical Report and a Case Study in Human-AI Engineering
IMT Atlantique(大西洋国立高等矿业电信学院);CNRS(法国国家科学研究中心);INSA Lyon(里昂国立应用科学学院);Inria(法国国家信息与自动化研究所)
研究时长最小化的时间相关车辆路径规划问题,核心方法是基于现有技术扩展开源求解器KAYROS,具有随时、精确等特性,主要贡献是在基准测试集上取得成果并介绍新基准测试集,展示求解器及相关内容,体现人类与人工智能协作。
2026-10-20 cs.AI cs.MS math.OC
User Guided Abductive Proof Generation for Answer Set Programming Queries (Extended Version)
Singapore Management University(新加坡管理大学);University of Toulouse(图卢兹大学)
我们提出了一种方法,用于生成可能的证据的查询相对于一个给定的答案集编程(ASP)规则集使用的溯因过程中的空间的溯因是自动构建的输入规则。给定一组(可能是空的)用户提供的事实,我们的方法推断出任何额外的事实,可能需要的蕴涵的查询,然后输出这些额外的事实,而无需用户明确指定的所有abdibles的空间。我们还提出了一种方法来生成一组有向边对应的理由图的查询。此外,通过不同形式的隐式项替换,我们的方法可以考虑用户提供的事实,并适当修改溯因解。过去关于绑架的工作主要是基于目标导向的方法。然而,这些方法可能导致求解器不是真正声明性的。少得多的工作已经做了实现绑架在一个自自底向上的的求解器,如Clingo ASP求解器。我们描述了新的ASP程序,可以直接在Clingo中运行,产生的溯因解和有向边集,而无需修改底层的求解引擎。
2022-09-16 cs.AI cs.LO
Quantitative Evaluation of Quantum/Classical Neural Network Using a Game Solver Metric
Faculty of Science;Technology, Keio University, Yokohama, Kanagawa 223-8522 Japan;Graduate School of Science;Department of Physics \& Astronomy, University College London, London, WC1E 6BT, United Kingdom
本文提出基于井字棋Elo评分的游戏求解基准,比较经典、量子和混合神经网络,发现混合网络性能接近经典网络,且量子通信开销适度,验证了游戏基准评估量子系统的可行性。
2025-11-10 cs.AI cs.LG quant-ph
Can LLMs Build a MaxSAT Solver from Papers? The CoreForge Experience
Carnegie Mellon University(卡内基梅隆大学)
该研究利用大语言模型从论文构建无权重 MaxSAT 求解器,采用结合论文讨论、代码实现及审核修订的迭代流程,评估特定配置,发现虽未现错误答案,但性能低于手工设计求解器,总结了相关经验教训。
2026-07-17 cs.AI cs.LO
lpopt: A Rule Optimization Tool for Answer Set Programming
TU Wien(维也纳工业大学)
最先进的答案集编程(ASP)求解器依赖于一个名为grounder的程序,将包含变量的非基础程序转换为无变量的命题程序。这种接地的大小很大程度上取决于非接地规则的大小,因此,减少这样的规则的大小是一个有前途的方法来提高求解性能。为此,在本文中,我们宣布lpopt,一个工具,它可以将大型逻辑编程规则分解为更小的规则,更容易处理当前的求解器。该工具是专门为处理ASP语言(ASP-Core)的标准语法而定制的,使用户更容易编写高效和直观的ASP程序,否则通常需要专家ASP工程师进行大量的手工调整。它基于Morak和Woltran(2012)提出的一个想法,我们对其进行了显著扩展,以处理完整的ASP语法,包括聚合,弱约束和算术表达式等复杂结构。我们提出的算法,如何对待这些结构的理论基础,以及实验评估显示我们的方法的可行性。
2016-08-23 cs.AI cs.LO cs.PL
Multi-threaded ASP Solving with clasp
Institut für Informatik(信息学研究所);Universität Potsdam(波茨坦大学);Simon Fraser University(西蒙弗雷泽大学);Griffith University(格里菲斯大学)
我们提出了新的多线程版本的国家的最先进的答案集求解器扣。我们详细介绍了它的组件和通信架构,并说明他们如何支持的主要功能的扣。此外,我们提供了一些见解的数据表示用于不同的约束类型处理的扣。所有这一切都伴随着一个广泛的实验分析的主要特点有关的多线程卡环。
2012-10-11 cs.AI cs.DC cs.LO