Проблема обрізаної шахівниці — це складальна головоломка, запропонована філософом Максом Блеком у книзі Critical Thinking (1946). Пізніше цієї проблеми торкалися Соломон Голомб (1954), Гамов та Штерн, (1958) та Мартін Гарднер в його колонці «Математичні ігри» в Scientific American. Проблема формулюється таким чином:
Припустімо, зі стандартної (8x8) шахівниці видалили дві клітинки в діагонально протилежних кутах, і залишилось 62 клітинки. Чи можливо розмістити 31 доміно розміром 2x1 так, щоб покрити всі ці клітинки?
Більшість розмірковувань над цією проблемою надають рішення «в концептуальному сенсі» без доказів.[1] Джон МакКарті запропонував її[2] як складну проблему для автоматичних доказових систем.[3] Насправді рішення цієї проблеми з використанням резолютивної системи виходу надзвичайно важке.[4]
Головоломку неможливо закінчити. Доміно, покладене на шахівницю, завжди покриє одну білу і одну чорну клітинку. Отже, набір доміно, розташований на шахівниці, покриє однакову кількість клітинок кожного кольору. Якщо з шахівниці забрати дві білі клітинки, то залишиться 30 білих клітинок та 32 чорних клітинки, тому закрити всі клітинки, що залишились, неможливо. Якщо з шахівниці забрати дві білі клітинки, то залишиться 30 чорних клітинок та 32 білих клітинки, і ситуація та сама.[5]
Доказ тої самої неможливості показує, що не існує ніякого складання доміно, коли будь-які дві білі (або чорні) клітинки видалені з шахівниці. Однак, якщо видалені дві клітинки різних кольорів, то завжди можливо заповнити доміно клітинки, що залишились на шахівниці; цей наслідок називається теорема Гоморі,[6] на честь математика Ральфа Гоморі, чий доказ був опублікований в 1973 році.[7] Теорема Гоморі була доведена з використанням гамільтонового циклу графу-решітки, сформованого клітинками шахівниці; видалення двох клітинок різних кольорів розриває цей цикл на два шляхи з рівною кількістю клітинок кожен та які дуже легко поділити на доміно.
більшість рішень цієї проблеми в літературі вирішують її в концептуальному сенсі, однак не дають доказів теореми для обох оригінальних формулювань МакКарті.
Проблема, запропонована Джон МакКарті в лекції "Heavy duty set theory"1, була вирішена тут.
Теорему обрізаної шахівниці запропонував більш як 40 років тому Джон МакКарті як “міцний горішок” для автоматичного міркування.