Насколько эффективны основанные на DPLL SAT-решатели на удовлетворительных экземплярах PHP?

Мы знаем, что основанные на DPLL SAT-решатели не могут правильно ответить на неудовлетворительных экземплярах (принцип "голубиной дыры"), например, "существует инъективное отображение от к ": $\mathrm{PHP}$ $n+1$ $n$

P H P_{n}^{n + 1} := (\underset{i \in [n + 1]}{⋀} \underset{j \in [n]}{⋁} p_{i, j}) \land (\underset{i \neq i^{'} \in [n + 1]}{⋀} \underset{j \in [n]}{⋀} (\neg p_{i, j} \lor \neg p_{i^{'}, j}))

$\mathrm{PHP^{n+1}_{n}} := \left(\bigwedge_{i\in[n+1]} \ \bigvee_{j\in[n]} \ p_{i,j}\right) \wedge \left(\bigwedge_{i\neq i'\in[n+1]} \ \bigwedge_{j\in[n]} \ (\lnot p_{i,j} \vee \lnot p_{i',j})\right)$

Я ищу результаты о том, как они работают на удовлетворительных экземплярах , например, на "есть инъективное отображение от до ". $\mathrm{PHP}$ $n$ $n$

Находят ли они быстро удовлетворительное назначение в таких случаях?

cc.complexity-theory lo.logic proof-complexity Кава
источник

Под «неправильным ответом» вы подразумеваете «нехватка ресурсов при достаточно больших значениях n»?

Виджай Д

@ Kaveh Вы разрешаете повторение предложений и / или повторение переменных в одном предложении? Спасибо

Tayfun Pay

@VijayD, я имею в виду, что алгоритм не возвращает правильный ответ за полиномиальное время для достаточно большого . Я надеюсь, что можно убедительно показать, что алгоритм на основе DPLL будет работать за полиномиальное время в этом семействе.

n

$n$

Каве

@ Гикстер, я не уверен, что ты имеешь в виду. У меня есть определенное семейство формул. Вы спрашиваете, есть ли повторение в этой формуле?

Каве

На удовлетворительных экземплярах решатели SAT на основе DPLL будут обеспечивать удовлетворительное назначение за линейное время. $PHP$

Чтобы понять почему, посмотрите, как кодирование CNF неудовлетворительного экземпляра с дырами и голубями синтаксически идентично экземпляру раскраски графов, где входной граф представляет собой клику из вершин. $PHP$ $n$ $n + 1$ $k = n$ $n + 1$

Точно так же кодирование CNF выполнимого экземпляра с дырами и голубями синтаксически идентично экземпляру раскраски графов, где входной граф представляет собой клику из вершин. $PHP$ $n$ $n$ $k = n$ $n$

Теперь раскрасить клику из вершин с помощью цветов просто: отсканируйте вершины и назначьте каждому из них один из оставшихся цветов (уже назначенные цвета автоматически исключаются кликой графа, используя распространение единиц) , Какой бы из оставшихся цветов вы ни выбрали, это будет хорошо и приведет вас к удовлетворительному заданию. $n$ $n$

С точки зрения решателя DPLL: каждый раз, когда он будет пытаться угадать логическое значение переменной , такое значение будет правильным (каким бы оно ни было), потому что, безусловно, будет удовлетворительное присваивание, в котором переменная имеет предполагаемое значение. , Распространение модулей выполнит остальную часть работы, направляя решатель вдоль удовлетворительного пути (другими словами: предотвращая угадывание неправильных значений). $v_i$ $v_i$

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

Джорджио Камерани
источник

Спасибо, это то, что я ожидал. Кстати, знаете ли вы ссылку, которая утверждает это (то есть «алгоритм DPLL решает выполнимые экземпляры PHP / GC за линейное время»)?

Каве

Добро пожаловать. Я не знаю ни одной ссылки, которая бы заявляла об этом, я просто вывел это сам по некоторым необработанным рассуждениям. Не должно быть трудным официально доказать это, полагаясь на тот факт, что каждый SAT-решатель использует некоторую разумную эвристику как при выборе следующей переменной, так и при угадывании ее логического значения. Следует отметить, что на самом деле существует, по крайней мере, одна необоснованная эвристика, которая мешает нам найти решение за линейное время (такой неразумной эвристикой было бы установить значение false для каждой переменной, пока это возможно). При разумной эвристике обеспечивается линейное время.

Джорджио Камерани

Я согласен. Я надеюсь, что кто-то мог где-то это заявить, чтобы я мог ссылаться, когда мне это нужно. Я хотел бы подождать еще несколько дней, и если никто не даст ссылку, я приму этот ответ. Еще раз спасибо. :)

Каве

Мое удовольствие ;-) Ура!

Джорджио Камерани

Насколько эффективны основанные на DPLL SAT-решатели на удовлетворительных экземплярах PHP?

Ответы: