Logic and computational complexity

点击翻译按钮获取中文摘要

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.