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

项目名称： 布尔可满足性算法和单调布尔函数的复杂性

项目编号： No.61502300

项目类型： 青年科学基金项目

立项/批准年度： 2016

项目学科： 自动化技术、计算机技术

项目作者： Dominik Scheder

作者单位： 上海交通大学

项目金额： 21万元

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

中文关键词： 布尔可满足性；指数级算法；布尔函数的分析；电路复杂性

英文摘要： 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).

英文关键词： Boolean Satisfiability;Exponential Algorithms;Analysis of Boolean Functions;Circuit Complexity