= Solution
Enumerate the <vertices> as $V=\{1,\ldots,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>:
$$
A=\bigwedge_{u\in V}\left[
\left(\bigvee_{v\in V}X_{u,v}\right)
\land\bigwedge_{v<w}(\neg X_{u,v}\lor\neg X_{u,w})\right].
$$
Next require that distinct <vertices> have distinct images:
$$
B=\bigwedge_{v\in V}\bigwedge_{u<w}(\neg X_{u,v}\lor\neg X_{w,v}).
$$
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:
$$
C=\bigwedge_{\substack{u,w,v,z\in V\\ e(u,w)\ne e(v,z)}}
(\neg X_{u,v}\lor\neg X_{w,z}).
$$
Checking both possible mismatches preserves both edges and nonedges. Finally require a moved <vertex>:
$$
D=\bigvee_{u\in V}\neg X_{u,u}.
$$
The desired <propositional formula> is
$$
\boxed{\varphi_G=A\land B\land C\land D.}
$$
If a <Boolean valuation> satisfies $\varphi_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>.
Back to article page
