AI Решение задачи о покрытии с помощью SAT-солвера

[AI]

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

предметов. Каждая из

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

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


Для предметов используем индекс

, для книг - индекс

. Предикат "книга

покрывает предмет

" обозначаем

.

Поставим задачу ответить для заданного числа

на вопрос, можно ли, используя не более

книг, покрыть все предметы.

Для решения задачи выберем

книг в определенном порядке. Определим булевы переменные

, обозначающие истинность высказывания "книга

выбрана

-й по порядку",

. Всего

переменных.

На переменные

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

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

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

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

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

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

для всех

:

хотя бы для одной книги

, такой, что

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

Теперь, умея для каждого

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

.

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

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


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

формируется КНФ.

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