One of the fundamental goals of theoretical computer science is tounderstand the possibilities and limits of efficient computation. Thisquest has two dimensions. Thetheory of algorithms focuses on finding efficient solutions toproblems, while computational complexity theory aims to understand whenand why problems are hard to solve. These two areas have differentphilosophies and use different sets of techniques. However, in recentyears there have been indications of deep and mysterious connectionsbetween them.In this project, we propose to explore and develop the connections betweenalgorithmic analysis and complexity lower bounds in a systematic way.On the one hand, we plan to use complexity lower bound techniques as inspirationto design new and improved algorithms for Satisfiability and otherNP-complete problems, as well as to analyze existing algorithms better.On the other hand, we plan to strengthen implications yielding circuitlower bounds from non-trivial algorithms for Satisfiability, and to derivenew circuit lower bounds using these stronger implications.This project has potential for massive impact in both the areas of algorithmsand computational complexity. Improved algorithms for Satisfiability could leadto improved SAT solvers, and the new analytical tools would lead to a betterunderstanding of existing heuristics. Complexity lower bound questions arefundamentalbut notoriously difficult, and new lower bounds would open the way tounconditionally secure cryptographic protocols and derandomization ofprobabilistic algorithms. More broadly, this project aims to initiate greaterdialogue between the two areas, with an exchange of ideas and techniqueswhich leads to accelerated progress in both, as well as a deeper understandingof the nature of efficient computation.