SAT-Angriff auf Tarskis Algebra-Problem: Kleinste Gegenmodelle haben Größe 12

A SAT Attack on Tarski's High School Algebra Problem

Tarskis Problem der Schulalgebra fragt, ob jede wahre Identität über Addition, Multiplikation und Exponentiation positiver ganzer Zahlen aus 11 elementaren Axiomen folgt. Wilkie zeigte, dass eine bestimmte Identität gültig ist, aber nicht aus den Axiomen folgt. Gurevič fand ein Gegenmodell mit 59 Elementen, später wurde es auf 12 reduziert. Mit SAT beweisen wir, dass die kleinsten Gegenmodelle genau 12 Elemente haben, und klassifizieren alle 8.957.952 solcher Modelle bis auf Isomorphie. Unser Ansatz übertrifft spezialisierte Tools wie Mace4 und SEM. Die Korrektheit des Hauptergebnisses wurde in Lean formal bewiesen.