 Solution

Enumerate the vertices as $V=\{1,\dots ,n\}$ and introduce a Boolean variable $X_{u,v}$ for each ordered pair of vertices. Its intended meaning is that a proposed graph automorphism sends $u$ to $v$. Build four groups of Boolean clauses.

First require exactly one image for each vertex:Next require that distinct vertices have distinct images:Together $A$ and $B$ specify an injective function $f:V\to V$. Since $V$ is finite, this function is a bijection; a separate surjectivity condition is unnecessary.

Write $e(u,w)=1$ when $(u,w)\in E$ and $e(u,w)=0$ otherwise. Prohibit every pair of images that would change adjacency:Checking both possible mismatches preserves both edges and nonedges. Finally require a moved vertex:The desired propositional formula is

If a Boolean valuation satisfies ${\phi }_G$, $A$ selects a unique image for every vertex, $B$ makes the resulting function a bijection, $C$ preserves adjacency in both directions, and $D$ makes this graph automorphism different from the identity function. Conversely, given such a graph automorphism $f$, set $X_{u,v}$ true exactly when $v=f(u)$. Each of $A,B,C,D$ is then satisfied.

There are $n^2$ Boolean variables, $O(n^3)$ image and injectivity Boolean clauses, and at most $n^4$ adjacency Boolean clauses. With the graph stored by its adjacency matrix, testing a mismatch takes constant time. Thus the construction has polynomial time and output length $O(n^4\log (n+1))$ with binary-indexed variable names. For $n=0$, interpret the empty logical disjunction $D$ as false; for $n=1$, $A$ and $D$ conflict. These cases correctly have no nonidentity graph automorphism.