Một định lý tiêu chuẩn là khả năng thỏa mãn mạch boolean là NP-đầy đủ (được hiển thị trong CLRS, Ví dụ).
Tôi quan tâm đến ý nghĩa chính thức của những tuyên bố này.
Từ CLRS, tôi có thể trích dẫn rằng
$$\text{CIRCUIT-SAT} = \{C \mid \text{$C$ là một mạch tổ hợp boolean thỏa mãn}\}$$
Trong Bitansky và cộng sự., tính thỏa mãn của mạch boolean được sử dụng để nắm bắt mệnh đề cần chứng minh.
Tuy nhiên, đây không phải là CIRCUIT-SAT: Bitansky et al. xem xét sự thỏa mãn của một mạch $C$ vì một đầu vào $x$. CIRCUIT-SAT chỉ mô tả sự hài lòng của một mạch $C$ vì không tí nào đầu vào $x$.
Một zk-SNARK chứng minh các tuyên bố $x \in L$ vì $L \trong NP$.
Điều được thực hiện để tạo zk-SNARK cho khả năng thỏa mãn mạch boolean là giảm $L$ đến một mạch boolean $C$ như vậy mà $C$ là thỏa đáng cho một đầu vào $x$ nếu $x \in L$. $C$ người mẫu $L$, có thể nói như vậy.
Tôi bối rối bởi những người nói rằng khả năng thỏa mãn mạch boolean (hoặc số học) là NP-đầy đủ. Như tôi hiểu nó, $L$ cần phải được mô hình hóa bởi một mạch $C$. Tuy nhiên, nếu tôi đi theo định nghĩa của CIRCUIT-SAT, $x$ sẽ cần phải được chuyển đổi thành một mạch $C$.
CIRCUIT-SAT cho zk-SNARK sẽ trông như thế nào
$$\text{CIRCUIT-SAT} = \{ (C, x) \mid \text{$C$ là mạch tổ hợp boolean thỏa đáng cho đầu vào $x$}\}$$
Chúng tôi muốn một mạch mỗi ngôn ngữ, không phải trên mỗi đầu vào.
Vì vậy, khi ai đó nói rằng khả năng đáp ứng của các mạch, R1CS, QSP hoặc QAP là NP-đầy đủ trong ngữ cảnh của zk-SNARK, thì thực tế họ có đề cập đến định nghĩa của tôi về CIRCUIT-SAT và các định nghĩa tương tự không?