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

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

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

29.09.2025 21:57

lapkin25 7 597 Источник

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

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

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

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

Для решения задачи выберем книг в определенном порядке. Определим булевы переменные $x_{b,i}$ , обозначающие истинность высказывания "книга выбрана -й по порядку", . Всего переменных.

На переменные $x_{b,i}$ наложим ограничения:

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

$x_{b,i}\to\neg x_{b,j}\text{ для любой пары } (i,j), \text{ где } i\neq j$

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

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

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

$x_{b_1,i}\to\neg x_{b_2,i}\text{ для любой пары } (b_1,b_2), \text{ где } b_1\neq b_2$

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

$\bigwedge_{i=1}^k\bigwedge_{\substack{b_1,b_2=1..N\\b_1 < b_2}} (\neg x_{b_1,i} \vee \neg x_{b_2,i})$

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

для всех : $x_{b,1}\vee x_{b,2} \vee \ldots \vee x_{b,k}$ хотя бы для одной книги , такой, что

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

$\bigwedge_{s=1}^M \bigvee_{\substack{b=1\\g(b,s)=1}}^N \bigvee_{i=1}^k x_{b,i}$

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

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

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

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

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

Комментарии (7)

mosinnik
30.09.2025 00:14
#28898322
В разговорах про решения с помощью SAT как обычно тут не хватает самой главной части - как из вон той формулы получить КНФ, скормить ее солверам и по результату уже дать ответ для каких-то заданных вводных. В общем show me the code, хотя бы на том же питоне, хотя бы на SMT, как это было в статье про крестики-нолики, и чтобы запустил тест и оно все отработало и наглядно.

qw1
30.09.2025 00:14
#28899452
Это какой-то жёсткий брут-форс.
Для размера задачи 20 книг и 10 предметов, выходит 200 переменных.
Не будет ли оптимальнее взять 20 переменных по кол-ву книг xi=0/1 (книга i взята/не взята) и придумать какой-то предикат, определяющий что количество переменных x со значением 1 ровно k штук.
1. lapkin25 Автор
  30.09.2025 00:14
  #28899584
  Тогда длина КНФ будет порядка .
  1. qw1
    30.09.2025 00:14
    #28899932
    Это если "в лоб" делать.
    А если реализовать на булевских функциях комбинационную схему сумматора, и сравнивать его побитовый выход с числом k?
    
    lapkin25 Автор
    30.09.2025 00:14
    #28900734
    Тогда потребуется соединить N сумматоров. К тому же сложность решения такой задачи выполнимости может сильно возрасти. В первоначальном варианте КНФ имеет простую структуру, и методу типа резолюций будет легче справиться с этой задачей.
    
    qw1
    30.09.2025 00:14
    #28905790
    Тут же не полноценные сумматоры, а только делающие +1*xi к предыдущему выходу.
    И длина числа (кол-во суммируемых бит log2(k), что немного.
    
    Интересна зависимость, как растёт сложность задачи от числа свободных переменных.
    Конечно, зависит от формул. Но мне кажется, в общем случае - экспоненциально.
    То есть, начиная с каких-то N,M оптимизация станет обязательной.