A SAT Attack on Tarski's High School Algebra Problem

30 pointsmatt_d4 days ago13 commentsView on HN

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.

stevefan19992 hours ago

I'm not sure, but maybe it is due to that the expression a - b can be replaced as a + (-b)?

Similarly, I think a * b and a / b can be replaced with the same trick, but then I realized it may not work on non-abelian, or where multiplicative inverse is not available...

Sharlin2 hours ago

We’re in the semiring of positive integers, so there are no additive (or multiplicative) inverses.

Sharlin2 hours ago

Subtraction is not closed over positive integers, which is untidy. The point of Tarski’s conjecture was to propose a minimal number of axioms and operations, AFAICS they define the standard semiring of positive integers (with the natural definition of exponentiation added).

(Edit: positive integers aren’t exactly a semiring because 0 is excluded, although some authors do define a semiring without the requirement of an additive identity element.)

munchler2 hours ago

Well, yes, but negative numbers are also well known to every high school math student.

Sharlin2 hours ago

Sure. But "High School Algebra (Excluding Subtraction) Problem" isn’t as catchy a name.

brookst2 hours ago

They subtracted the subtraction exclusion in the name of simplicity?

Transformanshen2 hours ago

The subtraction point is interesting but I don't think it makes the result disappointing. The whole point of Tarski's problem is what follows from that very restricted set of elementary identities so finding the exact minimum countermodel under those rules still seems like a pretty satisfying result.

woadwarrior012 hours ago

Because subtraction is not a total operation on positive integers. Negative numbers leave the domain.

NooneAtAll31 hour ago

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

yorwba1 hour ago

They use the properties of Wilkie's counterexample to restrict the search space. So you can't just pick arbitrary identities that hold over the positive integers and repeat the process until you've found a smaller model.

4063805811 hour ago

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

dooglius1 hour ago

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

LegionMammal97849 minutes ago

No, Gödel's incompleteness theorem applies to theories that can interpret first-order arithmetic, which includes quantified statements like "for all x, there exists a prime p > x".

In this case, we have the much simpler equational theory of positive integers under addition, multiplication, and exponentiation, which does not include any quantifiers. In fact, Gurevič showed that this theory is decidable [0]. On the other hand, Gurevič later showed that this theory is not finitely axiomatizable [1], so an infinite (but still computable) set of axioms is needed to fully characterize the theory.

[0] R. Gurevič, Equational theory of positive numbers with exponentiation, 1985, https://doi.org/10.2307/2044966

[1] R. Gurevič, Equational theory of positive numbers with exponentiation is not finitely axiomatizable, 1990, https://doi.org/10.1016/0168-0072(90)90049-8