Core Challenge 2022: Solver and Graph Descriptions
Takehide Soh, Yoshio Okamoto, Takehiro Ito
本文收集了提交给Core Challenge 2022的求解器和ISR实例的所有描述。
This paper collects all descriptions of solvers and ISR instances submitted to CoRe Challenge 2022.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
继续探索
Core Challenge 2023: Solver and Graph Descriptions
本文收集并整理了提交至CoRe Challenge 2023的全部求解器与ISR实例描述，为相关研究提供参考。
Can LLMs Build a MaxSAT Solver from Papers? The CoreForge Experience
该研究利用大语言模型从论文构建无权重 MaxSAT 求解器，采用结合论文讨论、代码实现及审核修订的迭代流程，评估特定配置，发现虽未现错误答案，但性能低于手工设计求解器，总结了相关经验教训。
Scalable Parallel Numerical CSP Solver
我们提出了一个并行求解器的数值约束满足问题（NCSP），可以扩展的核心数量。我们提出的方法在可用的内核上运行工人求解器，同时工人合作进行搜索空间分配和平衡。在实验中，我们达到了119倍的加速比，使用256个核心的并行计算机。
New Core-Guided and Hitting Set Algorithms for Multi-Objective Combinatorial Optimization
在过去的十年中，已经提出了大量的单目标布尔优化算法，这些算法依赖于高效的命题可满足性（SAT）求解器的迭代使用。但是SAT求解器在多目标组合优化（MOCO）算法中的应用还很少。由于缺乏有效的MOCO工具，许多现实世界的应用程序制定为多目标简化为单目标，使用线性组合或字典排序的目标函数进行优化。在本文中，我们扩展了最先进的MOCO求解器与两个新的不可满足性为基础的算法。第一个是核心引导的MOCO求解器。第二个是基于命中集的MOCO求解器。在广泛的基准测试实例中获得的实验结果表明，我们的新的不可满足性为基础的算法可以优于最先进的SAT为基础的算法MOCO。
Modelling Constraint Solver Architecture Design as a Constraint Problem
设计基于组件的约束求解器是一个复杂的问题。有些组件是必需的，有些是可选的，并且组件之间存在相互依赖性。正因为如此，以前的方法求解器的设计和修改一直是特设的和有限的。我们提出了一个系统，转换成一个约束问题的组件和目标约束求解器的特性的描述。求解此问题将产生有效求解器的描述。我们的方法是一个重要的一步，自动化设计和合成的约束求解器，专门为个人的约束问题类或实例。
Scalable Parallel Numerical Constraint Solver Using Global Load Balancing
提出了一种求解数值约束满足问题的可扩展并行求解器。我们的并行化方案由同质的工人求解器，其中每一个运行在一个可用的核心，并通过全球负载均衡（GLB）的方法与他人进行通信。并行求解器是用X10实现的，X10提供了GLB的实现作为一个库。在实验中，几个NCSP从文献中解决，并获得高达516倍的加速比使用600个核心的TSUBAME2.5超级计算机。
System Descriptions of the First International Competition on Computational Models of Argumentation (ICCMA'15)
本卷包含提交给第一届国际辩论计算模型竞赛（ICCMA'15）的18个求解器的系统描述，因此概述了抽象辩论问题的最新计算方法。有关比赛结果和个人求解器性能的更多信息，请访问http://argumentationcompetition.org/2015/。
GOLD: Geometry Problem Solver with Natural Language Description
GOLD模型通过分别处理几何图中的符号与几何基元，将提取的几何关系转化为自然语言描述，并利用大语言模型求解几何题，在多个数据集上显著超越此前最佳方法。
Unsatisfiable Cores for Constraint Programming
约束编程（CP）求解器通常通过反复寻找问题的解决方案来解决优化问题，同时对解决方案的成本设置越来越严格的界限。这种方法有些幼稚，特别是对于软约束优化问题，其中软约束大多得到满足。在布尔可满足性中解决软约束问题的不可满足核方法（例如MAXSAT）强制所有软约束保持初始状态。当求解失败时，它们返回一个不可满足的核心，作为一组不能同时保持的软约束。使用该信息，问题被放松以允许违反某些软约束，并且求解继续。由于懒惰子句生成（LCG）求解器也可以返回不可满足的核心，我们可以将MAXSAT不可满足的核心方法应用于CP。我们实现了原来的MAXSAT不可满足的核心求解算法WPM1，MSU3在一个国家的最先进的LCG求解器，并表明存在的问题，受益于这种混合的方法。
A Neurodiversity-Inspired Solver for the Abstraction \& Reasoning Corpus (ARC) Using Visual Imagery and Program Synthesis
本文提出一种受神经多样性启发的核心知识AI方法，结合视觉表象表征与树搜索程序合成，在ARC挑战中取得第四名，展示了灵活组合核心知识解决新任务的能力。
D-Wave's Nonlinear-Program Hybrid Solver: Description and Performance Analysis
本文介绍 D-Wave 新增的 Nonlinear-Program Hybrid Solver，并基于旅行商、背包和最大割问题的 45 个实例评估其性能，同时提供实现细节。
FOLASP: FO(.) as Input Language for Answer Ser Solvers
在过去的几十年里，答案集编程（ASP）已经成为声明式问题解决的一个重要范例。这一领域的技术进步是由于使用了共同标准，例如ASP-Core-2语言。虽然ASP的根源在于非单调推理，但人们也努力使ASP与经典的一阶逻辑（FO）相协调。这导致了FO（.）的发展，FO的一个富有表现力的扩展，它允许在纯粹的经典环境中解决类似ASP的问题。这种语言对于已经熟悉FO的领域专家来说可能更容易使用，并且可能更容易与基于经典逻辑的其他形式主义结合。它由IDP推理系统支持，该系统已成功地参加了许多ASP竞赛。然而，在这里，可用于FO（.）的系统数量有限阻碍了技术进步。在本文中，我们的目标是通过一个转换FO（.）的翻译工具来解决这个问题。规范，从而允许ASP-Core-2求解器用作FO（.）也我们目前的实验结果表明，我们的翻译与现成的ASP求解器的组合是有竞争力的IDP系统作为一种解决问题的方式制定FO（。）。正在考虑接受TPLP。
From Natural Language to Solver-Ready Power System Optimization: An LLM-Assisted, Validation-in-the-Loop Framework
本文提出一种LLM辅助智能体，通过领域感知提示、系统性验证与迭代修复，将电力系统优化的自然语言描述转化为求解器就绪的数学公式并生成可靠解，有效提升了决策效率与解的可行性。
Bounded Fitting for Expressive Description Logics
本文研究了在扩展ALC的表达式描述逻辑中，受限适配方法的理论性质和实现，通过SAT求解器实现，并与现有概念学习器比较，展示了其在复杂概念学习中的实用性。
SAILOR: Solver-Assisted Interactive LLM-based Optimization Recovery
SAILOR系统利用求解器辅助交互，通过检测缺失数值并向用户提问，实现优化问题的完整建模，在七个基准上验证了可行性。
Regularization by Texts for Latent Diffusion Inverse Solvers
本文提出文本正则化方法TReg，通过在潜在扩散逆求解中引入文本描述与自适应否定机制，有效缓解逆问题的模糊性，提升求解的准确性与效率。
Query Answering in Object Oriented Knowledge Bases in Logic Programming: Description and Challenge for ASP
本文介绍ASP中大规模知识库KB_Bio_101及其查询程序，并解释这些查询对当前ASP求解器构成重大实际挑战的原因。
Elastic Solver: Balancing Solution Time and Energy Consumption
组合决策问题出现在许多不同的领域，例如调度、路由、包装、生物信息学等等。尽管最近在开发可扩展的求解器方面取得了进展，但仍然存在许多问题，这些问题往往很难解决。通常，最先进的求解器包括本质上是随机的元素。如果使用不同的种子多次求解同一个实例，则根据问题实例和求解器的固有特性，可以观察到跨越多个数量级的高度变化的时间分布。因此，为了有效地解决问题实例，使用不同的种子并行解决同一实例通常是有用的。随着云计算的普及，人们自然会想到一种弹性求解器，它可以通过在数千台机器（或核心）上并行启动搜索来扩展。然而，这可能导致消耗大量能量。而且，并不是每个副本都需要数千台机器。面临的挑战是解决一个给定的问题实例的解决方案的时间和能源消耗之间的权衡最优。我们分析了机器（或核心）的数量不仅对解决方案的时间，而且对能源消耗的影响。我们强调，虽然解决方案的时间总是随着机器数量的增加而下降，但机器数量和能源消耗之间的关系更加复杂。在许多情况下，最佳的能源消耗可能会实现一个中间地带，我们详细分析了这种关系。进一步研究了求解时间和能量消耗之间的权衡，表明如果我们稍微增加求解时间，求解器的能量消耗可以大大减少。我们还开发了一个预测模型，证明这种见解可以利用更快的解决方案的时间在一个更节能的庄园。
From Errors to Proofs: Minimal-Core-Guided Repair for Neuro-Symbolic Constraint Solving
该研究提出最小核心引导的修复方法，将语言模型生成的不可满足程序的错误消息替换为最小不可满足核心，在77个问题的基准上使弱模型编造不可行问题解的比例从79%降至7%，核心价值是提供证书并拒绝编造解。
ASP-Core-2 Input Language Format
求解器输入语言的标准化已经成为知识表示和推理中几个领域发展的主要驱动力，促进了实际应用中的开发。在本文档中，我们介绍了用于答案集编程的ASP-Core-2标准输入语言，该语言自2013年以来一直被ASP竞赛活动采用。
SATformer: Transformer-Based UNSAT Core Learning
本研究提出基于Transformer的SATformer方法，通过建模子句交互识别不可满足子问题，结合多任务学习训练，性能显著优于NeuroSAT，还能将现有SAT求解器运行时间平均缩短21.33%。
扫码添加微信好友，提出您的宝贵建议 👇
💡 备注请填写：网站反馈
发表机构由 AI 从论文文本抽取，如发现错误，欢迎反馈修正建议。