A SAT Attack on Tarski's High School Algebra Problem

Bernardo Subercaseaux, Benjamin Przybocki

Tarski's high school algebra problem asks whether every true identity concerning addition, multiplication, and exponentiation of positive integers follows from a list of 11 element…