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