A SAT Attack on Tarski's High School Algebra Problem

I love SAT solver papers, always interesting to see auxiliary variable techniques, since those aren't really listed anywhere central

here for example, instead of saying {f(x,y,z)==g(x,y,z)}, authors instead make variable group a_w:=(f(x,y,z)=w||g(x,y,z)=w), and then apply "at most 1" to it. Can't be unequal if both functions only can have 1 result in total

this adds an index to iterate over, but separates internal subexpressions of f() and g(), removing 2 indixes (in this problem) and thus dropping whole power of n of clauses

---

what I don't get is that they aren't searching Tarski's problem per se, but for one specific solution to it (one identity that isn't resulting from given). I'd totally look for arithmetic models that violate expectations in other ways than Wilkie

Isn't the underlying question proved impossible by Godel's incompletness theorem?

Why is subtraction not part of the algebra? It’s certainly familiar to every high school math student. This omission allows the counterexample, so the reveal is a bit of a disappointment IMHO.

The lower bound had already been established in prior work: https://zenodo.org/records/18568303