Non-constructive algorithm existence proofs

The vast majority of positive results about computational problems are constructive proofs, i.e., a computational problem is proved to be solvable by showing an algorithm that solves it; a computational problem is shown to be in P by showing an algorithm that solves it in time that is polynomial in the size of the input; etc.

A simple example of a non-constructive algorithm was published in 1982 by Elwyn R. Berlekamp, John H. Conway, and Richard K. Guy, in their book Winning Ways for Your Mathematical Plays.

There exists an algorithm (given in the book as a flow chart) for determining whether a given first move is winning or losing: if it is a prime number greater than three, or one of a finite set of 3-smooth numbers, then it is a winning first move, and otherwise it is losing.

However, there is a non-constructive proof that shows that linkedness is decidable in polynomial time.

The proof relies on the following facts: Given an input graph G, the following "algorithm" solves the above problem: The non-constructive part here is the Robertson–Seymour theorem.

[1] The main idea is that a problem can be solved using an algorithm that uses, as a parameter, an unknown set.

The response to the query is just the dot product of the query vector by v. Every set of k queries can be represented by a k-by-n matrix over {0,1}; the set of responses is the product of the matrix by v. A matrix M is "good" if it enables us to uniquely identify v. This means that, for every vector v, the product M v is unique.