Questions tagged [proof-complexity]
propositional proof systems and corresponding bounded arithmetic theories
82
questions
38
votes
2
answers
4k
views
Axioms necessary for theoretical computer science
This question is inspired by a similar question about applied mathematics on mathoverflow, and that nagging thought that important questions of TCS such as P vs. NP might be independent of ZFC (or ...
37
votes
2
answers
2k
views
If P=NP, could we obtain proofs of Goldbach's Conjecture etc.?
This is a naive question, out of my expertise; apologies in advance.
Goldbach's Conjecture and many other unsolved questions in mathematics can be written
as short formulas in predicate calculus.
For ...
30
votes
6
answers
1k
views
Well known classes of boolean formulas that require exponentially long resolution proofs
You might often find cutting plane methods, variable propagation, branch and bound, clause learning, intelligent backtracking or even handwoven human heuristics in SAT solvers. Yet for decades the ...
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 (...
25
votes
2
answers
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?
...
19
votes
3
answers
1k
views
What algorithms are known for computing Craig interpolants?
Is there any survey of algorithms for computing interpolants? What about papers on only one algorithm? The case I'm most interested in is $A=\lnot p\land q$ and $C=q$, plus the constraint that the ...
18
votes
3
answers
592
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 ...
18
votes
2
answers
519
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 ...
17
votes
2
answers
4k
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 ...
15
votes
3
answers
619
views
Theories which characterize classes of computational complexity
When reading the paper "An applicative theory for FPH" you can encounter the following passage:
Considering theories which characterize classes of computational complexity, there are three ...
15
votes
1
answer
473
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{...
14
votes
1
answer
708
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?
14
votes
1
answer
616
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-...
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 ...
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 ...
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 ...
13
votes
2
answers
558
views
Does coNP-complete problem have subexponential size certificate?
Assuming NP != coNP, then there is no polynomial size certificate for coNP-complete problem. But what about subexponential size certificate? Particularly for coSAT, is there subexponential size proof ...
12
votes
1
answer
687
views
Using Kolmogorov complexity to establish proof complexity lower bounds?
The motivation for this question is the fact that most n-bit strings are incompressible. Intuitively, we can propose by analogy that most proofs for Tautologies are incompressible to polynomial size. ...
11
votes
4
answers
671
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, ...
11
votes
1
answer
771
views
NP vs co-NP and second-order logic
Assume that NP=co-NP and polynomial $p(x)$ bounds the length of the proof of unsatisfiability for a 3-CNF instance $x$. Then are there any results on what form any proof of unsatisfiability for $x$ of ...
10
votes
3
answers
413
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 ...
10
votes
1
answer
484
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 ...
10
votes
1
answer
404
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)...
10
votes
1
answer
264
views
A direct sum theorem for Resolution clause space complexity?
Resolution is a scheme to prove unsatisfiability of CNFs. A proof in resolution is a logical deduction of the empty clause for the initial clauses in of the CNF. In particular any initial clause can ...
9
votes
2
answers
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 ...
9
votes
2
answers
308
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
1
answer
303
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 ...
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 ...
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 ...
8
votes
3
answers
591
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 ...
8
votes
2
answers
1k
views
PCP theorem and proof complexity?
It is known that if $P=NP$ then $CoNP= PCP[O(log(n)),O(1)]$. Also, it is known that $NEXP=PCP[poly(n),poly(n)]$. It appears that PCP can't tell us which natural problems are not in $NP$. I wonder if ...
8
votes
2
answers
436
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 ...
8
votes
1
answer
292
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 ...
7
votes
2
answers
350
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) =...
7
votes
1
answer
205
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 ...
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 ...
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 ...
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 ...
6
votes
1
answer
124
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 ...
6
votes
1
answer
227
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 ...
6
votes
1
answer
338
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 ...
5
votes
2
answers
239
views
Can CDCL Algorithm Derived Conflict Clauses Always Be Obtained Through Resolution from an Unsatisfiable CNF Formula?
I have a question regarding the Conflict-Driven Clause Learning (CDCL) algorithm applied to an unsatisfiable CNF formula $F$.
Specifically, can all the conflict clauses learned by the CDCL algorithm ...
5
votes
1
answer
292
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 ...
5
votes
1
answer
95
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 ...
4
votes
2
answers
552
views
Do we currently know a polynomial-size Frege proof for Tseitin formulas?
There's a vast literature about super-polynomial lower bounds on proof lengths of Tseitin formulas in bounded-depth Frege systems, but what I'm curious about is: what if we don't restrict the depth of ...
4
votes
1
answer
158
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 ...
4
votes
1
answer
210
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 $(...
4
votes
1
answer
205
views
A variation of propositional pigeonhole principle
Let $n$ be the number of pigeons, and $x_{i,j}$ denote the Boolean variable indicating that pigeon #$i$ is mapped to hole #$j$. Then the propositional pigeonhole principle (PHP) is the conjunction of ...
4
votes
1
answer
141
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 ...
4
votes
1
answer
104
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 ...