Questions tagged [proof-complexity]

propositional proof systems and corresponding bounded arithmetic theories

Filter by
Sorted by
Tagged with
2
votes
0answers
99 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 ...
2
votes
0answers
90 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 ...
7
votes
1answer
180 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
0answers
96 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 ...
6
votes
1answer
93 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 ...
4
votes
0answers
190 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 ...
0
votes
1answer
57 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$. ...
2
votes
0answers
54 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 ...
2
votes
0answers
99 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?
4
votes
1answer
77 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 ...
3
votes
0answers
82 views

Primal/Dual of the Lasserre/ SOS SDP hierarchy

Sum of Squares proofs and the Lasserre hierarchy can both be stated as SDPs. It is often claimed without proof that these SDPs are dual to each other, although I do not see that this is obvious. I was ...
6
votes
1answer
199 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 ...
2
votes
2answers
101 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: ...
3
votes
2answers
133 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$ ...
1
vote
0answers
114 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)...
4
votes
0answers
66 views

Combinatorial characterization of hypergraph Tseitin satisfiability

The Tseitin formulas are as follows: Given a connected graph and a function $\alpha: V \rightarrow \{0,1\}$. Associate each edge $e$ with a variable $x_e$. The Tseitin formula $G(\alpha)$ is defined ...
4
votes
1answer
136 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 ...
0
votes
1answer
190 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(...
9
votes
1answer
246 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
votes
1answer
101 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
1answer
226 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+...
6
votes
2answers
327 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) =...
-3
votes
1answer
80 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
vote
0answers
102 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 ...
1
vote
0answers
132 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 ...
10
votes
3answers
353 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 ...
28
votes
6answers
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 (...
7
votes
0answers
203 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 ...
8
votes
1answer
262 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 ...
12
votes
4answers
976 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 ...
10
votes
4answers
543 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, ...
17
votes
3answers
526 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 ...
8
votes
1answer
230 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 the pigeonhole problem....
10
votes
1answer
402 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 ...
13
votes
1answer
480 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-...
15
votes
2answers
2k views

Is propositional resolution a complete proof system?

This question is about propositional logic and all occurrences of "resolution" should be read as "propositional resolution". This question is something extremely basic but it has been bothering me ...
23
votes
2answers
2k views

Sum-of-squares proof system

Recently I have seen several articles on arxiv that refer to a proof system called sum-of-squares. Can someone explain what is a sum-of-squares proof and why such proofs are important/interesting? ...
4
votes
1answer
152 views

Consequences of a $p$-optimal proof system for $\operatorname{TAUT}$

I'm reading a paper which shows the result: $(1)$ There is a $p$-optimal proof system for $\operatorname{TAUT}$. $\Leftrightarrow$ $(2)$ $L_{\leq}$ is a $P$-bounded logic for $P$. Both $(1)$ and $(...
9
votes
2answers
275 views

Intuition behind proof systems

I'm trying to under stand the paper On p-Optimal Proof Systems and Logic for PTIME. There is a notion called proof systems in the paper and I do not get the intution: $\Sigma = \{0,1\}$ ... We ...
9
votes
0answers
112 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 ...
15
votes
1answer
443 views

How efficient are DPLL-based SAT-solvers on satisfiable instances of PHP?

We know that DPLL based SAT-solvers fail to answer correctly on unsatisfiable instances of $\mathrm{PHP}$ (pigeon hole principle), e.g. on "there is a injective mapping from $n+1$ to $n$": $$\mathrm{...
7
votes
2answers
1k views

Automated theorem proving via unsupervised approaches

This question Where and how did computers help prove a theorem? considers some automated theorem proving successes. However they seem to be mostly supervised approaches, such as with the 4 color graph ...
0
votes
1answer
346 views

Proof Complexity and Circuit Lower bound for coNP

I have two questions (1)Circuit lower bound for coNP TAUT is a set of formulae such that any formula in TAUT is satisfied for all boolean assignments. UnSAT is the complement problem of SAT. It is ...
5
votes
1answer
226 views

Resolution vs Extended Resolution

Let $R(f)$ and $ER(f)$ be the minimum-size for unsat proofs of $f$ in Resolution and Extended Resolution respectively. What's the best bound we have on $D=\min_f (R(f)-ER(f))$ where $f$ belongs to a ...
8
votes
3answers
537 views

Graph problems with good characterization but not known to be in $P$

A decision problem has good characterization if it is in $NP \cap coNP$. Many natural graph problems have good characterizations. For instance, Kuratuwski's Theorem gives good characterization of ...
14
votes
1answer
605 views

Consequences of sub-exponential proofs/algorithms for SAT

Would there be any major consequences if SAT had at most subexponential unsat proofs or even more strongly, SAT had subexponential-time algorithms?
18
votes
2answers
462 views

Uses of XORification

XORification is the technique to make a Boolean function or formula harder by replacing every variable $x$ by the XOR of $k\geq 2$ distinct variables $x_1 \oplus \ldots \oplus x_k$. I am aware of ...
6
votes
1answer
316 views

Best lower bound for proof complexity of graph non-automorphism problem

Graph automorphism problem ( GA) of determining whether a graph has a nontrivial automorphism is a good candidate for a problem in NP-intermediate. I'm looking for references that study the ...
8
votes
2answers
409 views

Postselection in geometric complexity theory

Context: As I understand, in geometric complexity theory, the existence of obstructions serves as a proof-certificate, so to speak, for the nonexistence of an efficient computational circuit for the ...
7
votes
0answers
182 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 ...