В теоретической информатике проблема выполнимости схемы ( также известная как CIRCUIT-SAT , CircuitSAT , CSAT и т. д.) — это проблема принятия решения о том, имеет ли данная булева схема назначение входов, которое делает выход истинным. [1] Другими словами, она спрашивает, могут ли входы данной булевой схемы быть последовательно установлены в 1 или 0 так, чтобы схема выдавала 1. Если это так, схема называется выполнимой . В противном случае схема называется невыполнимой. На рисунке справа левая схема может быть удовлетворена, установив оба входа равными 1 , но правая схема невыполнима.
CircuitSAT тесно связана с задачей булевой выполнимости (SAT) и, как было доказано, является NP-полной . [2] Это прототипическая NP-полная задача; теорема Кука–Левина иногда доказывается на CircuitSAT вместо SAT, и тогда CircuitSAT можно свести к другим задачам выполнимости, чтобы доказать их NP-полноту. [1] [3] Выполнимость схемы, содержащей произвольные двоичные вентили, может быть определена со временем . [4]
При наличии схемы и удовлетворяющего набора входов можно вычислить выход каждого вентиля за постоянное время. Следовательно, выход схемы проверяем за полиномиальное время. Таким образом, Circuit SAT принадлежит к классу сложности NP. Чтобы показать NP-трудность , можно построить сокращение от 3SAT до Circuit SAT.
Предположим, что исходная формула 3SAT имеет переменные и операторы (AND, OR, NOT) . Разработайте схему так, чтобы она имела вход, соответствующий каждой переменной, и вентиль, соответствующий каждому оператору. Соедините вентили в соответствии с формулой 3SAT. Например, если формула 3SAT — схема будет иметь 3 входа, один вентиль AND, один вентиль OR и один вентиль NOT. Вход, соответствующий будет инвертирован перед отправкой на вентиль AND с помощью , а выход вентиля AND будет отправлен на вентиль OR с помощью
Обратите внимание, что формула 3SAT эквивалентна схеме, разработанной выше, поэтому их выход одинаков для одного и того же входа. Следовательно, если формула 3SAT имеет удовлетворяющее назначение, то соответствующая схема выведет 1, и наоборот. Таким образом, это допустимое сокращение, и схема SAT является NP-трудной.
Это завершает доказательство того, что схема SAT является NP-полной.
Предположим, что нам дана планарная булева схема (т. е. булева схема, базовый граф которой является планарным ), содержащая только вентили NAND с ровно двумя входами. Плоская схема SAT — это задача принятия решения о том, имеет ли эта схема назначение входов, которое делает выход истинным. Эта задача является NP-полной. Более того, если ограничения изменяются так, что любой вентиль в схеме становится вентилем NOR , то результирующая задача остается NP-полной. [5]
Circuit UNSAT — это задача принятия решения о том, выдает ли данная булева схема false для всех возможных назначений ее входов. Это дополнение к задаче Circuit SAT, и поэтому является Co-NP-полной .
Сокращение от CircuitSAT или его вариантов может быть использовано для демонстрации NP-трудности некоторых проблем и предоставляет нам альтернативу сокращениям с двойными шинами и двоичной логикой. Гаджеты, которые необходимо построить для такого сокращения, следующие:
В этой задаче спрашивается, возможно ли обнаружить все бомбы, имея доску Minesweeper . Было доказано, что она является CoNP-полной с помощью сокращения из задачи Circuit UNSAT. [6] Гаджеты, построенные для этого сокращения, это: провод, разделение, вентили AND и NOT и терминатор. [7] Есть три важных замечания относительно этих гаджетов. Во-первых, раздельный гаджет также может использоваться как гаджет NOT и гаджет turn. Во-вторых, достаточно построить гаджеты AND и NOT, потому что вместе они могут имитировать универсальный вентиль NAND. Наконец, поскольку три NAND могут быть составлены без пересечений для реализации XOR, и поскольку XOR достаточно для построения кроссовера, [8] это дает нам необходимый гаджет кроссовера.
Преобразование Цейтина представляет собой прямое сокращение от Circuit-SAT до SAT . Преобразование легко описать, если схема полностью построена из 2-входовых вентилей NAND ( функционально полный набор булевых операторов): назначим каждой сети в схеме переменную, затем для каждого вентиля NAND построим предложения конъюнктивной нормальной формы ( v 1 ∨ v 3 ) ∧ ( v 2 ∨ v 3 ) ∧ (¬ v 1 ∨ ¬ v 2 ∨ ¬ v 3 ), где v 1 и v 2 являются входами вентиля NAND, а v 3 является выходом. Эти предложения полностью описывают связь между тремя переменными. Объединение предложений из всех вентилей с дополнительным предложением, ограничивающим выходную переменную схемы, чтобы она была истинной, завершает сокращение; назначение переменных, удовлетворяющее всем ограничениям, существует тогда и только тогда, когда исходная схема выполнима, и любое решение является решением исходной задачи нахождения входов, которые делают выход схемы равным 1. [1] [9] Обратное утверждение — что SAT сводится к Circuit-SAT — следует тривиально, если переписать булеву формулу в виде схемы и решить ее.
