Horn formulas are an important fragment of propositional logic, with various applications including knowledge representation and reasoning. We define and study the hydra number of a graph, a graph property that arises from a combinatorial reformulation of a restricted version of the NP-hard problem of Horn formula minimization. This talk is based on joint work with Robert H. Sloan and Gyorgy Turan.