A Minesweeper Solver Using Logic Inference, CSP and Sampling
Yimin Tang, Tian Jiang, Yanpeng Hu
扫雷作为一个益智视频游戏，并证明它是一个NPC的问题.我们使用CSP、逻辑推理和采样来制作扫雷舰求解器，并且我们将每次选择限制在5秒内。
Minesweeper as a puzzle video game and is proved that it is an NPC problem. We use CSP, Logic Inference and Sampling to make a minesweeper solver and we limit us each select in 5 seconds.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
继续探索
Fast constraint satisfaction problem and learning-based algorithm for solving Minesweeper
扫雷是一个流行的基于空间的决策游戏，工作与不完全信息。作为一个典型的NP完全问题，它是一个主要的研究领域，采用各种人工智能范例。本文将此博弈模型化为约束满足问题和马尔可夫决策过程。提出了一种基于确定性解搜索的独立集依赖项方法（DSScp），用于快速枚举基于确定性解搜索的扫雷对策的所有解，并通过引入启发式算法对结果进行了改进.使用MDP，我们实现了机器学习方法对这些算法。我们训练稀疏数据的分类模型与CSP制定的结果。我们还提出了一种新的奖励方法，用于在扫雷游戏中应用改进的深度Q学习，以获得更好的准确性和多功能学习。对不同类型的扫雷游戏的总体结果进行了分析，并记录了其准确性。这些实验的结果表明，所提出的基于MDP的分类模型和深度Q学习的方法总体上是具有给定地雷密度的游戏的准确性方面的最佳方法。
Neural Network Learner for Minesweeper
扫雷是一个有趣的单人游戏的基础上逻辑，记忆和猜测。解决扫雷问题已经被证明是一个NP难的任务。确定性求解器是最著名的解决扫雷的方法。本计画提出一个以神经网络为基础的学习器来解决扫雷问题。为了选择最好的学习者，不同的神经网络架构和配置在数十万场比赛中进行训练。令人惊讶的是，所提出的神经网络为基础的学习者已被证明是一个非常好的近似函数解决扫雷。神经网络学习者与CSP求解器竞争得很好，特别是在游戏的初级和中级模式中。还观察到，尽管成功率很高，但最好的神经学习器比最好的确定性求解器慢得多。本报告还讨论了在为扫雷舰创建非常成功的神经网络时所面临的开销和限制。
Proteus: A Hierarchical Portfolio of Solvers and Transformations
近年来，解决SAT问题和CSP的组合方法越来越普遍。还有许多不同的编码用于将CSP表示为SAT实例。在本文中，我们利用SAT和CSP求解的进展，提出了一种新的分层投资组合为基础的方法来解决CSP，我们称之为Proteus，不纯粹依赖于CSP求解器。相反，它可以决定最好将CSP问题实例编码为SAT，选择适当的编码和相应的SAT求解器。我们的实验评估使用了一个实例的变形，涉及四个CSP求解器，三个SAT编码，和六个SAT求解器，评估最具挑战性的问题实例从CSP求解器的竞争，涉及全球和内涵的约束。我们表明，显着的性能改善，可以通过利用其他观点和求解器组合解决问题的变形。
Dr.Fill: Crosswords and an Implemented Solver for Singly Weighted CSPs
我们描述填充博士，一个程序，解决美国式的填字游戏。从技术的角度来看，菲尔博士的工作原理是将填字游戏转换为加权的csp，然后使用各种新颖的技术来找到解决方案。这些技术包括变量和值选择的一般适用的算法，有限差异搜索的变体，以及后处理和分区思想。没有使用分支和界限，因为它与后处理不兼容，并且实验确定没有什么实用价值。菲尔博士在美国填字游戏锦标赛上的填字游戏表现表明，它在世界上填字游戏的前五十名左右的选手中名列前茅。
Decentralized Constraint Satisfaction
我们发现，在无线网络中的几个重要的资源分配问题适合在共同的框架内的约束满足问题（CSP）。这些应用程序的要求，其中变量位于不同的网络设备，可能无法通信，但可能会干扰的启发，我们定义了自然的标准，CSP求解器必须具备，以实用。我们将这些算法称为分散式CSP求解器。最著名的CSP求解器是为集中式问题而设计的，不符合这些标准。我们介绍了一个随机分散CSP求解器，并证明了它会找到一个解决方案，在几乎肯定有限的时间，如果存在，也表明它有许多实际可取的属性。我们基准的算法的性能上的一个良好的研究类的CSP，随机k-SAT，说明该算法需要找到一个令人满意的分配的时间是有竞争力的随机集中式求解器的问题，为了一千个变量，尽管其分散的性质。我们证明了求解器的实际效用的问题，激励它的引入，用它来找到一个非干扰的信道分配从曼哈顿市中心的数据形成的网络。
Solution Dominance over Constraint Satisfaction Problems
约束满足问题（CSP）通常具有满足所有约束的许多解。然而，通常情况下，一些解决方案优于其他解决方案，也就是说，一些解决方案主导其他解决方案。我们目前的解决方案的优势作为一个正式的框架，理由这样的设置。我们将约束支配问题定义为具有支配关系的约束支配问题，即约束支配问题解的前序。该框架涵盖了约束满足的许多著名的变体，包括优化、多目标优化、Max-CSP、最小模型、最小校正子集以及CP-网和任意支配关系上的优化。我们扩展MiniZinc，一个声明性的语言建模CSP，通过引入优势nogoods的CDPs，这些可以从优势关系的原则性的方式。一种用于求解任意CDP的通用方法递增地调用CSP求解器，并且与任何支持MiniZinc的现有求解器兼容。这鼓励对一个问题尝试不同的解决方案支配关系，以及比较不同的求解器，而不必修改它们的实现。
SUNNY: a Lazy Portfolio Approach for Constraint Solving
* 出现在逻辑编程理论与实践（TPLP）中 * 在约束求解的背景下，组合方法允许人们利用不同求解器之间的协同作用，以创建全局更好的求解器。在本文中，我们提出了SUNNY：一个简单而灵活的算法，利用投资组合的约束求解器，以计算-没有学习一个明确的模型-一个时间表，他们解决一个给定的约束满足问题（CSP）。受到SUNNY与其他最先进方法的不同模拟所达到的性能的激励，我们开发了sunny-csp，这是一种有效的投资组合求解器，它利用底层的SUNNY算法来求解给定的CSP。对MiniZinc模型的详尽基准进行的实证测试表明，SUNNY的实际表现符合预测。这对于提高CSP组合求解器的能力以及尝试将它们导出到诸如答案集编程和约束逻辑编程等领域都是令人鼓舞的。
Scalable Parallel Numerical CSP Solver
我们提出了一个并行求解器的数值约束满足问题（NCSP），可以扩展的核心数量。我们提出的方法在可用的内核上运行工人求解器，同时工人合作进行搜索空间分配和平衡。在实验中，我们达到了119倍的加速比，使用256个核心的并行计算机。
Short Portfolio Training for CSP Solving
存在用于解决约束满足问题（CSP）和相关约束优化问题（COP）的许多不同方法。然而，有没有一个单一的求解器（或方法），以及所有类别的问题和许多投资组合的方法选择一个合适的求解器的基础上简单的语法功能的输入CSP实例已经开发。本文首先提出了一种基于k-近邻法的CSP投资组合方法。然后，我们提出了一种新的方法来使用组合系统-训练他们在开发时间短，特别是要解决的实例集，并使用它们在该集合上。已经进行了彻底的评估，并已表明，该方法产生良好的效果。我们为我们的投资组合评估了几种机器学习技术。由于其简单性和效率，选择k-最近邻方法特别适合我们的短训练方法，并且在测试方法中也产生了最好的结果。我们还证实，我们的方法在SAT域上产生了良好的效果。
Lifting Structural Tractability to CSP with Global Constraints
大范围的问题可以建模为约束满足问题（CSP），即必须同时满足的一组约束。约束既可以通过显式列出允许的值组合来扩展表示，也可以通过求解器提供的专用算法来隐式表示。这种隐式表示的约束（称为全局约束）被广泛使用;事实上，它们是约束编程在解决现实问题中取得成功的关键原因之一。近年来，已经确定了对产生易处理类的CSP实例的结构的各种限制。然而，许多这样的限制不能保证具有全局约束的CSP的易处理性。在本文中，我们调查的属性，这些限制利用扩展表示的约束，以实现易处理性，并表明，有大类的全球约束，也具有这些属性。这使我们能够解除这些限制的全球情况下，并确定新的听话类的CSP与全球约束。
An Empirical Evaluation of Portfolios Approaches for solving CSPs
最近的研究领域，如SAT求解和非线性规划表明，一个任意有效的求解器的性能可以显着优于一个投资组合的可能较慢的平均求解器。我们报告的实证评估和比较的投资组合方法适用于约束满足问题（CSP）。我们比较了在现成的机器学习算法上开发的模型与SAT领域中使用的方法，并适用于CSP，考虑不同的投资组合规模，并使用解决问题的数量和解决问题所需的时间作为评估指标。结果表明，最好的SAT方法在CSP领域也具有最佳性能，并且比基于分类算法的简单模型更具竞争力。
Structural Decompositions for Problems with Global Constraints
大范围的问题可以建模为约束满足问题（CSP），即必须同时满足的一组约束。约束既可以通过显式列出允许的值组合来扩展表示，也可以通过求解器提供的专用算法来隐式表示。这种隐式表示的约束（称为全局约束）被广泛使用;事实上，它们是约束编程在解决现实问题中取得成功的关键原因之一。近年来，CSP实例的结构上的各种限制已被证明可以产生易于处理的CSP类。然而，大多数这样的限制不能保证具有全局约束的CSP的可处理性。因此，我们研究的适用性，结构性限制的情况下，这样的约束。我们表明，当CSP实例的解决方案的数量是有界的关键部分的问题，结构的限制，可以用来派生新的听话的类。此外，我们表明，这一结果扩展到组合的实例从已知的听话的类，以及CSP的情况下，约束分配成本，以满足任务。
Perturbed Message Passing for Constraint Satisfaction Problems
我们介绍了一种有效的消息传递方案解决约束满足问题（CSP），它使用随机扰动的信念传播（BP）和调查传播（SP）消息绕过抽取，直接产生一个单一的满意的分配。我们的第一个CSP求解器，称为扰动Blief传播，平滑地插值两个众所周知的推理过程;它开始于BP，结束于Gibbs采样器，它从一组解决方案中产生一个样本。此外，我们应用类似的扰动计划SP产生另一个CSP求解器，扰动调查传播。在随机和真实世界的CSP上的实验结果表明，扰动BP通常更成功，同时比标准BP引导抽取效率高数十到数百倍。扰动BP还可以与最先进的SP引导抽取相媲美，SP引导抽取具有计算复杂性，通常比我们的方法（变量域和约束的基数）更差。此外，我们的随机可满足性和着色问题的实验表明，扰动SP可以优于SP指导的抽取，使其成为最好的不完全随机CSP求解困难的制度。
Building a Truly Distributed Constraint Solver with JADE
现实生活中的问题，如调度会议之间的人在不同的位置可以建模为分布式约束满足问题（CSP）。然后可以使用约束满足算法找到合适的和满意的解决方案，该算法可以是穷举的（回溯）或其他的（局部搜索）。然而，在这一领域的大多数研究测试他们的算法模拟在一台PC上，一个单一的程序入口点。我们的工作的主要贡献是设计和实现了一个真正的分布式约束求解器的基础上，使用Java代理DEFERMEMENT框架（JADE）的本地搜索算法，使不同机器上的代理之间的通信。特别是，我们讨论了真正的分布式约束求解器，这可能不是关键时，在一台机器上模拟的设计和实现问题。评估结果表明，我们真正的分布式约束求解器的工作以及在所观察到的限制，当测试与各种分布式CSP。我们的应用程序也可以采用任何约束求解算法，只需很少的修改。
CAST: Game Solvers as Turn-Level Teachers for LLM Agents
研究如何训练大语言模型在长期游戏中决策，提出CAST方法，利用游戏求解器状态值变化转化为求解器优势并注入RLVR，在多个游戏中优于基线，实现高平均零样本性能。
FourierCSP: Differentiable Constraint Satisfaction Problem Solving by Walsh-Fourier Expansion
FourierCSP通过沃尔什-傅里叶展开实现对通用约束满足问题的高效求解，扩展了连续局部搜索框架，提高了求解效率并推动神经符号整合的发展。
An Enhanced Features Extractor for a Portfolio of Constraint Solvers
最近的研究表明，一个任意有效的求解器可以显着优于一个投资组合的可能较慢的平均求解器。求解器的选择通常是通过（非）监督学习技术，利用从问题规范提取的功能。在本文中，我们提出了一个有用的和灵活的框架，能够提取一个广泛的功能集的约束（满意度/优化）可能不同的建模语言定义的问题：MiniZinc，FlatZinc或XCSP。我们还报告了一些实证结果表明，使用这些功能可以获得的性能是有效的，具有竞争力的最先进的CSP投资组合技术。
A Neurosymbolic Fast and Slow Architecture for Graph Coloring
本文提出神经符号双系统架构SOFAI_v2，通过元认知协调LLM快速求解与符号审慎求解，在图着色任务上显著提升成功率和速度。
Deep Reinforcement Learning for Combinatorial Optimization: Covering Salesman Problems
本文介绍了一种新的深度学习方法来近似解决覆盖推销员问题（CSP）。在这种方法中，给定CSP的城市位置作为输入，深度神经网络模型被设计为直接输出解决方案。它是在没有监督的情况下使用深度强化学习训练的。具体而言，在模型中，我们应用多头注意力来捕捉结构模式，并设计了一个动态嵌入来处理问题的动态模式。一旦模型经过训练，它就可以推广到各种类型的CSP任务（不同大小和拓扑），而不需要重新训练。通过控制实验，所提出的方法显示出理想的时间复杂度：它运行速度比传统的启发式求解器的最优性的微小差距超过20倍。此外，它在训练和推理方面都明显优于当前最先进的组合优化深度学习方法。与传统的求解器相比，这种方法对于实践中大多数具有挑战性的任务都是非常可取的，这些任务通常是大规模的，需要快速决策。
Dsat: A Native SAT Solver for Discrete Logic
本文提出一种用于离散逻辑的原生SAT求解器，通过扩展布尔逻辑，允许变量取任意值，并通过与CSP求解器、布尔SAT求解器等的比较验证其有效性。
LLM-Guided Evolutionary Search for Constraint Model Reformulation to Improve Solver Efficiency
本研究提出LLM引导的进化框架，引入PDR策略保留多样化上下文，在8个CSPLib问题上验证迭代重构可提升求解速度，且多样化上下文策略和验证选择均能增强加速效果。
A Complete Solver for Constraint Games
博弈论研究多个目标相互冲突的代理人必须达成集体决策的情况。代理效用函数的一个紧凑的表示语言的问题是至关重要的，因为一个$n$的球员游戏的经典表示是由一个$n$维矩阵的指数大小为每个球员。在本文中，我们使用的约束博弈的框架中，CSP被用来代表效用。约束编程-包括全局约束-允许轻松地为许多有用的游戏提供紧凑而优雅的模型。约束博弈有两种形式：约束满足博弈和约束优化博弈，第一种使用满足来定义布尔效用。除了多矩阵游戏，它也可以模拟更复杂的游戏，其中硬约束禁止某些情况。在本文中，我们研究了完整的搜索技术，并表明，我们的求解器使用的紧凑表示的约束游戏是快于经典的游戏求解器Gambit的一到两个数量级。
Ludii and XCSP: Playing and Solving Logic Puzzles
许多著名的单人游戏，通常被称为拼图，可以被证明是NP完全的。事实上，这类复杂性包含数百个谜题，因为人们特别喜欢完成一个棘手的谜题，比如数独，但也喜欢在完成后轻松检查解决方案的能力。出于这个原因，使用约束编程自然适合于解决它们。在本文中，我们专注于逻辑谜题描述的Ludii一般的游戏系统，我们建议使用XCSP形式主义，以解决他们与任何CSP求解器。
A framework for step-wise explaining how to solve constraint satisfaction problems
我们探索逐步解释如何解决约束满足问题的问题，与逻辑网格谜题的用例。更具体地说，我们研究的问题，解释的推理步骤，可以在传播过程中，以一种方式，很容易解释一个人。因此，我们的目标是给约束求解器可解释的机构，这可以帮助建立信任的求解器能够理解，甚至从解释中学习。主要的挑战是找到一系列简单的解释，每个解释都应该尽可能容易地让人类验证和理解。这与求解器在传播时可能使用的事实和约束的任意组合形成对比。我们建议使用成本函数来量化一个推理步骤的单个解释有多简单，并确定寻找CSP的最佳解释序列的解释-生产问题。我们的方法是不可知的基本约束传播机制，甚至可以提供解释的推理步骤，从约束的组合。在涉及多个约束的情况下，我们还开发了一种机制，允许打破最困难的步骤，从而使用户能够放大解释的特定部分。我们提出的算法迭代构造的解释序列，通过使用成本函数的乐观估计，以指导在每一步的最佳解释的搜索。我们的实验逻辑网格难题显示的质量的个人解释和解释序列获得的方法的可行性。
Proceedings 36th International Conference on Logic Programming (Technical Communications)
自1982年在马赛举行第一次会议以来，ICLP一直是展示逻辑编程研究的首要国际活动。在逻辑编程和相关领域的所有领域征求贡献，包括但不限于：-基础：语义学，形式主义，集合编程，非单调推理，知识表示。- 声明式编程：推理引擎，分析，类型和模式推理，部分求值，抽象解释，转换，验证，验证，建模，分析，测试，基于逻辑的领域特定语言，约束处理规则。- 相关范例和协同作用：归纳和协同归纳逻辑程序设计、约束逻辑程序设计、与SAT、SMT和CSP求解器的交互、用于类型推断和定理证明的逻辑编程技术、论证、概率逻辑程序设计、与面向对象和函数式编程的关系、描述逻辑、神经符号机器学习、混合深度学习和符号推理。- 实施情况：并发和分布，对象，协调，移动性，虚拟机，编译，高阶，类型系统，模块，约束处理规则，元编程，外部接口，用户界面。- 应用领域：数据库、大数据、数据集成和联合、软件工程、自然语言处理、Web和语义网、代理、人工智能、生物信息学、教育、计算生命科学、教育、网络安全和机器人技术。
扫码添加微信好友，提出您的宝贵建议 👇
💡 备注请填写：网站反馈
发表机构由 AI 从论文文本抽取，如发现错误，欢迎反馈修正建议。