DNA Non-Emptiness

Algorithm

The algorithm determines whether or not the language represented by the DNA is empty. If it isn't - the algorithm outputs a sample word from the language.
The implementation follows the algorithm described in this paper by King, Kupferman & Vardi.

General Idea

The algorithm works by searching for a cycle whose minimal edge is odd-numbered. It does this by a sort of binary search on the value of the minimal edge.
First, all edges with a smaller number than this value are removed, strongly connected components (SCC) are detected, and they are searched for an odd minimal edge.
If no such edge is found, the process is repeated recursively on two more or less disjoint aspects of the graph - once its condensation (where SCCs are treated as vertices) and once on the union of the SCCs themselves (after appropriate edges are removed in each case).
A more technical overview can be found on page 8 of the paper.

Source Code

Source code for this implementation can be found here.