Минимальное покрытие предметов с помощью SAT-солвера

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

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

Для предметов используем индекс , для книг — индекс . Предикат «книга покрывает предмет » обозначаем .

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

Для решения задачи выберем книг в определенном порядке. Определим булевы переменные , обозначающие истинность высказывания «книга выбрана -й по порядку», . Всего переменных.

На переменные наложим ограничения:

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

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

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

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

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

для всех : хотя бы для одной книги , такой, что

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

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

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

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

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

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

Источник: habr.com