Logic and computational complexity

我研究的主要目的是了解计算机程序在解决某些重要问题方面的局限性。这些问题需要满足一定数量的条件；假设有一组给定的条件，很容易检查所提出的解决方案实际上是否正确，但寻找解决方案似乎很困难。这类问题的一个日常例子是拼图游戏，如拼图游戏或解决魔方的问题。这类问题属于NP范畴。其中，最著名的是逻辑学中的可满足性问题，即命题逻辑的公式是否具有令人满意的赋值。

The principal aim of my research is to understand the limitations of computer programs in solving certain important types of problems. These problems are ones where there are a certain number of conditions to be satisfied; assuming a given collection of conditions, it is easy to check whether or not a proposed solution is in fact correct, but it appears to be difficult to search for a solution. An everyday example of this kind of problem is provided by puzzles, such as jigsaw puzzles, or the problem of solving Rubik's Cube. These type of problems are in the category NP. Of these, the best known is the Satisfiability problem from logic, which is the problem of whether a formula of propositional logic has a satisfying assignment. The main goal is to show that such problems, and in particular the Satisfiability problem, are hard to solve in general. In the case where a satisfiability problem has no solution, we can demonstrate this by providing a proof in a logical system. If we can show that in certain cases, where the problems are complicated, that the proofs of unsatisfiability must be exponentially long, then this shows that certain algorithms for the problem must take an exponentially long time in the worst case. This has already been shown for the best known and most successful algorithm for satisfiability, the resolution method. I hope in my research to extend these results to more powerful logical systems, and hence to broader classes of algorithms.