Questions tagged [proof-complexity]
propositional proof systems and corresponding bounded arithmetic theories
76
questions
4
votes
1
answer
94
views
Power of non-implicationally-complete Frege systems and Boolean equational calculus
We know that Frege systems are required to be implicationally complete -- namely, if a set of formulas $B_1,B_2,\cdots,B_t$ imply formula $C$, then this implication can be proven in the system. I'm ...
- 103
4
votes
1
answer
76
views
Methods for Determining the minimal Width of Resolution Refutations for CNF Formulas
Recall that the width of a resolution refutation $R$ of a CNF formula $F$ is the maximal number of literals in any clause occurring in $R$. I am intersting in finding the minimal width of some certain ...
- 165
2
votes
0
answers
68
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 ...
- 103
1
vote
0
answers
50
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 ...
- 103
3
votes
0
answers
58
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 ...
- 103
0
votes
0
answers
92
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 ...
- 165
1
vote
0
answers
69
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 ...
- 201
1
vote
1
answer
72
views
Why isn't the proof obtained using Buss's proof of the derivational completeness of LK anchored?
The version of Buss's proof I'm referring to is the proof of Lemma II.2.24 in Logical Foundations of Proof Complexity by Cook and Nguyen. In the interest of keeping this question self-contained I've ...
- 201
0
votes
0
answers
147
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 ...
- 165
13
votes
2
answers
2k
views
Algebraic equivalent of SAT?
Starting with a simple observation. If $x,y\in\{0,1\}$, then the arithmetic product $x\cdot y$ corresponds to the logical conjunction if we interpret $1$ as true and $0$ as false.
But then, for a ...
- 1,558
4
votes
1
answer
133
views
Is there a relation between the techniques used by Dan Willard, versus those of Brown and Palsberg, to exclude diagonalization?
This question extends my inquiry from a previous post [0].
Dan Willard's Self-Justifying Axiom Systems/Self-Verifying Theories [1] and Brown and Palsberg's self-interpreter for F-Omega [2] both employ ...
- 81
0
votes
0
answers
128
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 ...
- 125
7
votes
0
answers
100
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 ...
- 171
3
votes
1
answer
204
views
Proof of SPFA's worst-case complexity?
I am trying to prove the worst-case asymptotic time complexity of the Shortest Path Faster Algorithm (SPFA). I know the complexity is the same as the "original" Bellman-Ford (BF) algorithm, ...
- 73
9
votes
0
answers
398
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 ...
- 191
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 ...
- 153
-4
votes
1
answer
207
views
Is mathematical proof itself NP-hard?
At the 8:00 mark of this video, he claims that proving things is itself an NP problem. I'm looking for more insight into this. Could someone help explain this concept to me and also provide a link to ...
- 119
2
votes
0
answers
117
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 ...
- 20.8k
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 ...
- 1,530
7
votes
1
answer
202
views
Document references describing weaknesses for cutting planes and algebraic proof system?
Here, Fortnow says (section 4.3):
Since then complexity theorists have shown similar weaknesses in a number of other proof systems including cutting planes, algebraic proof systems based on ...
4
votes
1
answer
159
views
Eliminating tautological axioms in tree-like $k$-DNF resolution
The propositional proof system $k$-DNF-resolution, a.k.a. $Res(k)$, is a generalization of propositional resolution, where the lines in a proof are $k$-DNF formulas, i.e., disjunctions of $k$-terms of ...
- 4,601
6
votes
1
answer
112
views
Axioms of Minimum Size Resolution Refutations
Let $\phi$ be an unsatisfiable CNF formula and let $\Pi$ be a resolution refutation of $\phi$ of minimum size. Let $\psi$ be the subformula of $\phi$ containing the clauses that actually appear as ...
- 243
4
votes
0
answers
249
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 ...
- 539
0
votes
1
answer
62
views
Understanding the definition of a "restriction of a resolution derivation"
I am reading the paper An Introduction to Lower Bounds on Resolution Proof Systems. In its subsection 2.3 the author gives an inductive definition of the restriction of a resolution refutation $\pi$.
...
- 311
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 ...
- 311
3
votes
0
answers
131
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?
- 311
5
votes
1
answer
93
views
Resolution augmented with the rule of symmetry or the rule of extension
Krishnamurthy (here is the abstract of his paper) showed that resolution augmented with the principle of symmetry forms a proof system (referred to as SR) in which certain formulas (which do not admit ...
- 311
6
votes
1
answer
220
views
Resolution vs Nondeterministic Search Problems
It is well known that each resolution refutation $\Pi$ for an unsatisfiable CNF formula $F = C_1\wedge C_2 \wedge ... \wedge C_m$ over variables $X$ can be translated in polynomial time (in the size ...
- 1,062
2
votes
2
answers
122
views
IPS upper bound for subset sum axiom
I am reading the following paper
Michael A. Forbes, Amir Shpilka, Iddo Tzameret, Avi Wigderson ,"Proof Complexity Lower Bounds from Algebraic Circuit Complexity", 2016.
IPS is defined as follows:
...
- 31
3
votes
2
answers
141
views
Construct proof systems for common algorithmic task, like equivalence of regular expressions
A propositional proof system according to Cook and Reckhow for a language $L \subseteq \Sigma^{\ast}$ is a deterministic polynomial time function $f : \Sigma^{\ast} \to L$ that is onto.
For $y \in L$ ...
- 2,017
1
vote
0
answers
146
views
Proof of Correctness of Bottleneck Dijkstra Algorithm [closed]
I am working on a bottleneck multicast tree for which I am using bottleneck Dijkstra algorithm.
My question is 1) bottleneck Dijkstra has the same correctness as that of (simple) Dijkstra or not ?
2)...
- 11
4
votes
1
answer
157
views
Is there any work relating type systems and Cook-Reckhow proof systems?
An important subfield of computational complexity is proof complexity, mostly due to Cook and Reckhow. E.g. one notable result is that a proof system that has efficient proofs (i.e., in length ...
- 175
0
votes
1
answer
279
views
In regards to the tautologies of a polynomially-bounded propositional proof system
In the book 'Logical Foundations of Proof Complexity', co-authored by Stephen Cook, the following definition is given:
A proof-system $F$ is said to be polynomially-bounded if there is a polynomial p(...
10
votes
1
answer
343
views
Lower Bounds for Frege and Extended Frege
Wikipedia [1] states that the best known lower bound for size of Frege proofs is quadratic, and that there is no known superlinear lower bounds for the number of lines of Frege proofs.
Questions:
1)...
- 1,062
-1
votes
1
answer
120
views
On the difference between propositional proof system and polynomially-bounded proof system
For the definition of a propositional proof system we have:
An abstract proof system is a polynomial time function f whose range is equal to the set of tautologies. If τ is a tautology, then an f-...
-4
votes
1
answer
308
views
NP-completeness of one generalized subset sum problem (target sum belongs to interval) [closed]
I need to prove that decision problem:
for a given set of positive integers $a_1, ..., a_n$, does it exist a subset that sums up to a value within interval $[\frac{1}{2}\sum a_i; \frac{1}{2}\sum a_i+...
- 95
7
votes
2
answers
347
views
Are there any propositional proof systems which are not Cook-Reckhow proof systems?
An abstract proof system is a polynomial time function $f$ whose
range is equal to the set of tautologies. If $\tau$ is a tautology, then an $f$-proof of $\tau$ is any value $\pi$ such that $f(\pi) =...
- 71
-3
votes
1
answer
82
views
On the (Cook) definition of a propositional proof system [closed]
Def: An abstract proof system is a polynomial time function f whose
range is equal to the set of tautologies. If T is a tautology, then an f-proof of T is any value w such that f(w)= T
I'm a bit ...
- 1
2
votes
0
answers
119
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 ...
- 20.8k
1
vote
0
answers
154
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 ...
- 21
10
votes
3
answers
402
views
Graph theoretic restriction to Proofs in Proof Complexity Theory
Proof complexity is a most basic area of computational complexity theory. An ultimate purpose of this area is to prove $NP\neq coNP$, that is, any prover cannot give a proof of unsatisfiability of ...
- 101
28
votes
6
answers
1k
views
Natural NP-complete problems with "large" witnesses
The question on cstheory "What is NP restricted to linear size witnesses?" asks about the class NP restricted to linear size $O(n)$ witnesses, but
Are there natural NP-complete problems in which (...
- 22.6k
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 ...
- 20.8k
9
votes
1
answer
301
views
Proof complexity and lower bounds
One way to prove NP$\neq$ coNP is to show that for every propositional proof system $f$ computable in polynomial time, there exists a family of tautologies for which $f$ requires super polynomial ...
- 93
13
votes
4
answers
1k
views
Start learning proof complexity
I recently started to read a lot about proof complexity and have been really enjoying what I have been reading. I would really like to learn more about this, but I am having difficulty finding some ...
- 371
11
votes
4
answers
653
views
An easy case of SAT that is not easy for tree resolution
Is there a natural class $C$ of CNF formulas - preferably one that has previously been studied in the literature - with the following properties:
$C$ is an easy case of SAT, like e.g. Horn or 2-CNF, ...
- 4,601
18
votes
3
answers
589
views
Constructively efficient algorithms without efficient correctness and efficiency proof
I am looking for natural examples of efficient algorithms (i.e. in polynomial time) s.t.
their correctness and efficiency can be proven constructively (e.g. in $PRA$ or $HA$), but
no proof using only ...
- 21.4k
8
votes
1
answer
282
views
How do I use canonical ordering to reduce symmetry in the SAT encoding of the pigeonhole problem?
In the paper "Efficient CNF Encoding for Selecting 1 from N Objects", the authors introduce their "commander variable" technique for encoding the constraint, and then talk about ...
10
votes
1
answer
476
views
Proofs in $S_{2}^{1}$
In a talk by Razborov, a curious little statement is posted.
If FACTORING is hard, then Fermat’s little theorem is not provable in $S_{2}^{1}$.
What is $S_{2}^{1}$ and why are current proofs not ...
- 12.7k
14
votes
1
answer
582
views
A 3-CNF formula that requires resolution width $5$
Recall that the width of a resolution refutation $R$ of a CNF formula $F$ is the maximal number of literals in any clause occurring in $R$. For every $w$, there are unsatisfiable formulas $F$ in 3-...
- 4,601