Проблема выполнимости схемы - Википедия - Circuit satisfiability problem

Схема слева пригодна, а схема справа - нет.

В теоретическая информатика, то проблема выполнимости схемы (также известен как CIRCUIT-SAT, CircuitSAT, CSATи т. д.) является проблема решения определения того, является ли данный Логическая схема имеет назначение своих входов, которое делает выход истинным.[1] Другими словами, он спрашивает, могут ли входы данной логической схемы быть последовательно установлены на 1 или же 0 так что схема выводит 1. Если это так, схема называется удовлетворительный. В противном случае схема называется неудовлетворительно. На рисунке справа левая схема может быть удовлетворена путем установки обоих входов на 1, но правильная схема неудовлетворительна.

CircuitSAT тесно связан с Проблема логической выполнимости (SAT), и, как было доказано, НП-полный.[2] Это прототип NP-полной проблемы; в Теорема Кука – Левина иногда доказывается на CircuitSAT, а не на SAT, а затем сводится к другим задачам выполнимости, чтобы доказать их NP-полноту.[1][3] Выполнимость схемы, содержащей произвольные бинарные вентили могут быть решены во времени .[4]

Доказательство NP-полноты

Имея схему и удовлетворительный набор входов, можно вычислить выход каждого элемента за постоянное время. Следовательно, выходной сигнал схемы можно проверить за полиномиальное время. Таким образом, схема SAT относится к классу сложности NP. Показывать NP-твердость, можно построить снижение из 3СБ к цепи SAT.

Предположим, что исходная формула 3SAT содержит переменные , и операторы (И, ИЛИ, НЕ) . Разработайте схему так, чтобы она имела вход, соответствующий каждой переменной, и вентиль, соответствующий каждому оператору. Подключите ворота по формуле 3SAT. Например, если формула 3SAT имеет вид схема будет иметь 3 входа: один логический элемент И, один логический элемент ИЛИ и один элемент НЕ. Вход, соответствующий будет инвертирован перед отправкой в ​​логический элемент И с и выход логического элемента И будет отправлен в логический элемент ИЛИ с

Обратите внимание, что формула 3SAT эквивалентна схеме, разработанной выше, поэтому их выход такой же для того же входа. Следовательно, если формула 3SAT имеет удовлетворительное назначение, тогда соответствующая схема будет выводить 1, и наоборот. Итак, это допустимое сокращение, а схема SAT NP-сложна.

Это завершает доказательство того, что схема SAT является NP-полной.

Ограниченные варианты и связанные с ними проблемы

Планарная схема SAT

Предположим, что нам дана плоская логическая схема (т. Е. Логическая схема, базовый граф которой планарный ), содержащий только NAND ворота ровно с двумя входами. Планарная схема SAT - это проблема решения проблемы определения того, имеет ли эта схема назначение своих входов, которое делает выход истинным. Эта проблема является NP-полной.[5] Фактически, если изменить ограничения так, что любой вентиль в схеме будет НИ ворота, полученная задача остается NP-полной.[5]

Схема UNSAT

Схема UNSAT - это проблема решения, заключающаяся в том, чтобы определить, выдает ли данная логическая схема ложь для всех возможных назначений ее входов. Это дополнение к проблеме Circuit SAT и, следовательно, Со-НП-полный.

Снижение от CircuitSAT

Редукция из CircuitSAT или ее вариантов может быть использована для демонстрации NP-сложности определенных проблем и предоставляет нам альтернативу редукциям с двойной шиной и двоичной логикой. Гаджеты, которые необходимо создать для такого сокращения:

  • Проводной гаджет. Этот гаджет имитирует провода в цепи.
  • Раздельный гаджет. Этот гаджет гарантирует, что все выходные провода имеют то же значение, что и входной провод.
  • Гаджеты, имитирующие ворота автодрома.
  • Настоящий терминатор. Этот гаджет используется для принудительного установления значения True на выходе всей схемы.
  • Поворотный гаджет. Этот гаджет позволяет нам перенаправлять провода в нужном направлении по мере необходимости.
  • Кроссовер-гаджет. Этот гаджет позволяет нам соединять два провода, не взаимодействуя друг с другом.

Проблема вывода сапера

В этой задаче спрашивается, можно ли найти все бомбы с учетом Тральщик доска. Было доказано, что это CoNP-Complete через сокращение от Circuit UNSAT проблема.[6] Для этого сокращения созданы следующие устройства: провод, разделение, логические элементы И и НЕ и терминатор.[7] Относительно этих устройств можно сделать три важных замечания. Во-первых, разделенный гаджет также можно использовать как гаджет НЕ и как гаджет поворота. Во-вторых, создания гаджетов AND и NOT достаточно, потому что вместе они могут имитировать универсальный логический элемент NAND. Наконец, поскольку мы можем моделировать XOR с тремя NAND, и поскольку XOR достаточно для создания кроссовера, это дает нам необходимый кроссовер.

Преобразование Цейтина

Основная статья: Преобразование Цейтина

В Преобразование Цейтина это прямое сокращение от Circuit-SAT до СИДЕЛ. Преобразование легко описать, если схема полностью построена из двух входов. Ворота NAND (а функционально-законченный набор логических операторов): назначить каждый сеть в схеме переменную, затем для каждого логического элемента И-НЕ построить конъюнктивная нормальная форма статьи (v1 ∨ v3) ∧ (v2 ∨ v3) ∧ (¬v1 ∨ ¬v2 ∨ ¬v3), куда v1 и v2 являются входами в логический элемент И-НЕ и v3 это выход. Эти пункты полностью описывают взаимосвязь между тремя переменными. Объединение предложений из всех вентилей с дополнительным предложением, ограничивающим выходную переменную схемы, чтобы она была истинной, завершает сокращение; присвоение переменных, удовлетворяющих всем ограничениям, существует тогда и только тогда, когда исходная схема является выполнимой, и любое решение является решением исходной проблемы поиска входов, которые делают выход схемы равным 1.[1][8] Обратное - что SAT сводится к Circuit-SAT - следует тривиально, переписывая булеву формулу в виде схемы и решая ее.

Смотрите также

Рекомендации

  1. ^ а б c Дэвид Микс Баррингтон и Алексис Масил (5 июля 2000 г.). «Лекция 7: NP-полные задачи» (PDF).
  2. ^ Лука Тревизан (29 ноября 2001 г.). "Примечания к лекции 23: NP-полнота схемы-SAT" (PDF).
  3. ^ См. Также, например, неофициальное доказательство, приведенное в Скотт Ааронсон с конспект лекций с его курса Квантовые вычисления со времен Демокрита.
  4. ^ Сергей Нурк (1 декабря 2009 г.). «Верхняя граница O (2 ^ {0.4058m}) для контура SAT».
  5. ^ а б "Алгоритмические нижние границы: развлечения с доказательствами твердости в Массачусетском технологическом институте" (PDF).
  6. ^ Скотт, Аллан; Стеге, Ульрике; ван Рой, Ирис (01.12.2011). «Сапер не может быть NP-полным, но, тем не менее, сложен». Математический интеллект. 33 (4): 5–17. Дои:10.1007 / s00283-011-9256-х. ISSN  1866-7414.
  7. ^ Кэй, Ричард. Сапер NP-полный (PDF).
  8. ^ Маркес-Сильва, Жоао П. и Луис Герра э Сильва (1999). «Алгоритмы выполнения в комбинационных схемах на основе поиска с возвратом и рекурсивного обучения» (PDF).[постоянная мертвая ссылка ]