EPSRC Reference: 
EP/L024233/1 
Title: 
Parameterized Proof Complexity 
Principal Investigator: 
Beyersdorff, Dr O 
Other Investigators: 

Researcher CoInvestigators: 

Project Partners: 

Department: 
Sch of Computing 
Organisation: 
University of Leeds 
Scheme: 
First Grant  Revised 2009 
Starts: 
17 November 2014 
Ends: 
16 November 2016 
Value (£): 
100,013

EPSRC Research Topic Classifications: 
Fundamentals of Computing 


EPSRC Industrial Sector Classifications: 
No relevance to Underpinning Sectors 


Related Grants: 

Panel History: 
Panel Date  Panel Name  Outcome 
09 Apr 2014

EPSRC ICT Responsive Mode  Apr 2014

Announced


Summary on Grant Application Form 
Computational complexity studies the possibilities and limitations of efficient computation. Traditionally, a problem has been perceived as tractable if it admits a polynomialtime algorithm; and the class of all such problems forms the complexity class P. Conversely, a problem is hard if it is associated with a complexity class believed to be beyond the realm of tractability like NP. While the P vs NP question is one of the central questions of modern computer science and mathematics (as witnessed by its inclusion as one of the seven Millennium Prize Problems posed by the Clay Mathematics Institute in 2000), we seem to be far from a solution. However, literally thousands of problems of great practical significance from optimisation, artificial intelligence, computational biology, and many further fields are known to be NPcomplete. And they desperately need to be solved for practical instances.
Parameterized complexity is one of the main modern approaches that help to understand the precise border between tractability and intractability. While P vs NP colours the world of computational problems into black and white, parameterized complexity exploits additional structure of the problems and reveals a much more detailed picture. It results in algorithmic solutions for many NPhard problems using the new concept of fixed parameter tractability (FPT). This approach has revolutionised the way we approach intractable problems today; and many classically hard problems become solvable for large classes of relevant instances.
While parameterized complexity has been intensively studied during the last two decades, the concept of parameterization has been only recently transferred to proof complexity by Dantchev, Martin, and Szeider (FOCS 2007). Proof complexity studies the complexity of theorem proving: how difficult is it to construct a proof of a formal statement in a given proof system? What is the length of the shortest proof? These questions have tight relations to central problems in computational complexity and logic. Indeed, proof complexity offers one of the main approaches towards the P vs NP question via Cook's programme.
This project will be a substantial contribution towards the development of the field of parameterized proof complexity. While recent findings have already proved the effectiveness of the approach, much foundational work lies ahead. Similarly as parameterized complexity provides a fine classification of running times, parameterized proof complexity offers a more finegrained analysis of lengths of proofs. In particular, this results in FPTsize proofs for many formulas that require exponentialsize proofs in the classical setting. At the same time, showing lower bounds to the size of proofs becomes much harder: firstly, because there are less candidate formulas for hardness; and secondly, because many classical techniques turn out to be ineffective.
This project will develop new techniques and reassess current techniques in proof complexity and computational complexity for their applicability in parameterized proof complexity. These technical advances will be used to show strong lower bounds for parameterized proof systems where currently no nontrivial lower bounds are known. A particular system of interest is parameterized resolution with an efficient encoding of parameterized axioms.
In addition to its links to complexity and logic, proof complexity is the main theoretical tool to analyse the performance of modern SAT solvers. These are algorithms with very finetuned implementations that successfully solve the NPcomplete problem of boolean satisfiability (SAT) for large fractions of industrial instances stemming from applications as software verification or model checking. This project will develop new algorithmic approaches to SAT solving inspired by insights from parameterized proof complexity. One particular goal are parameterized algorithms that refine DPLLbased solvers.

Key Findings 
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk

Potential use in nonacademic contexts 
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk

Impacts 
Description 
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk 
Summary 

Date Materialised 


Sectors submitted by the Researcher 
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk

Project URL: 

Further Information: 

Organisation Website: 
http://www.leeds.ac.uk 