in a sense it's about a game. or... maybe it's better to call it a "challenge"

Tarski said "hey, what if we limit ourself only to positive integers? subtraction/division doesn't always work, so let's get rid of it. What can we say about +^? there are some obvious properties, like x+y=y+x for whatever x and y. Is that enough to describe all the equalities?".

Wilkie answered No, and a whole different hunt began - trying to find a set of pseudo "numbers" with pseudo "+^", that would have the same obvious properties, but not the non-obvious one

and SAT-solving is essentially asking computer to find things by describing what they are not - "1+2 is not invalid and can't be 2 different values", "1+(1+1) must not differ from (1+1)+1". A lot of such properties are easily expressible as "not the opposite" - but devil's in the details and some choices of opposites are faster for computer than others. Also symmetries are evil :)