Модели оптимизации для подмножественного покрытия

В недавнем номере информационного бюллетеня я жаловался на то, как исследователи вводят в заблуждение относительно применимости своей работы. Я привел SAT-решатели как пример. Люди предоставили интересные примеры в ответ, но то, что было новым для меня, - это понятие SMT (Сatisfiability Modulo Theories), расширение SAT. SMT кажется более практичным, чем обычный SAT (см. бюллетень за подробностями). Я хотел потратить некоторое время на изучение SMT-решателей и остановился на Z3, открытом исходном коде SMT-решателе от Microsoft.