On Complexity Measures in Polynomial Calculus
Proof complexity is the study of different resources that a proof needs in different proof systems for propositional logic. This line of inquiry relates to the fundamental questions in theoretical computer science, as lower bounds on proof size for an arbitrary proof system would separate P from NP....
Main Author: | |
---|---|
Format: | Doctoral Thesis |
Language: | English |
Published: |
KTH, Teoretisk datalogi, TCS
2016
|
Online Access: | http://urn.kb.se/resolve?urn=urn:nbn:se:kth:diva-197278 http://nbn-resolving.de/urn:isbn:978-91-7729-226-5 |
id |
ndltd-UPSALLA1-oai-DiVA.org-kth-197278 |
---|---|
record_format |
oai_dc |
spelling |
ndltd-UPSALLA1-oai-DiVA.org-kth-1972782016-12-27T05:15:36ZOn Complexity Measures in Polynomial CalculusengMikša, MladenKTH, Teoretisk datalogi, TCSStockholm, Sweden2016Proof complexity is the study of different resources that a proof needs in different proof systems for propositional logic. This line of inquiry relates to the fundamental questions in theoretical computer science, as lower bounds on proof size for an arbitrary proof system would separate P from NP. We study two simple proof systems: resolution and polynomial calculus. In resolution we reason using clauses, while in polynomial calculus we use polynomials. We study three measures of complexity of proofs: size, space, and width/degree. Size is the number of clauses or monomials that appear in a resolution or polynomial calculus proof, respectively. Space is the maximum number of clauses/monomials we need to keep at each time step of the proof. Width/degree is the size of the largest clause/monomial in a proof. Width is a lower bound for space in resolution. The original proof of this claim used finite model theory. In this thesis we give a different, more direct proof of the space-width relation. We can ask whether a similar relation holds between space and degree in polynomial calculus. We make some progress on this front by showing that when a formula F requires resolution width w then the XORified version of F requires polynomial calculus space Ω(w). We also show that space lower bounds do not imply degree lower bounds in polynomial calculus. Width/degree and size are also related, as strong lower bounds for width/degree imply strong lower bounds for size. Currently, proving width lower bounds has a well-developed machinery behind it. However, the degree measure is much less well-understood. We provide a unified framework for almost all previous degree lower bounds. We also prove some new degree and size lower bounds. In addition, we explore the relation between theory and practice by running experiments on some current state-of-the-art SAT solvers. <p>QC 20161206</p>Understanding the Hardness of Theorem ProvingDoctoral thesis, comprehensive summaryinfo:eu-repo/semantics/doctoralThesistexthttp://urn.kb.se/resolve?urn=urn:nbn:se:kth:diva-197278urn:isbn:978-91-7729-226-5TRITA-CSC-A, 1653-5723 ; 2017:02application/pdfinfo:eu-repo/semantics/openAccessinfo:eu-repo/grantAgreement/EC/FP7/279611 |
collection |
NDLTD |
language |
English |
format |
Doctoral Thesis |
sources |
NDLTD |
description |
Proof complexity is the study of different resources that a proof needs in different proof systems for propositional logic. This line of inquiry relates to the fundamental questions in theoretical computer science, as lower bounds on proof size for an arbitrary proof system would separate P from NP. We study two simple proof systems: resolution and polynomial calculus. In resolution we reason using clauses, while in polynomial calculus we use polynomials. We study three measures of complexity of proofs: size, space, and width/degree. Size is the number of clauses or monomials that appear in a resolution or polynomial calculus proof, respectively. Space is the maximum number of clauses/monomials we need to keep at each time step of the proof. Width/degree is the size of the largest clause/monomial in a proof. Width is a lower bound for space in resolution. The original proof of this claim used finite model theory. In this thesis we give a different, more direct proof of the space-width relation. We can ask whether a similar relation holds between space and degree in polynomial calculus. We make some progress on this front by showing that when a formula F requires resolution width w then the XORified version of F requires polynomial calculus space Ω(w). We also show that space lower bounds do not imply degree lower bounds in polynomial calculus. Width/degree and size are also related, as strong lower bounds for width/degree imply strong lower bounds for size. Currently, proving width lower bounds has a well-developed machinery behind it. However, the degree measure is much less well-understood. We provide a unified framework for almost all previous degree lower bounds. We also prove some new degree and size lower bounds. In addition, we explore the relation between theory and practice by running experiments on some current state-of-the-art SAT solvers. === <p>QC 20161206</p> === Understanding the Hardness of Theorem Proving |
author |
Mikša, Mladen |
spellingShingle |
Mikša, Mladen On Complexity Measures in Polynomial Calculus |
author_facet |
Mikša, Mladen |
author_sort |
Mikša, Mladen |
title |
On Complexity Measures in Polynomial Calculus |
title_short |
On Complexity Measures in Polynomial Calculus |
title_full |
On Complexity Measures in Polynomial Calculus |
title_fullStr |
On Complexity Measures in Polynomial Calculus |
title_full_unstemmed |
On Complexity Measures in Polynomial Calculus |
title_sort |
on complexity measures in polynomial calculus |
publisher |
KTH, Teoretisk datalogi, TCS |
publishDate |
2016 |
url |
http://urn.kb.se/resolve?urn=urn:nbn:se:kth:diva-197278 http://nbn-resolving.de/urn:isbn:978-91-7729-226-5 |
work_keys_str_mv |
AT miksamladen oncomplexitymeasuresinpolynomialcalculus |
_version_ |
1718406225655234560 |