Finding and proving the exact ground state of a generalized Ising model by convex optimization and MAX-SAT