Multi-agent path finding (MAPF) is a task of finding non-conflicting paths connecting agents' specified initial and goal positions in a shared environment. We focus on compilation-based solvers in which the MAPF problem is expressed in a different well established formalism such as mixed-integer linear programming (MILP), Boolean satisfiability (SAT), or constraint programming (CP). As the target solvers for these formalisms act as black-boxes it is challenging to integrate MAPF specific heuristics in the MAPF compilation-based solvers. We show in this work how the build a MAPF encoding for the target SAT solver in which domain specific heuristic knowledge is reflected. The heuristic knowledge is transferred to the SAT solver by selecting candidate paths for each agent and by constructing the encoding only for these candidate paths instead of constructing the encoding for all possible paths for an agent. The conducted experiments show that heuristically guided compilation outperforms the vanilla variants of the SAT-based MAPF solver.

在多代理路径查找（MAPF）中，任务是从其初始位置找到多个代理的非冲突路径，以给定单个目标位置。 MAPF表示经常通过启发式搜索解决的古典人工智能问题。基于搜索的技术的重要替代方案是将MAPF编译为不同的形式主义，例如布尔满足性（SAT）。基于SAT的基于SAT的方法将SAT求解器视为外部工具，其任务是返回输入MAPF的布尔模型的所有决策变量的分配。我们在本短文中存在一种名为DPLL（MAPF）的新型编译方案，其中相对于MAPF规则的判定变量的部分分配的一致性检查直接集成到SAT求解器中。该方案允许在SAT求解器和一致性检查程序同时协同工作以创建布尔模型并搜索其令人满意的分配来进行更远的自动编译。

我们从理论和算法的观点正式化和研究多目标任务分配和路径发现（MG-TAPF）问题。MG-TAPF问题是要计算到代理的任务分配，每个任务都由一系列目标位置组成，并为代理的无碰撞路径组成，这些代理商访问其分配任务的所有目标位置。从理论上讲，我们证明MG-TAPF问题是最佳解决的NP问题。我们提出算法，这些算法基于用于多代理路径的算法技术，发现问题并最佳地解决MG-TAPF问题。我们通过实验将这些算法在各种不同的基准域上进行比较。

在多代理路径查找（MAPF）问题中，一组在图表上移动的代理必须达到其自身各自的目的地，而无需间间冲突。在实用的MAPF应用中，如自动仓库导航，偶尔有数百个或更多代理商，MAPF必须在终身基础上迭代地解决。这种情景排除了离线计算密集型最佳方法的简单调整;因此，可扩展的子最优算法用于此类设置。理想的可扩展算法适用于可预测计算时间的迭代方案和输出合理的解决方案。对于上述目的，在本研究中，提出了一种具有回溯（PIBT）的优先级继承的新型算法以迭代地解决MAPF。 PIBT依赖于适应性优先级方案，专注于多个代理的相邻运动;因此它可以应用于若干域。我们证明，无论其数量如何，当环境是图形时，所有代理都保证在有限的时间内达到目的地，使得所有相邻节点属于一个简单的周期（例如，双绞线）。实验结果涵盖了各种场景，包括真正的机器人演示，揭示了所提出的方法的好处。即使用数百种代理商，PIBT也会立即产生可接受的解决方案，可以解决其他事实上MAPF方法的大型情况。此外，PIBT在运行时和解决方案质量的自动化仓库中的传送包中的迭代方案上占据了现有方法。

审查多个机器人的无碰撞路径的目的对于现实世界多机器人系统很重要，并且已被研究为在图形上的优化问题，称为多代理路径查找（MAPF）。这篇评论调查了不同类别的经典和最先进的MAPF算法，并进行了不同的研究尝试，以应对将MAPF技术推广到现实世界情景的挑战。最新的发现解决MAPF问题是在计算上具有挑战性的。最近的进步导致了MAPF算法，该算法可以在运行时计算数百个机器人和数千个导航任务的无碰撞路径。 MAPF的许多变体已被正式化，以使MAPF技术适应不同的现实需求，例如机器人运动学的考虑，实时系统的在线优化以及任务分配和路径计划的集成。用于MAPF问题的摘要算法技术已经解决了多个多机器人应用程序的重要方面，包括自动仓库履行和分类，自动化火车调度以及非独立机器人和四轮驱动器的导航。这展示了它们在大型多机器人系统的现实应用中的潜力。

传统的多代理路径规划者通常在优化单个物镜的同时计算路径的集合，例如路径长度。然而，许多应用可能需要多个目标，例如在规划期间同时优化的燃料消耗和完井时间，并且这些标准可能无法容易地进行比较，有时彼此竞争。天真地应用现有的多目标搜索算法，例如多目标A *（MoA *），以多代理路径查找可能被证明是效率低，作为可能的解决方案的空间的大小，即帕累托最优集合，可以用代理的数量（搜索空间的维度）指数增长。本文介绍了一种名为基于多目标冲突的搜索（Mo-CBS）的方法，该方法通过利用基于冲突的搜索（CBS），是单目标多代理的公知算法来绕过这种所谓的维度诅咒路径发现，以及多目标优化文献的优势原则。我们还开发了MO-CBS的几种变体，以进一步提高其性能。我们证明了MO-CBS及其变体能够计算整个帕累托最优集合。数值结果表明，Mo-CBS优于MoA *以及妈妈*，最近开发的最先进的多目标多功能策划员。

基于冲突的搜索（CBS）是一种广泛使用的算法，用于最佳地求解多代理探路（MAPF）问题。 CBS的核心思想是运行层次搜索，当在高级别的解决方案树上探索候选者的树时，在低级别上进行了针对特定代理的个人计划（受某些约束）进行。为了使运行时间的权衡取得最佳性，设计了有限的子最佳CB的不同变体，这改变了CBS的高级和低级搜索程序。此外，CBS的任何时间变体都存在将焦点搜索（FS）应用于CBS的高级搜索 - 任何时间BCB。然而，当我们简单地重新启动cbs的cbs与较低的亚XB绑定时，没有对这种算法的性能的全面分析。这项工作旨在填补这一空白。此外，我们介绍并评估了另一个在CBS上使用FS的CBS的随时随地。从经验上讲，我们证明其行为主要与任何时间BCB所证明的行为不同。最后，我们比较这两种算法从头开始，并表明在两个级别的CBS上使用焦点搜索在广泛的设置中可能是有益的。

组合优化是运营研究和计算机科学领域的一个公认领域。直到最近，它的方法一直集中在孤立地解决问题实例，而忽略了它们通常源于实践中的相关数据分布。但是，近年来，人们对使用机器学习，尤其是图形神经网络（GNN）的兴趣激增，作为组合任务的关键构件，直接作为求解器或通过增强确切的求解器。GNN的电感偏差有效地编码了组合和关系输入，因为它们对排列和对输入稀疏性的意识的不变性。本文介绍了对这个新兴领域的最新主要进步的概念回顾，旨在优化和机器学习研究人员。

本文收集了提交给核心挑战2022的求解器和ISR实例的所有描述。

命题模型计数或#SAT是计算布尔公式满足分配数量的问题。来自不同应用领域的许多问题，包括许多离散的概率推理问题，可以将#SAT求解器解决的模型计数问题转化为模型计数问题。但是，确切的#sat求解器通常无法扩展到工业规模实例。在本文中，我们提出了Neuro＃，这是一种学习分支启发式方法，以提高特定问题家族中的实例的精确#sat求解器的性能。我们通过实验表明，我们的方法减少了类似分布的持有实例的步骤，并将其推广到同一问题家族的更大实例。它能够在具有截然不同的结构的许多不同问题家族上实现这些结果。除了步骤计数的改进外，Neuro＃还可以在某些问题家族的较大实例上在较大的实例上实现壁式锁定速度的订单，尽管开头查询了模型。

We present an approach for the verification of feed-forward neural networks in which all nodes have a piece-wise linear activation function. Such networks are often used in deep learning and have been shown to be hard to verify for modern satisfiability modulo theory (SMT) and integer linear programming (ILP) solvers.The starting point of our approach is the addition of a global linear approximation of the overall network behavior to the verification problem that helps with SMT-like reasoning over the network behavior. We present a specialized verification algorithm that employs this approximation in a search process in which it infers additional node phases for the non-linear nodes in the network from partial node phase assignments, similar to unit propagation in classical SAT solving. We also show how to infer additional conflict clauses and safe node fixtures from the results of the analysis steps performed during the search. The resulting approach is evaluated on collision avoidance and handwritten digit recognition case studies.

多试路径查找（MAPF）是人工智能中的一个活跃领域，它具有许多真实的应用程序，例如仓库管理，交通控制，机器人技术等。最近，M*及其变体大大提高了解决该问题的能力MAPF问题。尽管在这些方法中使用的优异扩展显着降低了关节搜索空间的维度并降低了分支因子，但它们并不能充分利用每个代理的最佳路径的可能性非唯一性。结果，碰撞集的更新可能会带来大量冗余计算。在本文中，旁路的想法被引入细分扩展中，以减少冗余计算。具体而言，我们提出了BPM*算法，该算法是M*中旁路的细分扩展的实现。在实验中，我们表明BPM*在解决几个MAPF基准问题方面胜过最先进的问题。

在这项工作中，我们考虑了多代理拾取和交付（MAPD）问题，在该问题中，代理商不断参与新任务，并需要计划无碰撞的路径以执行它们。要执行任务，代理需要访问由接送位置和交货位置组成的两对目标位置。我们提出了两种算法的变体，该变体使用Anytime Algorithm大型邻域搜索（LNS）为每个代理分配一系列任务，并使用多代理路径查找（MAPF）基于算法优先级搜索（PBS）计划路径。 LNS-PBS已完善，用于良好的MAPD实例，MAPD实例的现实子类，并且比现有完整的MAPD算法中央更有效。 LNS-WPBS没有提供完整的保证，但在经验上比LNS-PBS更高效和稳定。它扩展到大型仓库中数千名代理商和数千个任务，并且在经验上比现有的可伸缩MAPD算法HBH+MLA*更有效。 LNS-PBS和LNS-WPB也适用于MAPD的更一般变体，即多目标MAPD（MG-MAPD）问题，其中任务可以具有不同数量的目标位置。

域特异性启发式方法是有效解决组合问题的必不可少的技术。当前将特定于域的启发式方法与答案集编程（ASP）集成的方法在处理基于部分分配的非单调指定的启发式方法时，这是不令人满意的。例如，在挑选尚未放入垃圾箱中的物品时，这种启发式方法经常发生。因此，我们介绍了ASP中域特异性启发式方法声明性规范的新颖语法和语义。我们的方法支持启发式陈述，依赖于解决过程中所维持的部分任务，这是不可能的。我们在Alpha中提供了一种实现，该实现使Alpha成为第一个支持声明指定的域特定启发式方法的懒惰的ASP系统。使用两个实际的示例域来证明我们的提议的好处。此外，我们使用我们的方法用A*实施知情}，该搜索首次在ASP中解决。 A*应用于两个进一步的搜索问题。实验证实，结合懒惰的ASP解决方案和我们的新型启发式方法对于解决工业大小的问题至关重要。

\ textit {约束路径发现}的经典问题是一个经过充分研究但充满挑战的主题，在各个领域，例如沟通和运输等各个领域的应用。权重限制了最短路径问题（WCSPP），作为仅具有一个侧面约束的约束路径查找的基本形式，旨在计划成本最佳路径，其权重/资源使用受到限制。鉴于问题的双标准性质（即处理路径的成本和权重），解决WCSPP的方法具有一些带有双目标搜索的共同属性。本文在约束路径查找和双目标搜索中利用了最新的基于A*的最新技术，并为WCSPP提供了两种精确的解决方案方法，两者都可以在非常大的图表上解决硬性问题实例。我们从经验上评估了算法在新的大型和现实的问题实例上的性能，并在时空指标中显示出它们比最新算法的优势。本文还调查了优先级队列在被a*的约束搜索中的重要性。我们通过对逼真的和随机图进行了广泛的实验来展示，基于桶的队列没有打破打盘的方式可以有效地改善详尽的双标准搜索的算法性能。

本文介绍了经典懒惰的概率路线图算法（Lazy PRM）的修订，该算法是由配对PRM和一种新颖的分支和切割（BC）算法产生的。切割是动态生成的约束，这些约束在PRM选择的几何图上施加的最低成本路径。削减消除无法映射到满足适当定义运动学约束的平滑计划中的路径。我们通过在最低成本路径中将花键拟合到顶点来生成候选平滑计划。使用最近提出的算法对计划进行了验证，该算法将它们映射到有限的痕迹中，而无需选择固定的离散步骤。痕量元素准确地描述了计划交叉约束边界何时模拟算术精度。我们使用我们最近提出的谷仓基准的方法评估了几个计划者，我们报告了方法可扩展性的证据。

回答集编程（ASP）已成为一种流行的和相当复杂的声明问题解决方法。这是由于其具有吸引力的地址解决方案的工作流程，这是可以轻松解决问题解决的方法，即使对于计算机科学外的守护者而言。与此不同，底层技术的高度复杂性使得ASP专家越来越难以将想法付诸实践。有关解决此问题，本教程旨在使用户能够构建自己的基于ASP的系统。更确切地说，我们展示了ASP系统Clingo如何用于扩展ASP和实现定制的专用系统。为此，我们提出了两个替代方案。我们从传统的AI技术开始，并展示元编程如何用于扩展ASP。这是一种相当轻的方法，依赖于Clingo的reation特征来使用ASP本身表达新功能。与此不同，本教程的主要部分使用传统的编程（在Python中）来通过其应用程序编程接口操纵Clingo。这种方法允许改变和控制ASP的整个模型 - 地面解决工作流程。 COMENT of Clingo的新应用程序课程使我们能够通过自定义类似于Clingo中的进程来绘制Clingo的基础架构。例如，我们可能会互动到程序的抽象语法树，控制各种形式的多射击求解，并为外国推论设置理论传播者。另一种横截面结构，跨越元以及应用程序编程是Clingo的中间格式，即指定底层接地器和求解器之间的界面。我们通过示例和几个非琐碎的案例研究说明了本教程的前述概念和技术。

MD4 and MD5 are seminal cryptographic hash functions proposed in early 1990s. MD4 consists of 48 steps and produces a 128-bit hash given a message of arbitrary finite size. MD5 is a more secure 64-step extension of MD4. Both MD4 and MD5 are vulnerable to practical collision attacks, yet it is still not realistic to invert them, i.e. to find a message given a hash. In 2007, the 39-step version of MD4 was inverted via reducing to SAT and applying a CDCL solver along with the so-called Dobbertin's constraints. As for MD5, in 2012 its 28-step version was inverted via a CDCL solver for one specified hash without adding any additional constraints. In this study, Cube-and-Conquer (a combination of CDCL and lookahead) is applied to invert step-reduced versions of MD4 and MD5. For this purpose, two algorithms are proposed. The first one generates inversion problems for MD4 by gradually modifying the Dobbertin's constraints. The second algorithm tries the cubing phase of Cube-and-Conquer with different cutoff thresholds to find the one with minimal runtime estimation of the conquer phase. This algorithm operates in two modes: (i) estimating the hardness of an arbitrary given formula; (ii) incomplete SAT-solving of a given satisfiable formula. While the first algorithm is focused on inverting step-reduced MD4, the second one is not area-specific and so is applicable to a variety of classes of hard SAT instances. In this study, for the first time in history, 40-, 41-, 42-, and 43-step MD4 are inverted via the first algorithm and the estimating mode of the second algorithm. 28-step MD5 is inverted for four hashes via the incomplete SAT-solving mode of the second algorithm. For three hashes out of them this is done for the first time.

我们提出了一个通用图形神经网络体系结构，可以作为任何约束满意度问题（CSP）作为末端2端搜索启发式训练。我们的体系结构可以通过政策梯度下降进行无监督的培训，以纯粹的数据驱动方式为任何CSP生成问题的特定启发式方法。该方法基于CSP的新型图表，既是通用又紧凑的，并且使我们能够使用一个GNN处理所有可能的CSP实例，而不管有限的Arity，关系或域大小。与以前的基于RL的方法不同，我们在全局搜索动作空间上运行，并允许我们的GNN在随机搜索的每个步骤中修改任何数量的变量。这使我们的方法能够正确利用GNN的固有并行性。我们进行了彻底的经验评估，从随机数据（包括图形着色，Maxcut，3-SAT和Max-K-Sat）中学习启发式和重要的CSP。我们的方法表现优于先验的神经组合优化的方法。它可以在测试实例上与常规搜索启发式竞争，甚至可以改善几个数量级，结构上比训练中看到的数量级更为复杂。

冲突驱动的子句学习（CDCL）是解决命题逻辑令人满意问题的非常成功的范式。这种求解器不是简单的深度优先回溯方法，而是以其他条款的形式了解了发生冲突的原因。但是，尽管CDCL求解器取得了巨大的成功，但仍然对以什么方式影响这些求解器的性能有限。考虑到不同的措施，本文非常令人惊讶地证明，从句学习（不摆脱某些条款）不仅可以帮助求解器，而且可能会大大恶化解决方案过程。通过进行广泛的经验分析，我们进一步发现，CDCL求解器的运行时分布是多模式的。这种多模式可以看作是上面描述的恶化现象的原因。同时，这也表明了为什么从条款删除结合条款学习的原因实际上是SAT解决的事实标准，尽管存在这种现象。作为最终贡献，我们表明Weibull混合物分布可以准确描述多模式分布。因此，在基本实例中添加新的子句具有长期运行时间的固有效果。该洞察力提供了一个解释，即为什么忘记条款的技术在CDCL求解器中有用，除了单位传播速度的优化。