布尔可满足性问题的算法与其在电路复杂性下界证明中的应用

The Boolean satisfiability problem examines whether there exists a truth assignment satisfied a given boolean expression (or circuit) . Because of its large correlation with other problems in computer science research, Boolean satisfying problem has always been the core problem of algorithm complexity. In the past 40 years, the research on the Boolean satisfiability problem has produced fruitful results. The main research directions include the proof of the running time and the design of the algorithm. This project starts with the algorithm design of satisfiability problem, and involves the design of random algorithm and deterministic algorithm and the analysis of time space complexity. And using Ryan Williams' recently proposed program to demonstrate the circuit complexity by designing an algorithm for SAT problems.

布尔可满足性问题考察的是对于一个给定的布尔表达式（或电路），是否存在一个对于所有变量的赋值，使得表达式取值为真。由于其与计算机科学研究中大量的关联性，布尔可满足性问题一直以来都是算法复杂性领域的核心问题。近40年来，围绕布尔可满足性问题的研究产生了丰硕的成果，其中主要的研究方向包括运行时间下限的证明和算法设计。本项目从可满足性问题的算法设计入手，涉及随机算法和确定性算法的设计和时间空间复杂性分析。并利用Ryan Williams最近提出的纲领，通过设计SAT问题的算法来证明电路复杂性下界。

布尔可满足性问题考察的是对于一个给定的布尔表达式(或电路)，是否存在一个对于所有变量的赋值，使得表达式取值为真。本项目主要从布尔可满足性问题出发，研究了布尔可满足性问题本身的求解算法，以及它在电路复杂性领域和计算复杂性领域中的各种应用。我们的研究内容和结果主要包括以下4个方面：.1. 布尔可满足性问题的求解算法改进。.2. 布尔可满足性问题在电路下界证明中的应用。.3. 针对布尔可满足性问题和其他NP完全问题的细粒度规约，以证明某些问题的指数时间或者多项式时间的算法求解下界，包括图染色，3-求和等等问题。.4. 针对与布尔可满足性问题非常类似的图染色问题，及其的线性空间推广的研究，包括算法设计和下界的证明。