Решаем задачу про ферзей при помощи SMT-солвера

SAT — Boolean SATisfiability Solver. Какое-то время назад я задался вопросом, почему: как получилось, что они настолько мощны, но ими никто не пользуется?  Я вспомнил об этом, когда прочитал пост Райана Бергера о решении «задачи ферзей с LinkedIn» как задачи SAT.Вкратце опишу задачу про ферзей (Queens). У нас есть сетка NxN, разделённая на N областей, и нам нужно разместить N ферзей так, чтобы в каждом столбце, строке и области находился ровно один. Ферзи могут находиться на одной диагонали, но не соседствовать по диагонали.