Skip to main content
27 votes
Accepted

What's the status of Babai's Graph isomorphism result?

Aggregating comments by Thomas Klimpel, Sasho Nikolov and Mohammad Al-Turkistany into a community answer: The correction (and hence the quasi-polynomial result) was immediately supported by Harald ...
20 votes
Accepted

Examples of algorithms and proofs that seem correct, but aren't

2D local maximum input: 2-dimensional $n \times n$ array $A$ output: a local maximum -- a pair $(i,j)$ such that $A[i,j]$ has no neighboring cell in the array that contains a strictly larger value. ...
Neal Young's user avatar
  • 10.8k
17 votes

Possible to do Complexity theory with only counting and Pigeonhole

If you are looking for non-pigeon-hole type arguments, then there is good news: they exist! The pigeon-hole principle is a certain template for proof by contradiction. There are concepts in TCS which ...
Lieuwe Vinkhuijzen's user avatar
14 votes

Proofs, Barriers and P vs NP

Contrary to some claims earlier in this thread, algebrization in the sense of Aaronson & Wigderson is not known to subsume relativization. For example, $$\tag{$\dagger$}(\exists \mathcal{C}: \...
Barış Aydınlıoğlu's user avatar
12 votes

Implications of unprovability of $P\neq NP$

As proved in the paper "On The Independence of P Versus NP" by S. Ben-David and S. Halevi: If $P \neq NP$ can be shown to be independent of Peano Arithmetic, then NP has extremely-close-to-...
Avi Tal's user avatar
  • 1,606
9 votes
Accepted

Proof that the graph optimization problem is NP-hard

This problem is in P, it can be reduced to the Minimum cut problem. The graph construction is as follows - Add a source and a sink vertex. For each vertex $i$, add an edge with cost $w(i)$ from ...
saisandeep's user avatar
9 votes
Accepted

Construction of arbitrary functions with exponential-size $MODp \circ MODq$ circuits

$\def\M#1{\mathrm{MOD}_{#1}}\def\F#1{\mathbb F_{#1}}$I don’t know of a reference, but here is one way how to prove the result. I’ll do it in three stages, each using one new idea: (1) multilinear ...
Emil Jeřábek's user avatar
7 votes
Accepted

Document references describing weaknesses for cutting planes and algebraic proof system?

For each of these proof systems we know that there are some formulas where the shortest proof needs to have exponential length. Some of the earliest examples are an exponential lower bound for the ...
notautogenerated's user avatar
6 votes

How to prove relations between "classes" of types?

One approach to such questions is via encodings. Say you have a language $L_1$ and a language $L_2$ and you want to show that they are somehow "the same", you can do this by finding an encoding $$ ...
Martin Berger's user avatar
6 votes
Accepted

Conversion between NP certificates

For general $L\in\mathrm{NP}$, this is equivalent to $\mathrm{FP=TFNP}$, hence likely false: On the one hand, if $V$ and $V'$ are verifiers of $L$, then “given $x$ and $u$ such that $V(x,u)$, find $u'$...
Emil Jeřábek's user avatar
5 votes

Examples of the value of proofs for algorithms

Here is a natural problem from graph theory where the proof and the algorithm are closely intertwined. In my view, one can discover this algorithm only via thinking about the proof and the algorithm "...
Andras Farago's user avatar
5 votes

Proof of Levenshtein distance

I looked into this last year while teaching. The other answers, including Prof. Erickson's excellent book, feel incomplete, because they handwave a step along the lines of "there is an optimal ...
usul's user avatar
  • 7,615
5 votes

Where is the quote "Informal proofs are algorithms, formal proofs are code" from?

He doesn't cite any references for it and Google doesn't return any results so I don't think he is really quoting from anywhere. The idea that a proof is a "construction" (a term in intuitionistic/...
Kaveh's user avatar
  • 21.7k
4 votes
Accepted

Complexity of counting the number of edge covers of a graph

After some more literature search, it appears that the complexity of counting the edge covers in a graph was shown to be #P-complete in bordewich2008path, Appendix A.1. (This assumes arbitrary graphs ...
a3nm's user avatar
  • 9,547
4 votes
Accepted

Uniqueness of the distribution maximizing the channel capacity

This conjecture is false. Here is a counterexample. Suppose we have a binary symmetric channel: $x_1 \rightarrow y_1$ with probability $1-\epsilon$ and $y_2$ with probability $\epsilon$, $x_2 \...
Peter Shor 's user avatar
3 votes
Accepted

How hard is this combinatorial optimisation problem?

This problem can be solved with dynamic programming in pseudo-polynomial time (proof below). Therefore, it is not possible to show that this problem is strongly NP-hard (unless P=NP). First, let's ...
Mikhail Rudoy's user avatar
3 votes

Formally proving no algorithm exists

What you are asking for is methods in proving lower bounds on the computational complexity (measured in space, time, etc) of given computational problems, and the answer is mostly that we have made ...
Samuel Schlesinger's user avatar
3 votes
Accepted

Formally proving no algorithm exists

See this lower bound for sorting, for example: http://planetmath.org/lowerboundforsorting You typically need to assume something about the algorithm's access to the input data. In this case, the ...
Aryeh's user avatar
  • 10.6k
3 votes

Proof of the pumping lemma for context-free languages using pushdown automata

When discussing this problem with Géraud Sénizergues, he pointed me this paper by Sakarovitch that already proves this result. The proof seems to date back to this paper by Ogden. References: ...
Lamine's user avatar
  • 1,137
3 votes

Sources that prove solving 2-SAT with DP takes linear time

It is a very basic exercise for undergraduate/graduate courses in Theoretical computer Science, and I think books avoid giving the solution so that students do not copy it without understanding. Here ...
J..y B..y's user avatar
  • 2,776
2 votes

Where and how did computers help prove a theorem?

A paper of mine with Gupta and Kumar titled On a bidirected relaxation for the MULTIWAY CUT problem was also based on running experiments. In fact we were trying to prove the converse of what we ended ...
2 votes

An Interactive Proof of God's Number?

Determining that $20$ is the diameter (God's number) of the Rubik's Cube Group $G$ under the half-turn metric with Singmaster generating set $s=\langle U, U', U^2, D, D', D^2,\cdots\rangle$ was a ...
Mark S's user avatar
  • 1,124
2 votes

Examples of the value of proofs for algorithms

I see several advantages of mastering the proof of correctness and complexity of an algorithm. I list them below and illustrate with a concrete example. I tried to stay in the domain of classical ...
holf's user avatar
  • 2,174
2 votes

Examples of the value of proofs for algorithms

A practical answer: In my career I encountered a few scenarios, some with my direct involvement, where I had to prove that my algorithm performs just as good as the currently best known possible. ...
Avi Tal's user avatar
  • 1,606
2 votes
Accepted

Formally prove that the loops of this sorting algorithm will terminate

Since the loop variables $i$ and $j$ are not modified in the loop body, you can compute the exact number of iterations. The inner loop is executed $n-i$ times in each iteration of the outer loop, so ...
Mark Dettinger's user avatar
2 votes
Accepted

Proving proof system properties within the proof system itself?

The first problem is what does is even mean that a propositional proof system can prove its own properties: there is a serious discrepancy of the languages, because the propositional proof system can ...
Emil Jeřábek's user avatar
2 votes

Proving proof system properties within the proof system itself?

There is no loop. The purpose of a formal system is to make reasoning principles explicit and to explain more precisely how reasoning works. The word "foundation" in "foundations of ...
Andrej Bauer's user avatar
  • 29.2k
2 votes
Accepted

Proving that a given formula in LTL is the smallest way to express it

I'm not sure whether it would work in your case, but in order to show succinctness results in modal/temporal logic (e.g. the fact the two-variable logic over words in exponentially more succinct than ...
Bartosz Bednarczyk's user avatar
2 votes

Establishing competing memory limits for pushdown automata

This answer is inspired by this question. The conjecture is false, for the following reason. Consider the alphabet $\Sigma=\{0,1\}$, and the language $A=\{0^n1(0|1)^n|n>0\}$. This language is ...
a3nm's user avatar
  • 9,547
2 votes

Halting problem proofs that do not utilise self-reference or diagonalization

P1 Perhaps you can somewhat avoid self reference in this way. Let $S_k$ be the total number of steps performed by the halting Turing machines of size $\leq k$ in their computation. Suppose the Halting ...
Marzio De Biasi's user avatar

Only top scored, non community-wiki answers of a minimum length are eligible