May, 2019

基于SMT的约束答案集求解器EZSMT+

HTML
PDF
TL;DR该研究使用基于满足性模理论求解器的约束应答集编程工具EZSMT+，其理论基础是通过所谓的级别排名对逻辑程序的应答集进行推广的Niemela的表征。
发现论文，激发创造
  • 具有学习功能的抽象答案集求解器

    本文利用转换系统来描述多种逻辑程序的答案集求解器，使得更容易证明它们的正确性、比较它们以及设计新的系统。

    Jan, 2010

  • 基于翻译的约束型答案集求解

    使用将约束满足问题转化为答案集编程的方式解决问题，实验表明该方法具有单位传播、本地一致性等特性，具有计算价值。

    Apr, 2011

  • 基于答案集规划的求解器调度

    本研究提出了一种使用 Answer Set Programming 自动确定精细的、非均匀且有序的求解器调度方案的方法，并且可以定制化地生成并行调度方案。

    Jan, 2014

  • 基于模板的析取答案集求解器

    本文介绍了使用转换系统来建模和分析矛盾性答案集求解器的方法，展示了该方法对于分析、比较和证明搜索算法正确性以及启发新的求解器设计是多么有效。同时，我们引入了通用模板，以设计多种技术在不同求解器中的组合，并证明了它对于捕捉DLV、GnT和Cmodels等求解器这样的主要技术的能力。

    Oct, 2015

  • lpopt: 用于答案集编程的规则优化工具

    介绍了 lpopt 工具，该工具可以将大型逻辑编程规则分解成更小的规则以提高现有求解程序的性能。

    Aug, 2016

  • 约束求解器EZCSP及其集成架构的重要性

    本研究提出了约束应答集编程 Constraint Answer Set Programming （CASP）新研究领域，开发相应的EZCSP语言及其解释器并对其进行了系统性的研究，其设计和算法细节清晰地证明了这种混合系统的发展具有挑战性。在此基础上，展开了基于EZCSP的案例研究，重点关注其提供的各种集成方式。

    Feb, 2017

  • Clingcon:下一代

    本篇论文介绍了第三代约束答案集系统 clingcon，它将 Answer Set Programming（ASP）与有限域约束处理（CP）相结合，并采用惰性方法实现对约束传播的扩展。

    May, 2017

  • 更少资源实现更好的拟交一致答案集

    本文介绍了一个用于计算划分半平衡模型的高效评估技术，以获取更好的语义解释的应用程序答案集，比现有方法消耗更小的计算资源。

    Jul, 2019

  • 约束答案集编程：集成与转化（或基于SMT的）方法

    本文提出了 Constraint answer set programming 技术的概述，重点介绍了整合法和翻译法两种设计 Constraint answer set 求解器的方法，并提供了一个基于该技术的 Traveling Salesman Problem 的编码实例。

    Jul, 2021

  • 推广级别排名约束用于单调及凸聚合函数

    在该论文中，作者重新考虑了级别排序约束，旨在更系统地覆盖基于聚合的ASP扩展。通过应用一系列程序转换，级别排序约束可以以一般形式重写，从而保留了单调和凸聚合的结构，并为它们的整合提供了统一的基础。这些结果为翻译器和求解器管道的实际应用开辟了新的可能性。

    Aug, 2023