Arithmetization-Oriented (AO) cryptographic algorithms operate on large finite fields. The most threatening attack on such designs is the Gröbner basis attack, which solves the equation system encoded from the cryptanalysis problem. However, encoding a primitive as a system of equations is not unique, and finding the optimal one with low solving complexity is a formidable challenge. This paper presents an automated tool that transforms the problem into a Mixed-Integer Quadratic Constraint Programming (MIQCP) model. By employing integer variables and constraints, the tool tracks degree propagation and determines strategic variable introduction points. The optimal MIQCP solution yields the most efficient solving complexity, offering the lowest computational burden for the Gröbner basis attack. We construct comprehensive models for the Griffin, Anemoi, and Ciminion permutations. Our experiments demonstrate reduced Gröbner basis attack complexity, surpassing the designers’ bounds. This versatile tool can be leveraged to accurately evaluate the security of new AO designs against Gröbner basis attacks.