Questions tagged [proof-complexity]

propositional proof systems and corresponding bounded arithmetic theories

23 questions with no upvoted or accepted answers
Filter by
Sorted by
Tagged with
14 votes
0 answers
275 views

Any example of an unsatisfiable integer program with non constant Rank Lower bounds for LS+ cuts but with short LS+ refutations?

Assume we want to refute an unsatisfiable CNF. We can interpret it as an integer program, thus a refutation can be done by applying Lovasz-Schrijver semidefinite cuts ($LS_{+}$ cuts) to its linear ...
MassimoLauria's user avatar
9 votes
0 answers
416 views

Examples of simulations in proof complexity that are not p-simulations

I am writing a paper on the complexity of some unorthodox proof systems, where I have two systems $P$ and $Q$ such that $P$ simulates $Q$ in the sense of it being possible to translate a $Q$-proof ...
Emre Yolcu's user avatar
9 votes
0 answers
124 views

Reference for a propositional proof system being equivalent to its soundness?

I am looking for the original reference for the following statement: Let $P$ be a propositional proof system containing $EF$. Then $P$ is equivalent to $EF+Sound(P)$. Background A propositional ...
Kaveh's user avatar
  • 21.6k
7 votes
0 answers
102 views

Algorithmically determining proof complexity for Frege systems?

I apologize if this falls wildly short of research level - I am just learning the very basics of proof complexity and lack any real logic background. Let $F$ be a Frege proof system (a finite complete ...
Sprotte's user avatar
  • 171
7 votes
0 answers
206 views

Implications of the impossibility of efficient sampling from random non-Hamiltonian graphs

Nisan's answer to this question shows the Impossiblity of efficient sampling from random non-Hamiltonian graphs (unless $NP=coNP$). I am interested in the implications of this conjecture. Does the ...
Mohammad Al-Turkistany's user avatar
7 votes
0 answers
183 views

Oracle sparating FIP for bounded-depth Frege from FIP for Frege (and hardness conditions on DDH)

Is there an oracle such that in the relativized world, bd-Frege (bounded depth Frege propositional proof system) has FIP (feasible interpolation property) but Frege does not have FIP? Such an oracle ...
Kaveh's user avatar
  • 21.6k
4 votes
0 answers
56 views

Complexity of circuit evaluation in Resolution

Consider the standard evaluation function for CNF formulas $\mathsf{Eval}(\varphi,x)$ taking as input a CNF $\varphi$ and an assignment $x$ to the variables and outputting the value of $\varphi(x)$. ...
Noel Arteche's user avatar
4 votes
0 answers
250 views

Testing emptiness property complexity in Sum of Squares Proof systems

Take the set $$\mathcal T=\{f_1(x_1,\dots,x_n)=\dots=f_m(x_1,\dots,x_n)=0, h_1(x_1,\dots,x_n)\geq a_1,\dots,h_t(x_1,\dots,x_n)\geq a_t\}$$ where $$h_1(x_1,\dots,x_n),\dots,h_t(x_1,\dots,x_n)\in\mathbb ...
VS.'s user avatar
  • 539
3 votes
0 answers
75 views

How does extended resolution p-simulate extended Frege?

I found a slide stating that "extended resolution and extended Frege p-simulate each other", without providing a proof. It's obvious that extended Frege p-simulates extended resolution, but ...
Soha's user avatar
  • 187
3 votes
0 answers
129 views

Have the proofs in Buss's "On Goedel’s Theorems on Lengths of Proofs" been formalized (mechanically checked)?

The paper On Gödel's theorems on lengths of proofs I: Number of lines and speedup for arithmetics contains quite interesting results on proof length. But some of the details are still, to me, a bit ...
Jacques Carette's user avatar
3 votes
0 answers
65 views

Efficient transformation of clausal proof into resolution proof

Clausal proof is used to certify unsat results of SAT solvers. However the main theoretical results are on resolution proof (for instance, the non existence of a polynomial resolution proof for the ...
RTK's user avatar
  • 311
3 votes
0 answers
137 views

Transforming a DAG-like resolution proof to a tree like resolution proof

How can a DAG-like resolution proof be transformed to a tree-like resolution proof? Is such a transformation possible in polynomial time?
RTK's user avatar
  • 311
2 votes
0 answers
73 views

Proof systems that may be stronger than extended Frege?

The extended Frege proof system is thought to be a fairly strong proof system, with no known superpolynomial lower bounds. But I wonder, if extended Frege is proved not to be polynomially bounded one ...
Soha's user avatar
  • 187
2 votes
0 answers
122 views

Asymptotic complexity lower bounds of proof checking

This paper on universal search mentions (on pp. 6-7) that proof checking can be done in $O(n^2)$ where $n$ is the length of the proof. Is this optimal? I don't want to specify the problem too ...
Mario Carneiro's user avatar
2 votes
0 answers
119 views

Proof systems induced by NP-complete problems

Satisfiability is the fundamental NP-complete problem. Cook-Reckhow theorem states that the existence of a propositional proof system that admits polynomial size proofs for all tautologies implies ...
Mohammad Al-Turkistany's user avatar
2 votes
0 answers
122 views

Techniques for showing intermediate status between $\mathsf{NP \cap coNP}$ and coNP-completeness

Inspired by Suresh's post, for a new problem in $\mathsf{coNP}$, whose true proof complexity is intermediate between $\mathsf{NP \cap coNP}$ and being coNP-complete, I am interested in methods which ...
Mohammad Al-Turkistany's user avatar
1 vote
0 answers
62 views

Automatizability of Extended Resolution

According to Krajícek, Jan and Pavel Pudlák. “Some Consequences of Cryptographical Conjectures for S12 and EF.” Inf. Comput. 140 (1998): 82-94., the extended Frege proof system is not automatizable ...
Soha's user avatar
  • 187
1 vote
0 answers
75 views

Do soundness and completeness need to be exact converses of eachother?

This question concerns the derivational soundness and completeness of the first-order proof system LK (without equality) as presented in Logical Foundations of Proof Complexity by Cook and Nguyen. In ...
Johnny's user avatar
  • 201
1 vote
0 answers
155 views

Do problems have to be statable in $\Pi_1$ to use Levin's universal search to find short proofs if P=NP

In If P=NP, could we obtain proofs of Goldbach's Conjecture etc.? it talks about the hypothetical world where P=NP and using the proof of it to prove a problem/theorem assuming that it has a short ...
time's user avatar
  • 21
0 votes
0 answers
94 views

On the polynomial-size Frege proof of the propositional pigeonhole principle

I'm reading a lecture note on the proof of PHP, which mentioned that a "basic fact" $$ \left(\sum\limits_{i=1}^{s-1} A_i\ge a\right) \land A_s \to \sum\limits_{i=1}^s A_i\ge a $$ is ...
Soha's user avatar
  • 187
0 votes
0 answers
116 views

When the tree-like resolution size is the same with general(regular) resolution size?

Background: For an unsatisfiable SAT formulas, the length of a resolution refutaion means the number of clauses in it. It's well known that there exist exponential separation between tree-like and ...
Jxb's user avatar
  • 316
0 votes
0 answers
156 views

What's the connection between branchwidth and treewidth

I understand that treewidth and branchwidth are essentially equivalent for a fixed graph, given that $branchwidth(G) = Θ(treewidth(G))$. However, my question pertains to a specific case involving ...
Jxb's user avatar
  • 316
0 votes
0 answers
130 views

Boolean logic: What is the name of this trick to replace explicit negations by implications?

Consider a Boolean circuit $C$ composed of some finite set of input variables $A_1,\ldots, A_n$ and the connectives $\lor\land\neg\rightarrow$ (with $X\rightarrow Y=\neg X\lor Y$) (update: assume that ...
Duyal Yolcu's user avatar