命题满足（SAT）是一个NP完整的问题，它影响了许多研究领域，例如计划，验证和安全性。主流现代SAT求解器基于冲突驱动的子句学习（CDCL）算法。最近的工作旨在通过图神经网络（GNNS）产生的预测来改善其可变分支启发式方法来增强CDCL SAT求解器。但是，到目前为止，这种方法要么尚未使解决方案更有效，要么需要在线访问大量的GPU资源。为了使GNN改进实用，本文提出了一种称为Neurocomb的方法，该方法以两个见解为基础：（1）重要变量和条款的预测可以与动态分支相结合，为更有效的混合分支策略，（2）它是（2）它是足以在SAT解决开始之前仅查询神经模型一次。 NeuroComb被实施，以增强称为Minisat的经典CDCL求解器，以及最新的CDCL求解器，称为葡萄糖。结果，它允许Minisat在最近的SATCOMP-2021竞争问题设置中解决11％和葡萄糖更多的问题，仅计算资源需求只有一个GPU。因此，NeuroComb是通过机器学习改善SAT解决的有效和实用方法。

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

We present the Neural Satisfiability Network (NSNet), a general neural framework that models satisfiability problems as probabilistic inference and meanwhile exhibits proper explainability. Inspired by the Belief Propagation (BP), NSNet uses a novel graph neural network (GNN) to parameterize BP in the latent space, where its hidden representations maintain the same probabilistic interpretation as BP. NSNet can be flexibly configured to solve both SAT and #SAT problems by applying different learning objectives. For SAT, instead of directly predicting a satisfying assignment, NSNet performs marginal inference among all satisfying solutions, which we empirically find is more feasible for neural networks to learn. With the estimated marginals, a satisfying assignment can be efficiently generated by rounding and executing a stochastic local search. For #SAT, NSNet performs approximate model counting by learning the Bethe approximation of the partition function. Our evaluations show that NSNet achieves competitive results in terms of inference accuracy and time efficiency on multiple SAT and #SAT datasets.

随着深度学习技术的快速发展，各种最近的工作试图应用图形神经网络（GNN）来解决诸如布尔满足（SAT）之类的NP硬问题，这表明了桥接机器学习与象征性差距的潜力。然而，GNN预测的解决方案的质量并未在文献中进行很好地研究。在本文中，我们研究了GNNS在学习中解决最大可满足性（MaxSAT）问题的能力，从理论和实践角度来看。我们构建了两种GNN模型来学习来自基准的MaxSAT实例的解决方案，并显示GNN通过实验评估解决MaxSAT问题的有吸引力。我们还基于算法对准理论，我们还提出了GNNS可以在一定程度上学会解决MaxSAT问题的影响的理论解释。

在本文中，我们提出了Satformer，这是一种基于新颖的变压器解决方案，可用于布尔（SAT）解决方案。与现有的基于学习的SAT求解器不同，在问题实例级别上学习的satformer学习了难以满足的问题实例的最低限度不满意的内核（MUC），这些实例为这些问题的因果关系提供了丰富的信息。具体而言，我们应用图形神经网络（GNN）以在连接正常格式（CNF）中获得条款的嵌入。层次变压器体系结构应用于子句嵌入以捕获条款之间的关系，并且当组成UNSAT核心的条款在一起时，自我发项权的权重被学到了很高，并将其设置为低。通过这样做，Satformer有效地了解了SAT预测条款之间的相关性。实验结果表明，Satformer比现有的基于端到端学习的SAT求解器更强大。

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

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

Generating diverse solutions to the Boolean Satisfiability Problem (SAT) is a hard computational problem with practical applications for testing and functional verification of software and hardware designs. We explore the way to generate such solutions using Denoising Diffusion coupled with a Graph Neural Network to implement the denoising function. We find that the obtained accuracy is similar to the currently best purely neural method and the produced SAT solutions are highly diverse, even if the system is trained with non-random solutions from a standard solver.

回溯搜索算法通常用于解决约束满足问题（CSP）。回溯搜索的效率在很大程度上取决于可变排序启发式。目前，最常用的启发式是根据专家知识进行手工制作的。在本文中，我们提出了一种基于深度的加强学习方法，可以自动发现新的变量订购启发式，更好地适用于给定类CSP实例。我们显示，直接优化搜索成本很难用于自动启动，并建议优化在搜索树中到达叶节点的预期成本。为了捕获变量和约束之间的复杂关系，我们设计基于图形神经网络的表示方案，可以处理具有不同大小和约束的CSP实例。随机CSP实例上的实验结果表明，学习的政策在最小化搜索树大小的方面优于古典手工制作的启发式，并且可以有效地推广到比训练中使用的实例。

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

Steiner树问题（STP）在图中旨在在连接给定的顶点集的图表中找到一个最小权重的树。它是一种经典的NP - 硬组合优化问题，具有许多现实世界应用（例如，VLSI芯片设计，运输网络规划和无线传感器网络）。为STP开发了许多精确和近似算法，但它们分别遭受高计算复杂性和弱案例解决方案保证。还开发了启发式算法。但是，它们中的每一个都需要应用域知识来设计，并且仅适用于特定方案。最近报道的观察结果，同一NP-COLLECLIAL问题的情况可能保持相同或相似的组合结构，但主要在其数据中不同，我们调查将机器学习技术应用于STP的可行性和益处。为此，我们基于新型图形神经网络和深增强学习设计了一种新型模型瓦坎。 Vulcan的核心是一种新颖的紧凑型图形嵌入，将高瞻度图形结构数据（即路径改变信息）转换为低维矢量表示。鉴于STP实例，Vulcan使用此嵌入来对其路径相关的信息进行编码，并基于双层Q网络（DDQN）将编码的图形发送到深度加强学习组件，以找到解决方案。除了STP之外，Vulcan还可以通过将解决方案（例如，SAT，MVC和X3C）来减少到STP来找到解决方案。我们使用现实世界和合成数据集进行广泛的实验，展示了vulcan的原型，并展示了它的功效和效率。

Partial MaxSAT (PMS) and Weighted PMS (WPMS) are two practical generalizations of the MaxSAT problem. In this paper, we propose a local search algorithm for these problems, called BandHS, which applies two multi-armed bandits to guide the search directions when escaping local optima. One bandit is combined with all the soft clauses to help the algorithm select to satisfy appropriate soft clauses, and the other bandit with all the literals in hard clauses to help the algorithm select appropriate literals to satisfy the hard clauses. These two bandits can improve the algorithm's search ability in both feasible and infeasible solution spaces. We further propose an initialization method for (W)PMS that prioritizes both unit and binary clauses when producing the initial solutions. Extensive experiments demonstrate the excellent performance and generalization capability of our proposed methods, that greatly boost the state-of-the-art local search algorithm, SATLike3.0, and the state-of-the-art SAT-based incomplete solver, NuWLS-c.

监督学习可以改善最先进的求解器的组合问题的设计，但是由于指数性最差的复杂性，标记大量组合实例通常是不切实际的。受图像的对比预训练的最新成功的启发，我们对增强设计对布尔满意度问题的对比预训练的影响进行了科学研究。虽然典型的图形对比前训练使用了标签 - 敏捷的增强，但我们的主要见解是，许多组合问题都有良好的态度，这允许设计具有标签的增强功能。我们发现，保留标签的增强对于对比度预训练的成功至关重要。我们表明，我们的表示形式能够达到与完全监督学习的可比测试准确性，而仅使用1％的标签。我们还证明，我们的表示形式更容易转移到看不见的域中的更大问题。我们的代码可在https://github.com/h4duan/contrastive-sat上找到。

我们解决了部分MaxSat（PMS）和加权PMS（WPM），这是MaxSat问题的两个实际概括，并为这些问题（称为BandMaxSat）提出了一种局部搜索算法，该算法应用了多臂Bantit模型来指导搜索方向。我们方法中的匪徒与输入（w）pms实例中的所有软子句相关联。每个手臂对应于软子句。 Bandit模型可以通过选择要在当前步骤中满足的软子句，即选择要拉的臂来帮助BandmaxSat选择一个良好的方向以逃脱本地Optima。我们进一步提出了一种初始化方法（w）PMS，在生产初始解决方案时优先考虑单元和二进制条款。广泛的实验表明，BandMaxSat显着优于最先进的（W）PMS本地搜索算法SATLIKE3.0。具体而言，BandMaxSat获得更好结果的实例数量大约是Satlike3.0获得的两倍。此外，我们将bandmaxsat与完整的求解器tt-open-wbo-inc相结合。最终的求解器bandmaxsat-c还胜过一些最好的最新完整（W）PMS求解器，包括satlike-c，loandra和tt-open-wbo-inc。

由于现实世界编程语言语法的复杂性，因此从原始源代码中的学习程序语义是具有挑战性的，并且由于难以重建长距离关系信息在程序中使用标识符暗示表示的长距离关系信息。在解决第一点时，我们将约束的Horn条款（CHC）视为程序验证问题的标准表示，提供了一种简单而编程的语言独立语法。对于第二个挑战，我们探索CHC的图表表示，并提出了一个新的关系超图神经网络（R-HYGNN）体系结构来学习程序功能。我们介绍了CHC的两个不同的图表。一个称为约束图（CG），并通过将符号及其关系分别翻译成键入节点和二进制边缘，并强调CHC的句法信息，并将其构造为抽象语法树的约束。第二个称为控制和数据流超图（CDHG），并通过表示通过三元超过的控制和数据流来强调CHC的语义信息。然后，我们提出了一种新的GNN体系结构R-HYGNN，扩展了关系图卷积网络，以处理超图。为了评估R-HYGNN从程序中提取语义信息的能力，我们使用R-HYGNN在两个图表上训练模型，以及使用CHC-COMP 2021的基准作为培训数据，在五个具有越来越多的代理任务上进行了越来越多的困难。最困难的代理任务要求该模型预测反例中的条款的出现，这是CHC的满意度。 CDHG在此任务中达到90.59％的精度。此外，R-HYGNN对由290多个条款组成的图表之一具有完美的预测。总体而言，我们的实验表明，R-HYGNN可以捕获复杂的程序功能，以实现指导验证问题。

Graph classification is an important area in both modern research and industry. Multiple applications, especially in chemistry and novel drug discovery, encourage rapid development of machine learning models in this area. To keep up with the pace of new research, proper experimental design, fair evaluation, and independent benchmarks are essential. Design of strong baselines is an indispensable element of such works. In this thesis, we explore multiple approaches to graph classification. We focus on Graph Neural Networks (GNNs), which emerged as a de facto standard deep learning technique for graph representation learning. Classical approaches, such as graph descriptors and molecular fingerprints, are also addressed. We design fair evaluation experimental protocol and choose proper datasets collection. This allows us to perform numerous experiments and rigorously analyze modern approaches. We arrive to many conclusions, which shed new light on performance and quality of novel algorithms. We investigate application of Jumping Knowledge GNN architecture to graph classification, which proves to be an efficient tool for improving base graph neural network architectures. Multiple improvements to baseline models are also proposed and experimentally verified, which constitutes an important contribution to the field of fair model comparison.

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.

为混合整数线性编程问题（MILLS）找到高质量解决方案对于许多实际应用非常重要。在这方面，提出了精炼启发式局部分支（LB）来生产改进解决方案，并且对MILP中的本地搜索方法的开发产生了高度影响力。该算法迭代地探索由所谓的本地分支约束定义的一系列解决方案邻域，即，限制与参考解决方案的距离的线性不等式。对于LB算法，邻域大小的选择对于性能至关重要。虽然它是由原始LB方案中的保守值初始化的，但我们的新观察是最佳规模强烈依赖于特定的MILP实例。在这项工作中，我们调查搜索附近的大小与底层LB算法的行为之间的关系，我们设计了一种基于倾斜的框架，用于引导LB启发式的邻居搜索。该框架由两阶段战略组成。对于第一阶段，训练缩放的回归模型以通过回归任务在第一迭代中预测LB邻域的大小。在第二阶段，我们利用加强学习和设计加强的邻域搜索策略，以动态调整随后的迭代处的大小。我们计算地表明，确实可以学习邻域大小，导致改进的性能，并且整个算法在实例大小相对于实例大小概括，并且显着地跨越实例概括。

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.

代表SAT实例的图表的视觉布局可以突出显示SAT实例的社区结构。SAT实例的社区结构与实例硬度和已知条款质量启发式方法有关。我们的工具SATVIZ使用可变交互图和强制定向的布局算法可视化CNF公式。借助SATVIZ，可以对条款证明进行动画，以连续突出最近学习子句的移动窗口中发生的变量。如果需要，Satviz还可以使用调整后的边缘权重创建可变交互图的新布局。在本文中，我们描述了Satviz的结构和特征集。我们还提出了一些使用Satviz创建的有趣的可视化。