Измерение сложности экземпляров SAT

Question

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

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

Учитывая пример SAT, есть ли какая -то быстрая эвристика для измерения сложности? Единственное условие состоит в том, что эти эвристики будут быстрее, чем фактически запуск существующих решателей SAT в этом экземпляре.

---

Связанный вопрос

Какие проблемы SAT просты? на cstheory.se. Эти вопросы задаются о привлеченных наборах экземпляров. Это аналогичный вопрос, но не совсем такой же. Я действительно заинтересован в эвристике, которая, учитывая один экземпляр, делает какое-то полуинтеллектное предположение о том, будет ли экземпляр трудным для решения.

Answer 1

В целом, это очень актуальный и интересный вопрос исследования. «Один из способов - запустить существующих решателей ...» И что это даже скажет нам? Мы могли видеть эмпирически, что экземпляр кажется трудным для конкретного решателя или конкретного алгоритма/эвристического, но что он на самом деле говорит о твердости этого экземпляра?

Одним из способов, которые были преследованы, является выявление различных структурных свойств случаев, которые приводят к эффективным алгоритмам. Эти свойства действительно предпочитают быть «легко» идентифицируемыми. Примером является топология базового графика ограничения, измеренная с использованием различных параметров ширины графика. Например, известно, что экземпляр решается в полиномиальное время, если прогиба дерева базового графика ограничения ограничена постоянной.

Другой подход был сосредоточен на роли скрытая структура экземпляров. Одним из примеров является Backdoor Set, означающее набор переменных, так что когда они создаются, оставшаяся проблема упрощается в класс. Например, Williams et al., 2003 1] Покажите, что даже при учете стоимости поиска переменных Backdoor можно все еще получить общее вычислительное преимущество, сосредоточившись на наборе Backdoor, при условии, что этот набор достаточно мал. Более того, Dilkina et al., 2007 2] Обратите внимание, что решатель вызвал Satz-Rand Удивительно хорошо находит небольшие сильные бэкдоры в ряде экспериментальных областей.

В последнее время, Ansotegui et al., 2008 3] предлагают использование сложности пространства, подобной деревьям, в качестве меры для решателей на основе DPLL. Они доказывают, что также постоянно связанное пространство подразумевает существование алгоритма решения полиномиального времени, где пространство является степенью полинома (теорема 6 в статье). Более того, они показывают, что пространство меньше чем размер прорезания велосипедов. Фактически, при определенных предположениях пространство также меньше, чем размер бэкдоров.

Они также формализуют то, что, я думаю, вы хотите, то есть:

Найдите меру $ psi $, и алгоритм, который дал формулу $ gamma $, решает удовлетворенность во времени $ o (n^{ psi ( gamma)}) $. Чем меньше мера, тем лучше он характеризует твердость формулы.

---

1] Уильямс, Райан, Карла П. Гомес и Барт Селман. «Бэкдоры к типичной сложности случая». Международная совместная конференция по искусственному интеллекту. Тол. 18, 2003.

2] Дилкина, Бистра, Карла Гомес и Ашиш Сабхарвал. «Компромисс в сложности обнаружения Backdoor». Принципы и практика программирования ограничения (CP 2007), с. 256-270, 2007.

3] Ансотеги, Карлос, Мария Луиза Бонет, Джорди Леви и Фелип Мана. «Измерение твердости экземпляров SAT». В материалах 23-й Национальной конференции по искусственному интеллекту (AAAI'08), с. 222-228, 2008.

Answer 2

Поскольку вы знаете о фазовом переходе, позвольте мне упомянуть несколько других простых проверок, о которых я знаю (которые, вероятно, подчинены анализу графа ограничения):

• Некоторые ранние случайные генераторы SAT непреднамеренно создали в основном простые формулы, потому что они использовали «постоянную плотность», что означает примерно одинаковую долю всей длины пункта. Они были в основном просты, потому что 2-х приличия и единицы значительно упрощают проблему, как и следовало ожидать, и действительно длинные предложения либо не добавляют много ветвления, либо облегчают гипер-разрешение еще лучше. Таким образом, кажется, что лучше придерживаться предложений с фиксированной длиной и варьировать другие параметры.
• Точно так же мощное правило упрощения - это чистое буквальное устранение. Очевидно, что формула действительно такая же сложная, как и количество нечистых литералов, в которой она имеет. Потому что разрешение создает новую нумерацию положений $ | x |*| lnot x | $ (это означает, что продукт происшествий $ x $ и его отрицание), количество разрешений максимизируется, когда существует равное количество положительных и отрицательных литералов для каждой переменной. Следовательно, сбалансированные генераторы SAT.
• Существует также техника, называемая «No Triangle SAT», которая кажется довольно свежей [1], которая является своего рода генератором жесткого значения, который запрещает «треугольникам». Треугольник - это набор предложений, содержащих 3 переменных $ V_1, V_2, V_3 $ которые происходят в паре во всех комбинациях в некоторых наборах пунктов (т.е. $ {v_1, v_2, ... }, {v_2, v_3, ... }, {v_1, v_3, ... } $) По -видимому, треугольники, как правило, облегчают формулу для известных решателей.

[1] https://arxiv.org/pdf/1903.03592.pdf

Answer 3

Помимо отличного ответа Джухо, вот еще один подход:

Ercsey-Ravasz & Toroczkai, Оптимизация твердость как временный хаос в аналоговом подходе к удовлетворению ограничения, Physics Nature Physics Том 7, стр. 966–970 (2011).

Этот подход состоит в том, чтобы переписать проблему SAT в динамическую систему, где любой аттрактор системы является решением проблемы SAT. Бассейны притяжения системы являются более фрактальными, так как проблема становится сложнее, и поэтому «сложность» экземпляра SAT может быть измерена путем изучения того, насколько хаотичны переходные процессы до сходится к системе.

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

Нетрудно придумать динамическую систему, для которой «решения» являются решением заданной проблемы SAT, но немного сложнее убедиться, что все решения являются аттракторами, а не репеллерами. Их решение состоит в том, чтобы ввести энергетические переменные (сродни мультипликаторам Lagrange), чтобы представить, насколько сильно нарушается ограничение, и попытаться заставить систему минимизировать энергию системы.

Интересно, что, используя их динамическую систему, вы можете решить проблемы SAT в полиномиальное время на аналоговом компьютере, что само по себе является замечательным результатом. Есть улов; Это может потребовать экспоненциально больших напряжений, чтобы представлять энергетические переменные, поэтому, к сожалению, вы не можете понять это на физическом оборудовании.