Small graphs without power-of-two cycles: a lower bound of 24, a correction to a construction of Exoo, and explicit bounds for f(k)

The Erdos-Gyarfas conjecture states that every graph with minimum degree at least 3 contains a cycle whose length is a power of two. We prove by a SAT-based exhaustive search, certified by DRAT proofs, that every graph with minimum degree at least 3 on at most 23 vertices contains a cycle of length