Powered by OpenAIRE graph
Found an issue? Give us feedback
image/svg+xml Jakob Voss, based on art designer at PLoS, modified by Wikipedia users Nina and Beao Closed Access logo, derived from PLoS Open Access logo. This version with transparent background. http://commons.wikimedia.org/wiki/File:Closed_Access_logo_transparent.svg Jakob Voss, based on art designer at PLoS, modified by Wikipedia users Nina and Beao Repository of the Cz...arrow_drop_down
image/svg+xml Jakob Voss, based on art designer at PLoS, modified by Wikipedia users Nina and Beao Closed Access logo, derived from PLoS Open Access logo. This version with transparent background. http://commons.wikimedia.org/wiki/File:Closed_Access_logo_transparent.svg Jakob Voss, based on art designer at PLoS, modified by Wikipedia users Nina and Beao
image/svg+xml Jakob Voss, based on art designer at PLoS, modified by Wikipedia users Nina and Beao Closed Access logo, derived from PLoS Open Access logo. This version with transparent background. http://commons.wikimedia.org/wiki/File:Closed_Access_logo_transparent.svg Jakob Voss, based on art designer at PLoS, modified by Wikipedia users Nina and Beao
DBLP
Article . 2023
Data sources: DBLP
DBLP
Article . 2022
Data sources: DBLP
versions View all 4 versions
addClaim

On Proof Complexity of Resolution over Polynomial Calculus

Authors: Erfan Khaniki;

On Proof Complexity of Resolution over Polynomial Calculus

Abstract

The proof system Res (PC d,R ) is a natural extension of the Resolution proof system that instead of disjunctions of literals operates with disjunctions of degree d multivariate polynomials over a ring R with Boolean variables. Proving super-polynomial lower bounds for the size of Res ( PC 1, R )-refutations of Conjunctive normal forms (CNFs) is one of the important problems in propositional proof complexity. The existence of such lower bounds is even open for Res ( PC 1,𝔽 ) when 𝔽 is a finite field, such as 𝔽 2 . In this article, we investigate Res ( PC d,R ) and tree-like Res ( PC d,R ) and prove size-width relations for them when R is a finite ring. As an application, we prove new lower bounds and reprove some known lower bounds for every finite field 𝔽 as follows: (1) We prove almost quadratic lower bounds for Res ( PC d ,𝔽)-refutations for every fixed d . The new lower bounds are for the following CNFs: (a) Mod q Tseitin formulas ( char (𝔽)≠ q ) and Flow formulas, (b) Random k -CNFs with linearly many clauses. (2) We also prove super-polynomial (more than n k for any fixed k ) and also exponential (2 nϵ for an ϵ > 0) lower bounds for tree-like Res ( PC d ,𝔽 )-refutations based on how big d is with respect to n for the following CNFs: (a) Mod q Tseitin formulas ( char (𝔽)≠ q ) and Flow formulas, (b) Random k -CNFs of suitable densities, (c) Pigeonhole principle and Counting mod q principle. The lower bounds for the dag-like systems are the first nontrivial lower bounds for these systems, including the case d =1. The lower bounds for the tree-like systems were known for the case d =1 (except for the Counting mod q principle, in which lower bounds for the case d > 1 were known too). Our lower bounds extend those results to the case where d > 1 and also give new proofs for the case d =1.

Country
Czech Republic
Related Organizations
Keywords

lower bounds, propositional pigeonhole principle, Polynomial Calculus, modular counting

  • BIP!
    Impact byBIP!
    selected citations
    These citations are derived from selected sources.
    This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).
    1
    popularity
    This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network.
    Average
    influence
    This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).
    Average
    impulse
    This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network.
    Average
Powered by OpenAIRE graph
Found an issue? Give us feedback
selected citations
These citations are derived from selected sources.
This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).
BIP!Citations provided by BIP!
popularity
This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network.
BIP!Popularity provided by BIP!
influence
This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).
BIP!Influence provided by BIP!
impulse
This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network.
BIP!Impulse provided by BIP!
1
Average
Average
Average
Upload OA version
Are you the author of this publication? Upload your Open Access version to Zenodo!
It’s fast and easy, just two clicks!