A SAT Attack on Tarski's High School Algebra Problem
Tarski's High School Algebra Problem, a classic question in universal algebra, asks if all true identities follow from 11 axioms; the answer, it turns out, is a complicated 'no'. This paper uses a sophisticated SAT attack to computationally determine the smallest countermodels, resolving a long-standing conjecture. It's a compelling example of how advanced computational methods are pushing the boundaries of pure mathematical discovery, a popular theme on Hacker News.
The Lowdown
This paper presents a computational resolution to a core question in universal algebra, Tarski's High School Algebra Problem. The problem, posed by Alfred Tarski, asks whether every true identity involving addition, multiplication, and exponentiation of positive integers can be derived from a set of 11 elementary identities. While seemingly straightforward, the question hides deep mathematical subtleties.
- Wilkie disproved Tarski's conjecture by presenting a specific complex identity that holds true for positive integers but cannot be deduced from Tarski's original 11 axioms, thereby showing the answer to Tarski's problem is 'no'.
- Subsequent research focused on finding the smallest 'countermodel' – an algebraic structure that satisfies Tarski's axioms but not Wilkie's identity. Gurevič initially found a 59-element countermodel, which was progressively reduced, culminating in a 12-element countermodel by Burris and Yeats.
- Zhang proved that no countermodel could exist with fewer than 11 elements, leaving the question of the absolute minimum size open between 11 and 12.
- The authors of this paper leveraged Satisfiability Modulo Theories (SAT) solvers to definitively prove that the smallest countermodels are indeed of size 12, confirming the conjecture by Burris and Yeats.
- Beyond just confirming the size, their SAT approach identified exactly 8,957,952 distinct 12-element countermodels (up to isomorphism) and provided a simple classification system for them.
- The paper highlights that their SAT-based methodology significantly outperformed dedicated tools like Mace4 and SEM in this specific problem. Furthermore, the correctness of their primary finding was formally verified using autoformalization within the Lean proof assistant.
This work brilliantly demonstrates the power of modern computational logic, specifically SAT solvers and formal verification, in providing conclusive answers to complex problems in abstract algebra, pushing the boundaries of what's discoverable through automated reasoning.