회로 만족도 문제

Circuit satisfiability problem
왼쪽 회로는 만족스럽지만 오른쪽 회로는 만족스럽지 않습니다.

이론 컴퓨터 과학에서 회로 만족도 문제(Circuit-SAT, Circuit이라고도 함)SAT, 수능 등)은 특정 부울회로에 [1]출력을 실현하는 입력이 할당되어 있는지 여부를 판정하는 문제입니다.즉, 소정의 부울 회로에 대한 입력이 1 또는 0으로 일관되게 설정될 수 있는지 여부를 묻고, 회로는 1을 출력한다.이 경우 회로는 만족스럽다고 불립니다.그렇지 않으면 회로를 불만족이라고 합니다.오른쪽 그림에서는 양쪽 입력을 1로 설정하면 왼쪽 회로는 만족할 수 있지만 오른쪽 회로는 만족할 수 없다.

CircuitSAT는 Boolean Sufficibility Problem([2]SAT; 부울 만족도 문제)과 밀접하게 관련되어 있으며 마찬가지로 NP-complete로 증명되어 있습니다.이것은 원형 NP-완전 문제이며, Cook-Levin 정리는 때때로 회로에서 증명됩니다.SAT 대신 SAT를 사용하여 NP-완전성을 [1][3]증명하기 위해 다른 만족도 문제로 축소합니다.의 임의의 게이트를하는 회로의 만족도는 시간( 0O([4]로 판단할 수 있습니다.

NP-완전성의 증명

회로와 만족스러운 입력 세트가 주어지면 각 게이트의 출력을 일정한 시간에 계산할 수 있습니다.따라서 회로의 출력은 다항식 시간으로 검증할 수 있다.따라서 회선 SAT는 복잡도 클래스 NP에 속합니다.NP-hardness를 나타내기 위해 3SAT에서 Circuit SAT로 축소를 구성할 수 있습니다.

원래의 3SAT 공식에 , x, (\}, \ 및 연산자(AND, OR, NOT) , (\2},\가 포함되어 있다고 가정합니다.교환입니다.3SAT 공식에 따라 게이트를 연결합니다.예를 들어, 3SAT 공식 x 2) 3, { x_})일 경우 회로에는 AND, OR 및 NOT 게이트의 3가지 입력이 있습니다. 1에 하는 입력은 x2,{ 의 AND 게이트로 전송되기 전에 반전되고 AND 게이트의 출력은 x의 게이트로 전송됩니다

3SAT 공식은 위에서 설계한 회로와 같기 때문에 동일한 입력에 대해 출력이 동일하다는 점에 유의하십시오.따라서 3SAT 공식에 만족스러운 할당이 있을 경우 대응하는 회로는 1을 출력하고 그 반대도 마찬가지입니다.이것은 유효한 삭감이며, 회선 SAT는 NP 하드입니다.

이것으로 회선 SAT가 NP-Complete라는 증명이 완료되었습니다.

제한된 변종 및 관련 문제

평면 회선 SAT

정확히 두 개의 입력이 있는 NAND 게이트만 포함하는 평면 부울 회로(즉, 기본 그래프가 평면인 부울 회로)가 주어졌다고 가정합니다.Planel Circuit SAT는 이 회로에 출력을 실현하는 입력이 할당되어 있는지 여부를 판별하는 문제입니다.이 문제는 [5]NP-완전입니다.실제로 회선 내의 게이트가 NOR 게이트가 되도록 제한을 변경하면 결과적으로 발생하는 문제는 NP-완전인 [5]채로 있습니다.

회선 UNSAT

회선 UNSAT는 입력의 가능한 모든 할당에 대해 특정 부울 회선이 false를 출력하는지 여부를 판별하는 문제입니다.이것은 회선 SAT 문제의 보완이므로 Co-NP-완전입니다.

회선으로부터의 삭감앉았다

회선으로부터의 삭감SAT 또는 그 변형은 특정 문제의 NP-hardness를 보여주기 위해 사용될 수 있으며 이중 레일 및 이진 로직 감소에 대한 대안을 제공합니다.이러한 축소가 필요한 가젯은 다음과 같습니다.

  • 와이어 가젯이 장치는 회로 내의 전선을 시뮬레이트합니다.
  • 분할된 가젯이 가젯을 사용하면 모든 출력 와이어가 입력 와이어와 동일한 값을 갖습니다.
  • 회로 게이트를 시뮬레이트하는 장치입니다.
  • 진정한 터미네이터 가젯입니다.이 가젯은 회로 전체의 출력이 True가 되도록 강제하기 위해 사용됩니다.
  • 턴 가젯.이 장치를 사용하면 필요에 따라 와이어를 올바른 방향으로 리디렉션할 수 있습니다.
  • 크로스오버 가젯이 장치를 사용하면 두 개의 와이어가 상호 작용하지 않고 서로 교차할 수 있습니다.

지뢰 찾기 추론 문제

이 문제는 지뢰 찾기 보드가 주어진 모든 폭탄을 찾을 수 있는지 여부를 묻습니다.Circuit UNSAT 문제를 [6]줄임으로써 CoNP-Complete임이 증명되었습니다.이 감소를 위해 구성된 가젯은 와이어, 분할, AND 및 NOT 게이트와 [7]터미네이터입니다.이 기기들에 관한 세 가지 중요한 관찰이 있다.첫째, 분할 가젯은 NOT 가젯과 턴 가젯으로도 사용할 수 있습니다.둘째, AND 가젯과 NOT 가젯을 함께 사용하면 범용 NAND 게이트를 시뮬레이션할 수 있기 때문에 구성만으로 충분합니다.마지막으로 3개의 NAND로 XOR를 시뮬레이션할 수 있고 XOR로 크로스오버를 구축하기에 충분하기 때문에 필요한 크로스오버 가젯을 제공합니다.

Tseytin 변환

주요 기사:체이틴 변환

Tseytin 변환은 Circuit-SAT에서 SAT로 쉽게 축소됩니다.만약 회로를 완전히 2-input 낸드(Boolean사업자들의functionally-complete 세트)게이츠의 회로에 변수, 그 다음에는 각각 NAND문을 모든 네트를 부여하면 생성된다 그 변화를 설명하기 위해 접속사 정규형 조항에 v1과 v2는 입력 ∧(v∨ v3)∧(¬v1 ∨ ¬v2 ∨ ¬v3),(v1∨ v3)을 짓기 쉽다. 낸드 gate 및3 v는 출력입니다.이 절들은 세 변수 간의 관계를 완전히 설명합니다.모든 게이트로부터의 절과 회로의 출력 변수가 참이 되도록 구속하는 추가 절을 결합함으로써 절감을 완료한다.모든 제약을 만족시키는 변수의 할당은 원래 회로가 만족할 수 있는 경우에만 존재하며, 모든 해결책은 다음과 같은 입력을 찾는 원래의 문제에 대한 해결책이다.회로를 [1][8]1로 출력합니다.반대로, SAT는 회선 SAT로 환원할 수 있습니다.부울식을 회선으로 고쳐서 해결함으로써, 3차적으로 행해집니다.

「 」를 참조해 주세요.

레퍼런스

  1. ^ a b c David Mix Barrington and Alexis Maciel (July 5, 2000). "Lecture 7: NP-Complete Problems" (PDF).
  2. ^ Luca Trevisan (November 29, 2001). "Notes for Lecture 23: NP-completeness of Circuit-SAT" (PDF). Archived from the original (PDF) on December 26, 2011. Retrieved February 4, 2012.
  3. ^ 예를 들어 Scott Aaronson의 데모크리투스 이후 양자컴퓨팅 강좌 강의 노트에 기재된 비공식 증거를 참조하십시오.
  4. ^ Sergey Nurk (December 1, 2009). "An O(2^{0.4058m}) upper bound for Circuit SAT".
  5. ^ a b "Algorithmic Lower Bounds: Fun With Hardness Proofs at MIT" (PDF).
  6. ^ Scott, Allan; Stege, Ulrike; van Rooij, Iris (2011-12-01). "Minesweeper May Not Be NP-Complete but Is Hard Nonetheless". The Mathematical Intelligencer. 33 (4): 5–17. doi:10.1007/s00283-011-9256-x. ISSN 1866-7414.
  7. ^ Kaye, Richard. Minesweeper is NP-complete (PDF).
  8. ^ Marques-Silva, João P. and Luís Guerra e Silva (1999). "Algorithms for Satisfiability in Combinational Circuits Based on Backtrack Search and Recursive Learning" (PDF).[영구 데드링크]