MathOverflow will be down for maintenance for approximately 3 hours, starting Monday evening (06/24/2013) at approximately 9:00 PM Eastern time (UTC-4).

The Robertson–Seymour theorem implies that every minor-closed family $F$ of finite graphs is decidable in time $O(n^3)$. However, it does not provide an explicit algorithm until one supplies an explicit finite list of forbidden minors that characterize $F$; the proof that such a list always exists is non-constructive.