Стандартная теорема состоит в том, что выполнимость логических схем является NP-полной (показано на рис. CLRS, Например).
Меня интересует, что формально означают эти заявления.
Из CLRS я могу процитировать, что
$$\text{CIRCUIT-SAT} = \{C \mid \text{$C$ — выполнимая логическая комбинационная схема}\}$$
В Битанский и др., выполнимость логических схем используется для фиксации утверждения, которое необходимо доказать.
Однако это не CIRCUIT-SAT: Bitansky et al. рассмотрим выполнимость схемы $С$ за ан вход $х$. CIRCUIT-SAT просто описывает выполнимость схемы $С$ за Любые вход $х$.
Zk-SNARK доказывает утверждения $x \в л$ за $L \в НП$.
Что делается для создания zk-SNARK для выполнимости логических схем, так это уменьшение $L$ к булевой схеме $С$ такой, что $С$ выполнимо для входа $х$ если $x \в л$. $С$ модели $L$, так сказать.
Меня смущают люди, говорящие, что выполнимость логических (или арифметических) схем является NP-полной. Как я понимаю, $L$ необходимо смоделировать схемой $С$. Однако, если бы я следовал определению CIRCUIT-SAT, $х$ нужно будет преобразовать в цепь $С$.
Как должен выглядеть CIRCUIT-SAT для zk-SNARK:
$$\text{CIRCUIT-SAT} = \{ (C, x) \mid \text{$C$ — выполнимая логическая комбинационная схема для входа $x$}\}$$
Мы хотим цепь на язык, а не на вход.
Итак, когда кто-то говорит, что выполнимость цепей, R1CS, QSP или QAP является NP-полной в контексте zk-SNARK, ссылаются ли они на мое определение CIRCUIT-SAT и подобных?
