Студенты пришли в библиотеку, чтобы подготовиться к экзаменам. Всего у них M предметов. Каждая из N книг покрывает некоторое множество предметов. Нужно выбрать минимальное число книг, которые покроют все предметы.

Сведение к проблеме выполнимости КНФ

Для предметов используем индекс s=1..M, для книг - индекс b=1..N. Предикат "книга b покрывает предмет s" обозначаем g(b,s).

Поставим задачу ответить для заданного числа k=1..N на вопрос, можно ли, используя не более k книг, покрыть все предметы.

Для решения задачи выберем k книг в определенном порядке. Определим булевы переменные x_{b,i}, обозначающие истинность высказывания "книга b выбрана i-й по порядку", i=1..k. Всего Nk переменных.

На переменные x_{b,i} наложим ограничения:

  1. Для каждой книги порядок может быть только один:

x_{b,i}\to\neg x_{b,j}\text{ для любой пары } (i,j), \text{ где } i\neq j

Запишем эти условия в виде КНФ:

\bigwedge_{b=1}^N\bigwedge_{\substack{i,j=1..k\\i < j}} (\neg x_{b,i} \vee \neg x_{b,j})

2. Каждому порядку может соответствовать только одна книга:

x_{b_1,i}\to\neg x_{b_2,i}\text{ для любой пары } (b_1,b_2), \text{ где } b_1\neq b_2

Запишем эти условия в виде КНФ:

\bigwedge_{i=1}^k\bigwedge_{\substack{b_1,b_2=1..N\\b_1 < b_2}} (\neg x_{b_1,i} \vee \neg x_{b_2,i})

3. Каждый предмет покрывается хотя бы одной из выбранных книг:

для всех s : x_{b,1}\vee x_{b,2} \vee \ldots \vee x_{b,k} хотя бы для одной книги b, такой, что g(b,s)=1

Запишем эти условия в виде КНФ:

\bigwedge_{s=1}^M \bigvee_{\substack{b=1\\g(b,s)=1}}^N \bigvee_{i=1}^k x_{b,i}

Теперь, умея для каждого k решать вопрос выполнимости КНФ, искомое минимальное покрытие находится бинарным поиском по k.

Заметим, что условие 1 является необязательным.

Реализация с помощью SAT-солвера

Таким образом, имея на входе информацию о том, какие предметы какими книгами покрываются, для каждого значения k формируется КНФ.

Полученную КНФ нетрудно ввести в любой SAT-солвер (например: онлайн, офлайн) в подходящем формате (например, DIMACS CNF).