Как решить проблему покрытия вершины с помощью SAT и оптимизации?

Question

Итак, прямо сейчас я работаю над использованием SAT для решения проблемы минимального покрытия вершин, и вот моя кодировка для графа G = {V,E} имеет k покрытий вершин, и вот пункты:

Let n = sizeof(V);

Во-первых, хотя бы одна вершина находится в вершинном покрытии:

For i in {1..k}
    Add clause (x<1,i> ∨ x<2,i> ∨ ··· ∨ x<n,i>);

Тогда ни одна вершина не может появиться дважды в вершинном покрытии:

For j in {1..n}
    For l and m in {1..k} with l < m
        Add clause (¬x<j,l> ∨ ¬x<j,m>) 

После этого только одна вершина может появиться в определенной позиции в вершинном покрытии:

For j in {1..k}
    For l and m in {1..n} with l < m
        Add clause (¬x<l,j> ∨ ¬x<m,j>) 

Наконец, хотя бы одна вершина в вершинном покрытии должна происходить из ребер:

For i and j in each edge e from E
    Add clause (x<i,1> ∨ x<i,2> ∨ ... ∨ x<i,k> ∨ x<j,1> ∨ ... ∨ x<j,k>)

Теперь я могу получить минимальное покрытие вершин, используя эту кодировку, но эффективность очень низкая. Я могу получить результат только для любого графа с < 20 вершинами, иначе мне потребуются минуты и часы, чтобы получить результат. Сейчас я подумываю снизить его с SAT еще больше, возможно, до 3SAT. Но похоже, что я не могу просто изменить все предложения с nCNF на 3CNF для получения того же результата. Может ли кто-нибудь помочь мне понять, что мне делать дальше? Нужна ли мне новая кодировка?

Огромное спасибо.

Кстати, я использую MiniSAT в качестве решателя.

Answer 1

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

Примечание: мой пример основан на синтаксисе SMT-LIB и может быть решен с помощью решателя MaxSMT, например, z3 и optimathsat. Однако, поскольку он не использует никаких функций SMT, вы можете написать то же самое в стандартном формате WCNF, используемом на соревнованиях MaxSAT. Это даст вам больше выбора при выборе решателя для решения проблемы. Я могу ошибаться, но я предполагаю, что решатели MaxSAT могут превзойти MaxSMT в этой конкретной проблеме.

---

Пусть G = {V, E} - граф.

Сначала объявите логическую переменную для каждой вершины графа:

(declare-fun vertex_1 () Bool)
...
(declare-fun vertex_K () Bool)

(Любая вершина без ребер должна быть опущена, потому что это просто потеря времени.)

Во-вторых, объявите логическую переменную для каждого ребра в графе, соединяющего вершину i с вершиной j (считать неориентированным)

(declare-fun edge_i_j () Bool)
...

В-третьих, утверждайте, что каждое ребро edge_i_j должны быть покрыты:

(assert edge_i_j)
...

В-четвертых, если край edge_i_j покрыта, то либо вершина i или вершина j должно быть true:

(assert (=> edge_i_j (or vertex_i vertex_j)))
...

В-пятых, для каждого vertex_iутверждать с мягкой оговоркой, чтоvertex_i должно быть false. Если это не так, получите штраф в размере1 по стоимости cover:

(assert-soft (not vertex_i) :weight 1 :id cover)

Наконец решим проблему:

(set-option :config opt.maxsmt_engine=maxres) ; only for optimathsat
(minimize cover)                              ; only for optimathsat
(check-sat)
(get-objectives)
(get-model)

На этом этапе можно использовать любой эффективный движок MaxSAT/MaxSMT (например, MaxRes), чтобы получить модель, которая покрывает все ребра, используя наименьшее количество вершин (если таковые имеются).