Студенты пришли в библиотеку, чтобы подготовиться к экзаменам. Всего у них 
предметов. Каждая из 
книг покрывает некоторое множество предметов. Нужно выбрать минимальное число книг, которые покроют все предметы.
Сведение к проблеме выполнимости КНФ
Для предметов используем индекс 
, для книг — индекс 
. Предикат «книга 
покрывает предмет 
» обозначаем 
.
Поставим задачу ответить для заданного числа 
на вопрос, можно ли, используя не более 
книг, покрыть все предметы.
Для решения задачи выберем 
книг в определенном порядке. Определим булевы переменные 
, обозначающие истинность высказывания «книга 
выбрана 
-й по порядку», 
. Всего 
переменных.
На переменные 
наложим ограничения:
Для каждой книги порядок может быть только один:
Запишем эти условия в виде КНФ:
2. Каждому порядку может соответствовать только одна книга:
Запишем эти условия в виде КНФ:
3. Каждый предмет покрывается хотя бы одной из выбранных книг:
для всех 
: 
хотя бы для одной книги 
, такой, что 
Запишем эти условия в виде КНФ:
Теперь, умея для каждого 
решать вопрос выполнимости КНФ, искомое минимальное покрытие находится бинарным поиском по 
.
Заметим, что условие 1 является необязательным.
Реализация с помощью SAT-солвера
Таким образом, имея на входе информацию о том, какие предметы какими книгами покрываются, для каждого значения 
формируется КНФ.
Полученную КНФ нетрудно ввести в любой SAT-солвер (например: онлайн, офлайн) в подходящем формате (например, DIMACS CNF).
Источник: habr.com
