Specify finite group satisfying two conditions Let $G = \left\{ 0, 1, 2, 3, 4, 5, 6, 7\right\}$ be a group with the operation $\circ$, which satisfies the following conditions:
\begin{align}
a \circ b \leq a + b \quad & \forall a,b \in G & (a) \\
a \circ a = 0 \quad & \forall a \in G & (b)
\end{align}
I have to create the operator table for this Group.
Since $a \circ a = 0$ for all $a \in G$, $0$ is the identity element and each element is self-inverse. Using this information, I get the operator table below. Each free space $\circ(a,b)$ must satisfy $0 < \circ(a,b) \leq a + b$ (because the inverse element is unique in a group and because of the above condition (a)). Also, associativity must be satisfied (since $(G,\circ)$ is a group).
\begin{array}[t]{l|ccccccc}
\circ & 0 & 1 & 2 & 3 & 4 & 5 & 6 & 7 \\
\hline
0 & 0 & 1 & 2 & 3 & 4 & 5 & 6 & 7 \\
1 & 1 & 0 &   &   &   &   &   &   \\
2 & 2 &   & 0 &   &   &   &   &   \\
3 & 3 &   &   & 0 &   &   &   &   \\
4 & 4 &   &   &   & 0 &   &   &   \\
5 & 5 &   &   &   &   & 0 &   &   \\
6 & 6 &   &   &   &   &   & 0 &   \\
7 & 7 &   &   &   &   &   &   & 0 \\
\end{array}
I wrote a minizinc (a CSP solver) program, which fills out the operation table. There is one unique solution (symmetric among both diagonals):
\begin{array}[t]{l|rr}
\circ & 0 & 1 & 2 & 3 & 4 & 5 & 6 & 7 \\
\hline
0 & 0 & 1 & 2 & 3 & 4 & 5 & 6 & 7 \\
1 & 1 & 0 & 3 & 2 & 5 & 4 & 7 & 6 \\
2 & 2 & 3 & 0 & 1 & 6 & 7 & 4 & 5 \\
3 & 3 & 2 & 1 & 0 & 7 & 6 & 5 & 4 \\
4 & 4 & 5 & 6 & 7 & 0 & 1 & 2 & 3 \\
5 & 5 & 4 & 7 & 6 & 1 & 0 & 3 & 2 \\
6 & 6 & 7 & 4 & 5 & 2 & 3 & 0 & 1 \\
7 & 7 & 6 & 5 & 4 & 3 & 2 & 1 & 0 \\
\end{array}
My question: Is there an elegant way of solving this problem rather than trying out all possible combinations? If yes, whats the mapping rule of $\circ?$
Thanks in advance for any help!
 A: There is a shorter way to solve the problem, although I wouldn't call it elegant.
But before that, the more important thing: there is also a very short way to describe how this operation $\circ$ that you found operates. To calculate $a \circ b$, you just write $a$ and $b$ in binary, then apply the bitwise XOR, and then convert the result back from binary to decimal.
For instance, look at this identity that I took from your operation table: $3 \circ 5 = 6$. Written in binary we have $3 = 011$ and $5 = 101$. Their bitwise XOR is $011 \oplus 101 = 110$, which is the binary notation for $6$. You can see for yourself that this rule describes your operation table completely.
Now, moving on to the computer-free solution. First of all, from the equality $0 \circ 0 = 0$ we see that $0$ must be the neutral element. Next, from the equality $x \circ x = 0$ for all $x$ it follows that $G$ is an elementary abelian 2-group, so it must be isomorphic to $\mathbb{Z}_2^3$. This also makes $G$ a vector space over the field $\mathbb{Z}_2$.
Now we just need to establish an isomorphism $f: G \to \mathbb{Z}_2^3$. Then we will have our multiplication rule as $x \circ y = f^{-1}(f(x) + f(y))$.
Choosing an isomorphism $f$ is essentially the same as choosing a basis in $G$. To choose a basis in $G$, we first note that $1 \circ 2 = 3$ (we know that $1 \circ 2 \leq 1 + 2$, and it cannot be $0$, $1$ or $2$). Then for our basis we can pick (say) $1$, $2$ and anything else other than $0$ and $3$. I choose to pick the basis $(1,2,4)$.
Now using the rule $x \circ y \leq x + y$ it's not hard to find all the linear combinations of the basis elements. Here they are:
$$
\begin{align*}
1 \circ 2 &= 3 \\
1 \circ 4 &= 5 \\
2 \circ 4 &= 6 \\
1 \circ 2 \circ 4 &= 7
\end{align*}
$$
Now we build the isomorphism $f$ by sending $1$ to $(0,0,1)$, $2$ to $(0,1,0)$, $4$ to $(1,0,0)$. Images of other elements are determined uniquely from linearity of $f$. Here they are:
$$
\begin{align*}
f(0) &= (0,0,0) \\
f(1) &= (0,0,1) \\
f(2) &= (0,1,0) \\
f(3) &= f(1 \circ 2) = f(1) + f(2) = (0,1,1) \\
f(4) &= (1,0,0) \\
f(5) &= f(1 \circ 4) = f(1) + f(4) = (1,0,1) \\
f(6) &= f(2 \circ 4) = f(2) + f(4) = (1,1,0) \\
f(7) &= f(1 \circ 2 \circ 4) = (1,1,1)
\end{align*}
$$
As you see, the image of each number turns out to be that number written in binary code. Now, if we recall that $f$ is an isomorphism, i.e. $f(x \circ y) = f(x) + f(y)$, we see that $\circ$ must operate exactly by XORing the binary codes of its operands.
