Scale-Free Satisfiability

布尔逻辑是描述来自物流和优化等各个领域的工业决策问题的标准语言。解决这些问题对应于为给定公式的布尔变量找到令人满意的赋值。对于具有数百万个变量的实例，工业求解器可以非常高效地发现这一点。这种实用效率与理论计算机科学最经典的结果形成了鲜明对比：证明命题可满足性(SAT)的计算难度。这些结果之间的差异是由于最坏情况下的公式与实际应用中出现的公式之间的明显结构差异。为了解决这个问题，在过去的二十年里，人们对随机公式的平均情况行为进行了广泛的研究。这项研究的大部分假设变量都是随机出现的。然而，从均匀分布中提取的公式也具有与工业SAT实例集非常不同的统计结构。例如，工业公式经常在变量出现时表现出很大的波动。因此，生成更接近真实世界实例的合成实例是“SAT研究中的重大挑战”之一。这个项目将研究非均匀和无标度分布，它们似乎更接近于工业SAT实例。我们想要确定哪些统计特性使现实世界的SAT实例比目前理论所能解释的要容易得多。我们将根据可用于分析大规模无标度网络的概率工具，开发必要的数学机制。更好地理解关键参数将导致工业应用中更有效和更有原则的SAT解算器。

Boolean logic is the standard language to describe industrial decision problems coming from various domains like logistics and optimization. Solving these problems corresponds to finding a satisfying assignment to the Boolean variables of a given formula. This can be found very efficiently with industrial solvers for instances with millions of variables.This practical efficiency stands in contrast to the most classical result of theoretical computer science: the proven computational hardness of propositional satisfiability (SAT). The disparity between these results is due to the stark structural differences between worst-case formulas and those that appear in practical applications. To address this, the average-case behavior over random formulas was extensively studied in the last two decades. Most of this research assumes that variables appear uniformly at random. However, formulas drawn from a uniform distribution also have very different statistical structure than sets of industrial SAT instances. For example, industrial formulas often exhibit large fluctuations in variable occurrence.Thus it is one of the "grand challenges in SAT research" to generate synthetic instances that are more similar to real-world instances. This project will study non-uniform and scale-free distributions, which appear to resemble industrial SAT instances more closely. We want to determine which statistical properties make real-world SAT instances much easier to solve than theory can explain so far. We will develop the necessary mathematical machinery based on the probabilistic tools available for the analysis of large scale-free networks. A better understanding of the critical parameters will lead the way to more efficient and principled SAT solvers on industrial applications.