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
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
WSAT(cc) - a fast local-search ASP solver
我们描述WSAT(CC),本地搜索求解器计算模型的理论在语言的命题逻辑扩展的基数原子。WSAT(cc)是PS+逻辑的处理后端,PS+是最近提出的回答集编程的形式主义。
2003-10-31 cs.AI
Transition Systems for Model Generators - A Unifying Approach
University of Kentucky(肯塔基大学)
命题逻辑的一个基本任务是计算命题公式的模型。为此任务开发的程序称为可满足性求解器。我们表明,过渡系统引入Nieuwenhuis,Oliveras和Tinelli模型和分析可满足性求解器可以适应求解器开发的其他两个命题形式主义:逻辑编程下的答案集语义,和逻辑PC(ID)。我们表明,在每种情况下,计算模型的任务可以被看作是“可满足性模答案集编程”,其目标是找到一个模型的理论,也是一个答案集的某个程序。我们开发的统一的角度来看,特别是,求解器CLASP和MINISATID是密切相关的,尽管正在开发不同的形式主义,一个答案集编程和后者的逻辑PC(ID)。
2011-05-03 cs.AI
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
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
AS2 -- Attention-Based Soft Answer Sets: An End-to-End Differentiable Neuro-Soft-Symbolic Reasoning Architecture
Clemson University(克莱姆森大学)
AS2提出一种端到端可微的神经-软符号推理架构,通过软连续近似替代离散求解器,实现约束满足反馈的可微传递,提升在视觉数独和MNIST加法任务中的性能。
2026-11-05 cs.AI
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
Translation-based Constraint Answer Set Solving
NICTA(国家信息与通信技术研究院);University of New South Wales(新南威尔士大学)
我们通过转换到回答集编程(ASP)来解决约束满足问题。我们的重新制定的属性,单位传播的ASP求解器实现定义良好的局部一致性属性,如弧,边界和范围的一致性。实验证明了这种方法的计算价值。
2011-04-20 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
Constraint Answer Set Programming: Integrational and Translational (or SMT-based) Approaches
University of Nebraska Omaha(内布拉斯加大学奥马哈分校)
约束回答集编程(英语:Constraint answer set programming,缩写为CASP)是一种自动推理的混合方法,它综合了回答集编程、约束处理和可满足性模理论等不同研究领域的进展。约束答案集编程展示了有希望的结果,包括开发了大量的求解器:acsolver,clingcon,ezcsp,idp,inca,dingo,mingo,aspmt,clingo[l,dl]和ezsmt。它为声明式编程应用程序(如解决复杂的训练调度问题)开辟了新的视野。系统的设计,以找到解决方案,约束答案集程序可以分组,根据他们的建设,我们称之为,整合或翻译的方法。本文的重点是一个概述的关键成分的设计约束答案集求解器之间的区别和平行的集成和翻译的方法。本文还提供了一个一瞥,其用户开发的程序,利用CASP编码的旅行推销员问题的说明。此外,我们把CASP技术在地图上的自动推理同行之间,以及讨论未来的可能性,CASP的发展。
2021-07-17 cs.AI
Planning with Incomplete Information in Quantified Answer Set Programming
New Mexico State University(新墨西哥州立大学);Omaha State University(奥马哈州立大学);University of Potsdam(波茨坦大学)
我们提出了一个通用的方法来规划与不完全信息的答案集编程(ASP)。更确切地说,我们考虑的问题,符合和条件规划与感知行动和假设。我们表示规划问题,使用一个简单的形式主义,其中逻辑程序描述的状态,初始状态和目标状态之间的过渡函数。为了解决规划问题,我们使用量化答案集编程(QASP),ASP的扩展与原子上的存在和通用量词类似于量化布尔公式(QBF)。我们定义了量化的逻辑程序的语言,并用它来表示符合和条件规划的不同变体的解决方案。在实践方面,我们提出了一个基于约束的QASP求解器,量化的逻辑程序转换成QBF,然后执行QBF求解器,我们实验评估的方法一致性和条件规划基准。正在考虑接受TPLP。
2021-08-13 cs.AI
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
A survey of advances in epistemic logic program solvers
Space and Naval Warfare Systems Center Atlantic(大西洋太空与海战系统中心);College of Charleston(查尔斯顿学院)
最近对答案集编程扩展的研究包括对认知规范语言的重新兴趣,它增加了模态运算符K(“已知”)和M(“可能是真的”),以提供更强大的内省推理和增强的能力,特别是在不完整信息的推理时。认知逻辑程序是这种语言中的一组规则。注入了研究一直是一个有效的解决方案,使实际使用这样的程序解决问题的愿望。在本文中,我们报告的认知逻辑程序求解器的发展现状。
2018-09-19 cs.AI
Abstract Modular Systems and Solvers
University of Nebraska at Omaha(内布拉斯加大学奥马哈分校);University of Kentucky(肯塔基大学)
将不同的形式主义集成到模块化知识表示系统中提供了更高的表达性、建模便利性和计算优势。我们引入抽象模块和抽象模块化系统的概念来研究集成异构多逻辑系统的模型查找程序或求解器的设计和分析背后的一般原理。我们展示了抽象模块和抽象模块化系统如何产生过渡系统,这是一个自然和方便的表示,求解器开创了SAT社区。我们说明了我们的方法,显示它如何适用于回答集编程和命题逻辑,并基于这两个形式主义的多逻辑系统。
2013-12-20 cs.AI
A Parallel Memory-efficient Epistemic Logic Program Solver: Harder, Better, Faster
Space and Naval Warfare Systems Center Atlantic(大西洋空间与海战系统中心);College of Charleston(查尔斯顿学院);New Mexico State University(新墨西哥州立大学)
由于答案集编程(ASP)的实际使用已经增长与发展的高效求解器,我们期望在ASP的扩展越来越感兴趣,因为它们的语义稳定和求解器支持他们成熟。认知规范(Epistemic Specifications)就是这样一种扩展,它将模态运算符K和M添加到ASP语言中。我们把这种语言中的程序称为认知逻辑程序(ELP)。由于搜索空间的指数增长,求解器迄今为止仅适用于最简单的ELP。我们描述了一种能够更好地解决更难的问题的求解器(例如,没有指数增长的存储器需求w.r.t. K和M出现),比任何其他已知的ELP求解器更快。
2016-10-13 cs.AI
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
Extending Answer Set Programs with Neural Networks
Arizona State University(亚利桑那州立大学)
低级感知与高级推理的集成是人工智能中最古老的问题之一。最近,提出了几个建议,以实现复杂的神经网络架构的推理过程。虽然这些工作的目的是扩展神经网络的推理能力,一个自然的问题,我们认为是:我们可以扩展答案集程序与神经网络,以允许复杂的和高层次的推理神经网络的输出?作为一个初步的结果,我们提出了NeurASP -一个简单的扩展答案集程序,通过拥抱神经网络,其中神经网络输出被视为概率分布在原子事实的答案集程序。我们表明,NeurASP不仅可以提高预先训练的神经网络的感知精度,而且还有助于训练一个神经网络更好地通过逻辑规则的限制。然而,由于内部使用符号推理引擎,使用NeurASP进行训练将比纯神经网络训练花费更多的时间。对于未来的工作,我们计划研究解决NeurASP可扩展性问题的潜在方法。一种潜在的方法是将逻辑程序直接嵌入到神经网络中。在这条路线上,我们计划首先设计一个SAT求解器使用神经网络,然后扩展这样的求解器,以允许逻辑程序。
2020-09-22 cs.AI
Anytime Computation of Cautious Consequences in Answer Set Programming
University of Calabria(卡拉布里亚大学)
在回答集编程(ASP)中,查询回答通常通过计算逻辑程序的谨慎结果(的子集)来解决。这个任务在计算上是非常困难的,并且存在计算谨慎后果在合理时间内不可行的程序。然而,目前的ASP求解器只在计算结束时才产生(整个)一组谨慎的后果。本文报告了计算谨慎后果的策略,还介绍了随时算法能够产生声音的答案在计算过程中。
2014-09-15 cs.AI
Translating Answer-Set Programs into Bit-Vector Logic
Aalto University School of Science(阿尔托大学理学院)
答案集编程(ASP)是一种用于声明性问题解决的范例,其中问题首先被形式化为规则集,即,答案集程序,在一个统一的方式,然后通过计算程序的答案集解决。可满足性模理论(SMT)框架遵循类似的建模哲学,但语法是基于命题逻辑的扩展,而不是规则。最近,提供了从答案集程序到差分逻辑的翻译-使特定SMT求解器能够用于答案集的计算。在本文中,翻译的另一个SMT片段,即固定宽度的位向量理论的基础上进行了修改。因此,甚至可以利用更多的SMT求解器来计算答案集。初步的实验比较的结果也报告。他们建议的性能水平,这是通过不同的逻辑实现类似。
2011-08-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
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
Modeling Variations of First-Order Horn Abduction in Answer Set Programming
Institut für Logic and Computation(逻辑与计算研究所);Technische Universität Wien(维也纳技术大学);Marmara University(马尔马拉大学)
我们研究绑架在一阶角逻辑理论,所有的原子都可以被绑架,我们正在寻找首选的解决方案,就三个目标函数:基数极小,连贯性和加权绑架。我们表示这个推理问题的答案集编程(ASP),以获得一个灵活的框架,实验与全球的约束条件和目标函数,并测试什么是可能的ASP的边界。在ASP中实现这个问题是具有挑战性的,因为它需要在某些常量之间创造值和等价,因为唯一名称假设通常不成立。为了允许循环理论的推理,我们正式描述细粒度的变化限制Skolemization。我们确定长期等价作为一个主要的实例化瓶颈,并提高我们的方法的效率与按需约束,用于消除相同的瓶颈,在国家的最先进的求解器。我们评估我们的方法实验上的ACCEL基准计划识别自然语言理解。我们的编码是公开的,模块化的,我们的方法比ACCEL基准测试中最先进的求解器更有效。
2018-01-31 cs.AI
A System for Interactive Query Answering with Answer Set Programming
Universität Potsdam(波茨坦大学);Simon Fraser University(西蒙弗雷泽大学);Griffith University(格里菲斯大学)
反应式答案集编程为将在线信息纳入操作解决过程铺平了道路。虽然这项技术最初是为了处理动态环境中的数据流而设计的,比如辅助生活和认知机器人,但它同样可以用于整合用户提供的事实、规则或查询。因此,我们提出了一个系统的设计和实现的交互式查询回答与反应式答案集编程。我们的系统quontroller是基于反应求解器oclingo和实现作为一个专用的前端。我们描述了它的功能和实现,并通过一些选定的用例说明了它的功能。
2013-12-20 cs.AI
Answer Set Planning: A Survey
New Mexico State University(新墨西哥州立大学);Saint Joseph’s University(圣约瑟夫大学);University of Potsdam(波茨坦大学)
答案集规划是指使用答案集编程(ASP)来计算计划,即,规划问题的解决方案,将世界的一种状态转变为另一种状态。高效和可扩展的答案集求解器的发展提供了一个显着的推动基于ASP的规划系统的发展。本文综述了在过去的25年中,在回答集规划领域取得的进展,从它的基础到它在具有挑战性的规划领域中的应用。该调查探讨了答案集规划的优点和缺点。它还讨论了答案集规划的典型应用,并提出了一系列未来研究的挑战。
2022-02-11 cs.AI
Hybrid Answer Set Programming: Foundations and Applications
University of Potsdam(波茨坦大学)
针对标准回答集编程(ASP)求解器无法处理数值及复杂约束的问题,提出带约束的此处与彼处逻辑(HT_c)作为理论基础,为混合ASP提供支持,同时探讨其理论特征与应用价值。
2025-02-13 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
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
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
aspps --- an implementation of answer-set programming with propositional schemata
我们提出了一个答案集编程范例的实现,称为aspps(答案集编程与命题模式的缩写)。系统aspps是为处理PS+理论而设计的。它包括两个基本模块。第一个模块psgrnd为PS+理论奠定了基础。第二个模块,称为aspps,是一个求解器。它计算地面PS+理论的模型。
2001-07-19 cs.AI cs.LO
Automated Aggregator -- Rewriting with the Counting Aggregate
University of Kentucky(肯塔基大学)
答案集编程是一种领先的声明式约束编程范式,广泛用于复杂的知识密集型应用程序。现代答案集程序设计语言支持许多等效的方法来对程序中的约束和规范进行建模。然而,到目前为止,答案集编程还没有开发出系统的方法来构建表示,这将统一地提供自动化处理。这表明,编码选择,以同样的方式选择算法和组合求解,可能是一个可行的方向,以提高性能的答案集求解。必要的先决条件是自动生成可能的替代编码的过程。在这里,我们提出了一个自动重写系统,自动聚合器或AAgg,给出了一个非地面逻辑程序,产生一个家庭的等效程序与互补的性能时,运行在现代的答案集编程求解器。我们通过实验分析证明了这种行为,并提出了该系统的使用自动答案集编程求解器选择工具。
2020-09-22 cs.AI cs.LO
Possibilistic Answer Set Programming Revisited
University of Washington(华盛顿大学);Vrije Universiteit Brussel(布鲁塞尔自由大学);Universiteit Gent(根特大学)
可能性答案集编程(PASP)通过为每个规则附加一定程度的确定性来扩展答案集编程(ASP)。虽然从应用程序的角度来看,这样的扩展是重要的,但现有的语义并没有很好的动机,并且并不总是产生直观的结果。为了开发一个更合适的语义,我们首先介绍了一个典型的ASP程序的答案集的可能性逻辑方面的表征,其中ASP程序指定了一组约束的可能性分布。然后自然地将这种特征推广到定义PASP程序的答案集。我们还提供了一个语法对应,导致一个可能性的推广著名的Gelfond Lifschitz约简,我们展示了我们的框架可以很容易地使用标准的ASP求解器来实现。
2012-03-15 cs.AI
eclingo: A solver for Epistemic Logic Programs
University of Corunna(拉科鲁尼亚大学);University of Potsdam(波茨坦大学)
我们描述eclingo,一个求解器的认知逻辑程序下Gelfond 1991年语义建立在回答集编程系统clingo。eclingo的输入语言使用clingo的语法扩展功能来定义主观文字,就像在认知逻辑程序中一样,允许在程序的所有或部分答案集中检查常规文字的真实性。eclingo解决过程遵循猜测和检查策略。它首先为主观文字生成潜在的真值,在第二步中,它检查所获得的结果与程序的谨慎和勇敢的后果。这个过程是使用clingo的多镜头功能来实现的。我们还实现了一些优化,旨在减少搜索空间,从而提高eclingo在某些情况下的效率。最后,我们比较了eclingo的效率与两个国家的最先进的求解器的认知逻辑程序对基准的情况下,表明eclingo一般优于他们得到的结果。正在考虑接受TPLP。
2020-08-05 cs.AI cs.LO
Knowledge-Graph Paths as Intermediate Supervision for Self-Evolving Search Agents
Xiaohongshu Inc.(小红书公司)
本文通过利用知识图谱路径作为中间监督,改进自演化搜索代理的提问生成和奖励塑造,解决传统方法中提问孤立和奖励信息不足的问题,提升多跳问答性能。
2026-05-07 cs.AI
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
Strong Equivalence in Answer Set Programming with Constraints
University of Corunna(拉科鲁尼亚大学);University of Nebraska Omaha(内布拉斯加大学奥马哈分校);University of Potsdam(波茨坦大学);Potassco Solutions(Potassco解决方案公司)
本文研究带约束回答集编程中的强等价性,证明其可由带约束的 Here-and-There 逻辑等价性刻画,并给出从 clingo 类求解器语言到该逻辑的翻译,同时分析了判定强等价性的计算复杂度。
2025-02-06 cs.AI cs.LO
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
PDDL+ Planning via Constraint Answer Set Programming
Drexel University(德雷塞尔大学);University of Genoa(热那亚大学)
PDDL+是PDDL的一个扩展,它可以用混合离散-连续动态来建模规划域。在本文中,我们提出了一种新的方法,PDDL+规划的基础上约束回答集编程(CASP),即ASP规则加数值约束。据我们所知,我们是第一次尝试连接PDDL+规划和逻辑编程。我们提供了一个编码的PDDL+模型到CASP问题。该编码可以处理非线性混合域,并为将逻辑编程应用于PDDL+规划奠定了坚实的基础。作为一个案例研究,我们考虑EZCSP CASP求解器,并获得了一组PDDL+基准问题有前途的结果。
2016-08-31 cs.AI
SUNNY: a Lazy Portfolio Approach for Constraint Solving
Department of Computer Science and Engineering/Lab. Focus INRIA University of Bologna(博洛尼亚大学计算机科学与工程系/INRIA Focus实验室)
* 出现在逻辑编程理论与实践(TPLP)中 * 在约束求解的背景下,组合方法允许人们利用不同求解器之间的协同作用,以创建全局更好的求解器。在本文中,我们提出了SUNNY:一个简单而灵活的算法,利用投资组合的约束求解器,以计算-没有学习一个明确的模型-一个时间表,他们解决一个给定的约束满足问题(CSP)。受到SUNNY与其他最先进方法的不同模拟所达到的性能的激励,我们开发了sunny-csp,这是一种有效的投资组合求解器,它利用底层的SUNNY算法来求解给定的CSP。对MiniZinc模型的详尽基准进行的实证测试表明,SUNNY的实际表现符合预测。这对于提高CSP组合求解器的能力以及尝试将它们导出到诸如答案集编程和约束逻辑编程等领域都是令人鼓舞的。
2014-05-13 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
Complexity and Compilation of GZ-Aggregates in Answer Set Programming
University of Calabria(卡拉布里亚大学)
Gelfond和Zhang最近提出了一种新的基于恶性循环原理的稳定模型语义,以改善对具有聚集的逻辑程序的解释。本文重点讨论了这种新语义下的一致性测试和谨慎推理的复杂性。一些令人惊讶的结果凸显了与主流聚合稳定模型语义的相似之处和差异。此外,该文件报告的编译技术的设计,实现新的语义上现有的ASP求解器,最终导致实现一个原型系统,允许实验Gelfond张的聚合。出现在逻辑编程理论与实践(TPLP),ICLP 2015会议记录。
2015-07-14 cs.AI
Qsmodels: ASP Planning in Interactive Gaming Environment
Università degli studi di Milano(米兰大学);Università degli studi di Messina(墨西拿大学)
Qmodels是一个新的应用答案集编程的互动游戏环境。我们描述了一个软件架构,通过它,一个机器人在雷神之锤3竞技场内的行为可以由一个计划者控制。规划器被编写为答案集程序,并由Smodels求解器解释。
2015-05-27 cs.AI
A Proof-of-Concept for Explainable Disease Diagnosis Using Large Language Models and Answer Set Programming
本研究提出McCoy框架,结合大型语言模型与答案集编程,实现可解释的疾病诊断,初步结果显示其在小规模诊断任务中表现优异。
2025-12-30 cs.AI
Weight Learning in a Probabilistic Extension of Answer Set Programs
School of Computing, Informatics and Decision Systems Engineering(计算、信息与决策系统工程学院);Arizona State University(亚利桑那州立大学)
LPMLN是答案集程序的概率扩展,其权重方案源自马尔可夫逻辑。以前的工作已经表明如何在LPMLN推理可以实现。本文提出了LPMLN中权学习的概念,并从Markov逻辑的权学习算法中导出了LPMLN的学习算法。我们还提出了一个原型实现,使用答案集求解器的学习,以及一些示例域,说明不同的LPMLN学习功能。在LPMLN学习是根据稳定的模型语义,从而学习参数的概率扩展知识丰富的领域,答案集编程已被证明是有用的,但限于确定性的情况下,如可达性分析和推理的行动在动态域。我们还应用该方法来学习参数的概率溯因推理的行动。
2018-10-09 cs.AI
Answering the "why" in Answer Set Programming - A Survey of Explanation Approaches
Institut de Recherche en Informatique de Toulouse (IRIT)(图卢兹计算机科学研究所);Université de Toulouse(图卢兹大学);Technische Universität Darmstadt(达姆施塔特工业大学)
人工智能(AI)解决问题和决策的方法变得越来越复杂,导致解决方案的可理解性降低。欧盟新的《通用数据保护条例》试图通过规定人工智能系统所做决定的“解释权”来解决这一问题。可能受到这一新规定影响的人工智能范例之一是答案集编程(ASP)。由于出现了高效的解决方案,ASP最近已被用于解决各种领域的问题,包括医学,密码学和生物学。为了确保成功应用ASP作为解决问题的范例在未来,ASP解决方案的解释是至关重要的。在这项调查中,我们给出了一个概述的方法,提供了一个答案的问题,为什么答案集是一个解决方案,一个给定的问题,特别是离线的理由,因果图,论证性的解释和为什么不出处,并强调他们的相似性和差异。此外,我们审查的方法解释为什么一组文字是不是一个答案集或为什么没有解决方案存在于所有。
2018-09-21 cs.AI
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
Automated verification of weak equivalence within the SMODELS system
在答案集编程(ASP)中,通过(i)编写其答案集对应于问题的解的逻辑程序,以及通过(ii)使用答案集求解器作为搜索引擎来计算程序的答案集,来解决手头的问题。通常,程序员在优化程序长度和特定求解器上的执行时间时,为特定问题创建一系列逐渐改进的逻辑程序。这将程序员引向确保程序是等效的元级问题,即,它们产生相同的答案集。为了在方法层面简化答案集编程,我们提出了一种基于翻译的方法来验证逻辑程序的等效性。其基本思想是将所考虑的逻辑程序P和Q转换为单个逻辑程序EQT(P,Q),其答案集(如果存在的话)产生P和Q等价的反例。该方法是在这里开发的一个稍微更一般的设置时,考虑到原子的可见性比较答案集。本文提出的基于推理的方法已被实现为一个翻译器,称为lpeq,使验证弱等价的模型系统内使用相同的搜索引擎的搜索模型。我们用lpeq和smodels进行的实验表明,在某些情况下,用这种方式建立逻辑程序的等价性比简单的交叉检查答案集要快得多。
2006-08-25 cs.AI cs.LO
diff-SAT -- A Software for Sampling and Probabilistic Reasoning for SAT and Answer Set Programming
National University of Ireland, Galway(爱尔兰国立高威大学)
本文介绍了diff-SAT,一个答案集和SAT求解器,它结合了经常使用概率条款,事实和规则的能力,解决和采样的最佳世界观(满足布尔变量分配或答案集的多集)受用户提供的概率约束。采样过程使用称为可微可满足性求解($\partial\mathrm{SAT}$)或可微答案集编程($\partial\mathrm{ASP}$)的基于梯度下降的优化方法来最小化用户定义的可微目标函数。用例是i.a.概率逻辑编程(以概率答案集编程的形式),概率布尔可满足性求解(PSAT)和模型多集(答案集或布尔解释)的分布感知采样。
2021-01-03 cs.AI cs.LO
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
Automata Techniques for Temporal Answer Set Programming
University of Potsdam(波茨坦大学)
回答集编程(ASP)的时态和动态扩展在解决动态问题方面发挥了重要作用,因为它们允许使用时态运算符以非常有效的方式对动态场景进行推理。在我的博士学位上。研究,我打算利用自动机理论和动态逻辑之间的关系,添加自动机为基础的技术,以ASP求解器CLINGO帮助我们处理这些类型的问题。
2021-09-17 cs.AI cs.FL cs.LO
Answer Set Networks: Casting Answer Set Programming into Deep Learning
TU Darmstadt(达姆施塔特工业大学);TU Eindhoven(埃因霍温理工大学);Hessian Center for AI (hessian.AI)(黑森人工智能中心(hessian.AI));German Research Center for AI (DFKI)(德国人工智能研究中心(DFKI))
提出基于图神经网络的回答集网络(ASN),将回答集编程引入深度学习,利用GPU并行计算高效求解,在多任务上优于现有CPU受限的神经符号系统,并首次实现用逻辑引导微调大型语言模型及无人机宪法导航。
2026-10-06 cs.AI cs.LG cs.SC
Generalizing Level Ranking Constraints for Monotone and Convex Aggregates
Tampere University(坦佩雷大学);Aalto University(阿尔托大学)
本研究泛化层级排序约束以系统支持ASP中的单调与凸聚合,通过程序变换得到通用形式,为翻译型ASP实现提供统一基础。
2023-08-30 cs.AI cs.LO
Going Beyond Approximation: Encoding Constraints for Explainable Multi-hop Inference via Differentiable Combinatorial Solvers
University of Manchester(曼彻斯特大学);Idiap Research Institute(Idiap研究所)
线性规划(ILP)提供了一种可行的机制来编码关于自然语言可解释的多跳推理的显式和可控的假设。然而,ILP公式是不可微的,并且不能集成到更广泛的深度学习架构中。最近,Thayaparan等人(2021 a)提出了一种新的方法,将ILP与Transformers集成,以实现复杂多跳推理的端到端可区分性。虽然这种混合框架已被证明提供更好的答案和解释选择比变压器为基础的和现有的ILP求解器,神经符号积分仍然依赖于凸松弛的ILP制定,这可能会产生次优的解决方案。为了改善这些限制,我们提出了Diff-Comb Explainer,这是一种基于可微分黑盒组合求解器(DBCS)的新型神经符号架构(Pogančić et al.,2019年)。与现有的可微求解器,所提出的模型不需要的显式语义约束的转换和放松,允许直接和更有效的集成ILP配方。Diff-Comb Explainer比不可微求解器、Transformers和现有的基于可微约束的多跳推理框架具有更高的准确性和可解释性。
2022-08-05 cs.AI cs.CL