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

Окт 1, 2025 0

Студенты пришли в библиотеку, чтобы подготовиться к экзаменам. Всего у них 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}toneg x_{b,j}text{ для любой пары } (i,j), text{ где } ineq j

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

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

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

x_{b_1,i}toneg x_{b_2,i}text{ для любой пары } (b_1,b_2), text{ где } b_1neq b_2

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

bigwedge_{i=1}^kbigwedge_{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).

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

✅ Найденные теги: Минимальное, новости

Похожие записи

Метки:
Каталог бесплатных опенсорс-решений, которые можно развернуть локально и забыть о подписках

Еще новости рубрики

fantasy
Архив рубрики ~Обо всем~

Фантазии

Июл 2, 2024
mirovozrenye
Архив рубрики ~Обо всем~

Мировоззрение

Июл 2, 2024
vydumshiky
Архив рубрики ~Обо всем~

Влияние выдумщиков и фантазеров на развитие…

Июл 2, 2024
vozmozhnosty
Архив рубрики ~Обо всем~

Нет ничего невозможного

Июл 2, 2024
присоединяйтесь в телеграмНовости Телеграм

Присоединяйтесь
к нам в

TELEGRAM

Рубрики

галерея

Фото сгенерированных лиц: исследование показывает, что люди не могут отличить настоящие лица от сгенерированных
Нейросети построили капитализм за трое суток: 100 агентов Claude заперли…
Скетч: цифровой осьминог и виртуальный мир внутри компьютера с человечком.
Сцена с жестами пальцами, где один жест символизирует "VPN", а другой "KHP".
‼️Paramount купила Warner Bros. Discovery — сумма сделки составила безумные…
Скриншот репозитория GitHub "Claude Scientific Skills" AI для научных исследований.
Структура эффективного запроса Claude с элементами задачи, контекста и референса.
Эскиз и готовая веб-страница платформы для AI-дизайна в современном темном режиме.
ideipro logotyp
Image Not Found

НОВОСТИ ДРУГИХ РУБРИК

Звёздное небо с галактиками и туманностями, космос, Вселенная, астрофотография.
Архив рубрики ~Лента новостей~

Система оповещения обсерватории Рубина отправила 800 000 сигналов в первую ночь наблюдений.

Астрономы будут получать оповещения о небесных явлениях в течение нескольких минут после их обнаружения. Теренс О'Брайен, редактор раздела «Выходные». Публикации этого автора будут добавляться в вашу ежедневную рассылку по электронной почте и в ленту новостей на главной…

ЧИТАТЬ
Мар 2, 2026
Женщина с длинными тёмными волосами в синем свете, нейтральный фон.
Архив рубрики ~Лента новостей~

Расследование в отношении 61-фунтовой машины, которая «пожирает» пластик и выплевывает кирпичи.

Обзор компактного пресса для мягкого пластика Clear Drop — и что будет дальше. Шон Холлистер, старший редактор Публикации этого автора будут добавляться в вашу ежедневную рассылку по электронной почте и в ленту новостей на главной странице вашего…

ЧИТАТЬ
Мар 2, 2026
Черный углеродное волокно с текстурой плетения, отражающий свет.
Архив рубрики ~Лента новостей~

Материал будущего: как работает «бессмертный» композит

Учёные из Университета штата Северная Каролина представили композит нового поколения, способный самостоятельно восстанавливаться после серьёзных повреждений.  Речь идёт о модифицированном армированном волокном полимере (FRP), который не просто сохраняет прочность при малом весе, но и способен «залечивать» внутренние…

ЧИТАТЬ
Мар 2, 2026
Круглый экран с изображением замка и горы, рядом электронная плата.
Архив рубрики ~Лента новостей~

Круглый дисплей Waveshare для креативных проектов

Круглый 7-дюймовый сенсорный дисплей от Waveshare создан для разработчиков и дизайнеров, которым нужен нестандартный экран.  Это IPS-панель с разрешением 1 080×1 080 пикселей, поддержкой 10-точечного ёмкостного сенсора, оптической склейкой и защитным закалённым стеклом, выполненная в круглом форм-факторе.…

ЧИТАТЬ
Мар 2, 2026

Впишите свой почтовый адрес и мы будем присылать вам на почту самые свежие новости в числе самых первых

ИдеиPRO