Ataque SAT al problema de álgebra de secundaria de Tarski
A SAT Attack on Tarski's High School Algebra Problem
El problema de álgebra de secundaria de Tarski pregunta si toda identidad verdadera sobre suma, multiplicación y exponenciación de enteros positivos se deduce de 11 identidades elementales. Wilkie mostró una identidad válida que no se deduce de los axiomas, y Gurevič construyó un contra-modelo de 59 elementos. Con SAT, demostramos que los contra-modelos más pequeños tienen tamaño 12, como conjeturaron Burris y Yeats, y que hay exactamente 8,957,952 contra-modelos en 12 elementos hasta isomorfismo. Nuestro enfoque supera a herramientas dedicadas y verificamos la corrección en Lean.
Usando SAT, demostramos que los contra-modelos más pequeños son de tamaño 12, como conjeturaron Burris y Yeats.