Архив рубрики ~Лента новостей~

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

Студенты пришли в библиотеку, чтобы подготовиться к экзаменам. Всего у них 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

✅ Найденные теги: Минимальное, новости
Читайте также
Архив рубрики ~Обо всем~ Мы профессионально отслеживаем выгодные предложения: вот лучшие предложения, которые нашли наши эксперты CNET на этой неделе. Архив рубрики ~Обо всем~ Как обучить модель оценки в эпоху искусственного интеллекта Архив рубрики ~Коротко из Telegram~ 🤖 Промышленным компаниям помогут внедрить ИИ На Архитектурном совете кластера… Архив рубрики ~Коротко из Telegram~ Шопоголикам выписали плацебо Любопытный тренд пришел из Южной Кореи. Там… Архив рубрики ~Коротко из Telegram~ Возвращаясь в мир без интернета Ozon Банк начал тестировать перевод… Архив рубрики ~Коротко из Telegram~ ♻️ Городские камеры подключат к борьбе с незаконными свалками NtechLab… Архив рубрики ~Коротко из Telegram~ Эксперты Data Insight выпустили новый рейтинг крупнейших интернет-магазинов России за… Архив рубрики ~Коротко из Telegram~ LLM delenda est или Язык до AGI не доведет Свежее… Архив рубрики ~Коротко из Telegram~ Обратил внимание, что ребята из Anthropic Institute (исследовательская лаба Антропиков)… Архив рубрики ~Коротко из Telegram~ Про Fable 5 еще. Сегодня уже была новость об этой… Архив рубрики ~Коротко из Telegram~ Pokémon Go помогал ловить покемонов, а теперь может помочь дронам… Архив рубрики ~Коротко из Telegram~ Учёные собрали полную карту нервной системы дрозофилы Исследователи полностью оцифровали… Архив рубрики ~Коротко из Telegram~ Apple Intelligence пересобрали с нуля Apple переводит Apple Intelligence на… Архив рубрики ~Коротко из Telegram~ Суд поставил ИИ-детекторы на место Суд признал незаконным отчисление студентки… Архив рубрики ~Обо всем~ Мы профессионально отслеживаем выгодные предложения: вот лучшие предложения, которые нашли наши эксперты CNET на этой неделе. Архив рубрики ~Обо всем~ Как обучить модель оценки в эпоху искусственного интеллекта Архив рубрики ~Коротко из Telegram~ 🤖 Промышленным компаниям помогут внедрить ИИ На Архитектурном совете кластера… Архив рубрики ~Коротко из Telegram~ Шопоголикам выписали плацебо Любопытный тренд пришел из Южной Кореи. Там… Архив рубрики ~Коротко из Telegram~ Возвращаясь в мир без интернета Ozon Банк начал тестировать перевод… Архив рубрики ~Коротко из Telegram~ ♻️ Городские камеры подключат к борьбе с незаконными свалками NtechLab… Архив рубрики ~Коротко из Telegram~ Эксперты Data Insight выпустили новый рейтинг крупнейших интернет-магазинов России за… Архив рубрики ~Коротко из Telegram~ LLM delenda est или Язык до AGI не доведет Свежее… Архив рубрики ~Коротко из Telegram~ Обратил внимание, что ребята из Anthropic Institute (исследовательская лаба Антропиков)… Архив рубрики ~Коротко из Telegram~ Про Fable 5 еще. Сегодня уже была новость об этой… Архив рубрики ~Коротко из Telegram~ Pokémon Go помогал ловить покемонов, а теперь может помочь дронам… Архив рубрики ~Коротко из Telegram~ Учёные собрали полную карту нервной системы дрозофилы Исследователи полностью оцифровали… Архив рубрики ~Коротко из Telegram~ Apple Intelligence пересобрали с нуля Apple переводит Apple Intelligence на… Архив рубрики ~Коротко из Telegram~ Суд поставил ИИ-детекторы на место Суд признал незаконным отчисление студентки…

Подписка на рассылку

Получайте свежие новости и идеи на почту. Без спама — только самое интересное.

Нажимая «Подписаться», вы соглашаетесь с политикой конфиденциальности.