布尔可满足性算法和单调布尔函数的复杂性

Satisfiability of boolean formulas (SAT) is one of the most important NP-complete problems in both theory and practice. ..The first goal of this paper is to improve current algorithms for Satisfiability of boolean formulas (SAT). SAT is NP-complete and most likely no sub-exponential algorithms for SAT exist. Still, theoretical computer scientists have no reasonable conjecture about the optimal (exponential) running time for important subclasses of SAT, such as 3-SAT. Our goals include improving the analysis of state-of-the-art SAT algorithms (in particular the algorithm called PPSZ) via a more thorough analysis of correlated random variables. It is remarkable that we do not understand at all the worst-case running time of PPSZ, the currently fastest algorithm for k-SAT. This is a gap which this project attempts to close. This will include both better bower bounds (i.e., hard instances) and a tighter, potentially much more sophisticated analysis of the algorithm and can lead to a significantly improved running time. Also, we will investigate how prevalent design paradigms can be modified to obtain faster algorithms; furthermore, whether completely new paradigms can lead to better algorithms. ..The second goal is to study the complexity of monotone Boolean functions. Here, one focus will be on the average and maximum sensitivity of a function. These are two complexity measures that are important in decision tree complexity, circuit complexity, machine learning and many more. Our goal is making progress towards a conjecture by Rocco Servedio concerning the relationship between maximum and average sensitivity of monotone Boolean functions. The other focus will be monotone circuit complexity of monotone functions. While general circuit complexity is a notoriously hard research problem, several non-trivial lower bounds have been proved on the size of monotone circuits. Examples are exponential lower bounds on unbounded monotone circuits (initiated by Razborov in 1985) and superpolynomial lower bounds on constant-depth circuits (Ajtai and Gurevich, 1987). In this project we will investigate several new directions: (1) Inapproximaility of functions by monotone circuits; (2) improving superpolynomial lower boudns to exponential lower bounds; (3) considering wider classes of circuits, such as monotone circuits of logarithmic-depth (monotone NC1).

本项目的第一个目标是改善当前布尔公式可满足性（SAT）的算法。SAT是NP完全问题并且极有可能不存在解决SAT问题的亚指数时间算法。值得注意的是，我们完全不清楚PPSZ在最坏情况下的运行时间。PPSZ是目前最快的K-SAT算法。该项目试图扫除这一盲障。这将需要更好更紧的上下界（如困难实例）和更严谨且可能更复杂的算法分析，并可能能够显著提高运行时间。..第二个目标是研究单调布尔函数的复杂性。其中，一个研究重点是函数的平均灵敏度和最大灵敏度。另一个重点是单调函数的单调电路复杂性。例如，无界单调电路的指数下界（Razborov, 1985）和在恒定深度电路上的超多项式下界（Ajtai, Gurevich, 1987）。在这个项目中，我们将在一些新方向上进行研究：由单调电路导致的函数的不可近似性; 将超多项式下界提升为指数下界; 考虑其他类别的电路，如对数深度（单调NC1）的单调电路.

该项目专注于研究 NP 完全可满足性问题（SAT）的算法。 SAT 是逻辑上的决策问题，在理论和实践中都很重要。 然而，现在几乎没有能够快速解决 SAT 的方法; 因此，研究界有两种思路：(a) 并非寻找一种在任何情况下都表现良好的方法，而是找到具有实践意义的方法（启发式）；(b) 找到能显着改善平凡穷举搜索的方法，并研究哪些类别的 SAT 问题可以运用这些方法（中等指数算法）。..该项目侧重于 (b)。 属于理论研究（专注于数学证明，没有实验评估）。 我们在简化和改善现有技术水平上做出了重要贡献。