참 수량화된 부울 공식

계산 복잡도 이론에서, 언어 TQBF는 진정한 양자화된 부울 공식으로 구성된 공식 언어이다.(완전하게) 정량화된 부울 공식은 모든 변수가 문장 시작 부분에서 존재 또는 보편적 수량화자를 사용하여 정량화(또는 한계화)되는 정량화된 명제 논리의 공식이다.이러한 공식은 (자유 변수가 없기 때문에) true 또는 false에 해당합니다.이러한 수식이 true로 평가되면 해당 수식은 TQBF 언어로 표시됩니다.QSAT(Quantized SAT)라고도 합니다.

개요

계산 복잡도 이론에서, 정량화된 부울 공식 문제(QBF)는 존재 양자와 보편 양자 모두를 각 변수에 적용할 수 있는 부울 만족도 문제의 일반화이다.바꿔 말하면, 부울 변수 집합에 대한 수량화된 센텐셜 형식이 참인지 거짓인지 묻습니다.예를 들어 QBF의 인스턴스를 다음에 나타냅니다.

((x\lor z)\land y)\displaystyle \forall x\land y)

QBF는 ^[1]다항식 공간과 무제한 시간에서 결정론적 또는 비결정론적 튜링 기계에 의해 풀 수 있는 문제의 클래스인 PSPACE의 표준적인 완전한 문제입니다.추상 구문 트리의 형태로 주어진 공식은 공식을 평가하는 일련의 상호 재귀적 절차에 의해 쉽게 해결될 수 있다.이러한 알고리즘은 트리 높이에 비례하는 공간을 사용하며, 최악의 경우 선형이지만 수량자 수에 있어 시간 지수적 값을 사용합니다.

일반적으로 알려진 MA , PSPACE는 결정론적 또는 확률론적 다항식 시간 내에 QBF를 해결할 수 없으며, 주어진 솔루션을 검증할 수도 없다(실제로 만족도 문제와 달리 솔루션을 간결하게 특정할 수 있는 방법은 없다).AP = PSPACE이기 때문에 선형 시간 내에 대체 튜링 기계를 사용하여 해결할 수 있습니다. 여기서 AP는 대체 기계가 다항 ^[2]시간 내에 해결할 수 있는 문제의 클래스입니다.

결정 결과 IP = PSPACE가 제시되었을 때(^[3]인터랙티브 증명 시스템 참조), 문제의 특정 산술화를 해결함으로써 QBF를 해결할 수 있는 인터랙티브 증명 시스템을 제시함으로써 수행되었다.

QBF 공식에는 유용한 표준 형식이 많이 있습니다.예를 들어, 모든 정량자를 공식의 앞쪽으로 이동하고 범용 정량자와 실존 정량자 사이를 번갈아 이동시키는 다항식 시간 다원 감소가 있음을 보여줄 수 있다.IP = PSPACE 증명에서 유용함을 증명한 또 다른 감소가 있는데, 각 변수의 용도와 해당 변수의 결합 양자 사이에 단 하나의 범용 수량자가 배치되지 않는다.이는 산술화의 특정 하위 표현식의 제품 수를 제한하는 데 매우 중요했습니다.

프리넥스 정규형

완전 정량화된 부울 공식은 프리넥스 정규형이라고 불리는 매우 구체적인 형태를 가지고 있다고 가정할 수 있다.이것은 두 개의 기본적인 부분으로 구성되어 있습니다: 수량자만을 포함하는 부분과 일반적으로 ${\(\$ 로 표시되는 계량화되지 않은 부울 공식 포함 부분. $\displaystyle n$ n개의 \ $displaystyle\displaystyle$ n $}$ 부울 $\displaystyle n$ 변수가 $\displaystyle n$ 경우 전체 공식은 다음과 같이 쓸 수 있습니다.

\displaystyle \exists x_{1}\forall x_{3}\exists x_{n}\phi(x_{1},x_{2},x_{3},\dots,x_{n})}

여기서 모든 변수는 수량화 범위에 포함됩니다.더미 변수를 도입함으로써 프리넥스 정규 형식의 공식은 존재자와 보편자가 번갈아 나타나는 문장으로 변환할 수 있다.더미 $\displaystyle y_{1}$ $\displaystyle y_{1}$ 1 $(\$ 을 사용하여

\displaystyle \displaystyle \displaystyle x_{1}\phi(x_{2})\displaystyle \displaystyle x_{1}\displaystyle x_{2}\phi(x_{1},x_{2})\displaystyle \map x_map x_{1}\displaysty(x_{2})

두 번째 문장은 true 값은 같지만 제한된 구문을 따릅니다.완전 수량화된 부울 공식이 프리넥스 정규형이라고 가정하는 것은 증거의 빈번한 특징이다.

QBF 솔러

순진한

QBF가 TQBF에 있는지 여부를 판단하기 위한 간단한 재귀 알고리즘이 있습니다(즉, true).특정 QBF를 지정하다

({displaystyle Q_{1}x_{1}Q_{2}x_{2}\cdots Q_{n}x_{n}\phi(x_{1},x_{2},\dots,x_{n}).}

수식에 수량 지정자가 없는 경우 수식을 반환할 수 있습니다.그렇지 않으면 첫 번째 수량자를 제거하고 첫 번째 변수에 대해 가능한 두 값을 확인합니다.

({displaystyle A=Q_{2}x_{2}\cdots Q_{n}x_{n}\phi(0,x_{2}\displaystyle,x_{n}),}

B=Q_{2}x_{2}\cdots Q_{n}x_{n}\phi(1,x_{2}\displaystyle,x_{n}).

$Q_{1}=\exists$ 1 $Q_{1}=\exists$ " $Q_{1}=\exists$ { $display$ Q $_$ { 1 } = \ $exists$ $Q_{1}=\exists$ 、 A $A\lor B$ （ \ $displaystyle$ A \ lor B $A\land B$ ^[4] $A\lor B$ $Q_{1}=\forall$ 1 $Q_{1}=\forall$ " \ $displaystyle$ Q_ ${1$ } = \ $forall$ 이면 A $A\land B$ 를 $A\land B$ 합니다.

이 알고리즘은 얼마나 빨리 실행됩니까?첫 번째 QBF의 각 수량자에 대해 알고리즘은 선형적으로 작은 서브 문제만으로2개의 재귀 콜을 발신합니다.이것에 의해, 알고리즘에 지수 런타임 O(2)^[citation needed]가ⁿ 주어집니다.

이 알고리즘은 얼마나 많은 공간을 사용합니까?알고리즘을 호출할 때마다 A와 B를 계산하는 중간 결과를 저장해야 합니다.각 재귀 콜은 1개의 수량자를 떼어내기 때문에 재귀의 총 깊이는 수량자 수로 선형입니다.계량자가 없는 공식은 변수 수에서 공간 로그로 계산할 수 있습니다.초기 QBF는 완전히 정량화되었기 때문에 변수와 같은 수 이상의 정량자가 있습니다.따라서 이 알고리즘은 O(n + log n) = O(n) 공간을 사용합니다.이것에 의해, TQBF 언어는 PSPACE 복잡도 ^{[citation needed]}클래스의 일부가 됩니다.

최첨단

QBF의 PSPACE 완전성에도 불구하고 이러한 인스턴스를 해결하기 위해 많은 솔버가 개발되었습니다.(이것은 단일 존재 수량화 버전인 SAT의 상황과 유사합니다.NP-완전이지만 많은 SAT 인스턴스를 휴리스틱하게 해결할 수 있습니다.)^[5]^[6]2QBF로 알려진 2개의 정량자만 존재하는 경우는 특별한 ^[7]^{[weasel words]}주의를 받았습니다.

QBF 솔버 경합 QBFEVAL은 ^[5]^[6]2004년부터 매년 어느 정도 실행되고 있습니다.솔버는 QDIMACS 형식과 QCIR ^[8]형식 또는 QAIGER 형식의 인스턴스를 읽어야 합니다.고성능 QBF 솔버는 일반적으로 QDPLL(DPLL의 일반화) 또는 ^[5]^[6]^[7]CEGAR를 사용합니다.QBF 해결에 대한 연구는 1998년 QBF를 위한 DPLL 역추적 개발로 시작되었고,^[9] 2002년 절 학습 및 변수 제거가 도입되었다. 따라서 1960년대부터 개발되어 온 SAT 해결과 비교하면 ^[9]^{[weasel words]}QBF는 2017년 현재 비교적 젊은 연구 분야이다.

주요 QBF 솔버는 다음과 같습니다.

CADE: 증분 결정화와^{[clarification needed]} ^[10]그 답을 증명할 수 있는 능력을 바탕으로 하나의 정량자 교대로 제한된 정량화된 부울 공식(Skolem 함수를 계산하는 능력)을 해결합니다.
CAQE - 정량화된 부울 수식을 위한 CEGAR 기반 솔버. QBFEVAL 최신 ^[11]에디션의 우승자입니다.
DepQBF - 수량화된 부울^[12] 수식을 위한 검색 기반 해결사
sKizzo - 기호 스콜렘화를 사용하고, 만족도의 증명서를 추출하고, 하이브리드 추론 엔진을 사용하고, 추상 분기를 구현하고, 제한된 수량자를 처리하며, 유효한 할당을 열거한 최초의 해결사이며, QBFEVAL 2005, 2006,^[13] 2007의 수상자이다.

적용들

QBF 솔버는 안전한 계획을 포함한 (인공지능에서) 계획에 적용될 수 있다. 후자는 로봇 ^[14]공학 응용에 중요하다.QBF 솔버는 SAT 기반 ^[14]솔버에 필요한 것보다 짧은 인코딩을 제공하기 때문에 경계 모델 체크에도 적용할 수 있습니다.

QBF의 평가는 기존 정량화된 변수를 제어하는 플레이어와 보편적으로 정량화된 변수를 제어하는 플레이어의 2인 게임으로 볼 수 있다.이것에 의해, QBF 는 리액티브 합성 문제의 ^[14]부호화에 적합합니다.마찬가지로, QBF 해결사는 게임 이론에서 적대적 게임을 모델링하는 데 사용될 수 있습니다.예를 들어, QBF 솔버는 지리 게임의 승리 전략을 찾기 위해 사용할 수 있으며,^[15] 그러면 자동으로 인터랙티브하게 플레이할 수 있습니다.

QBF 솔버는 정식 등가성 체크에 사용할 수 있으며 부울 ^[14]함수를 합성하는 데도 사용할 수 있습니다.

QBF로 부호화할 수 있는 기타 유형의 문제는 다음과 같습니다.

접속 정규 형식의 불만족 공식의 절이 최소 불만족^[9]^[16] 부분 집합에 속하는지 여부 및 불만족 공식의 절이 최대 불만족^[16] 부분 집합에 속하는지 여부 검출
적합성^[9]^{[clarification needed]} 계획의 부호화
ASP 관련^[9]^{[clarification needed]} 문제
추상적^[9]^{[clarification needed]} 논쟁
선형 시간 논리 모델^[9]^{[clarification needed]} 확인
비결정론적 유한 오토마톤^[9]^{[clarification needed]} 언어
분산형^[9]^{[clarification needed]} 시스템의 통합과 신뢰성

내선번호

QBFEVAL 2020에서는 인스턴스가 Henkin 정량자(DQDIMACS 형식으로 표현)를 가질 수 있는 "DQBF 트랙"^[8]이 도입되었습니다.

PSPACE 완전성

TQBF 언어는 복잡도 이론에서 표준 PSPACE-완전 문제로서 기능합니다.PSPACE-complete가 된다는 것은 언어가 PSPACE에 있고 언어도 PSPACE-hard라는 것을 의미합니다.위의 알고리즘은 TQBF가 PSPACE에 있는 것을 나타내고 있습니다.TQBF가 PSPACE-hard임을 나타내려면 복잡도 클래스 PSPACE 내의 모든 언어가 다항식 시간에 TQBF로 축소될 수 있음을 보여줘야 합니다.예.,

\displaystyle L\in\mathsf {PSPACE}, L\leq _{p}\mathrm {TQBF}.}

즉, PSPACE 언어 L의 경우 $입력$ x가 L에 있는지 여부는 (입력 길이에 비례하여) 다항식 시간에 실행되어야 하는 $일부$ 함수 $f(x)$ 에 대해 f $f(x)$ x $f(x)$ ) { $displaystyle f($ x)}가 $f(x)$ TQBF에 있는지 $f(x)$ 를 확인하여 판단할 수 있습니다.상징적으로

\displaystyle x in L\iff f(x)\in \mathrm {TQBF} .}

TQBF가 PSPACE 하드임을 증명하려면 f를 $지정$ 해야 합니다.

L이 PSPACE 언어라고 가정합니다.이것은 L이 다항식 공간 결정론적 튜링 기계(DTM)에 의해 결정될 수 있다는 것을 의미한다.이것은 TQBF에 대한 L의 감소에 매우 중요합니다, 왜냐하면 그러한 튜링 기계의 구성은 공식에 의해 인코딩된 튜링 기계 테이프의 각 셀의 내용뿐만 아니라 기계의 상태를 나타내는 부울 변수와 함께 부울 공식으로 표현될 수 있기 때문입니다.공식이 순서를 정해요.특히 감축에서는 $c_{1}$ c1(\ $displaystyle c_{$ 1 $c_{1}$ })과 변수 $c_{2}$ c2(\ $displaystyle c_{$ 2 $c_{2}$ 를 사용합니다.이 변수 c1과 $\phi _{c_{1},c_{2},t}$ (\displaystyle c_{1}, c_ ${$ 2})는 QBF $\phi _{c_{1},c_{2},t}$ $\phi _{c_{1},c_{2},t}$ $\phi _{c_{1},c_{2},t}$ $\phi _{c_{1},c_{2},t}$ , t $\displaystyle \phi$ _ ${c_1},$ true, true, c_{ $2}}$ 를 $\phi_{c_1,c_2,t}$ 구축할 때 사용할 수 있습니다.L용 TM은 $(\$ 로 $c_{1}$ 인코딩된 Configuration에서 $(\$ 로 $c_{2}$ 인코딩된 Configuration으로 t스텝 이하로 이행할 수 있습니다. $다음$ 으로 함수 f는 L의 DTM에서 QBF $\phi _{c_{\text{start}},c_{\text{accept}},T}$ $\phi _{c_{\text{start}},c_{\text{accept}},T}$ start , $\phi _{c_{\text{start}},c_{\text{accept}},T}$ accept , $\phi _{c_{\text{start}},c_{\text{accept}},T}$ { $display$ style \ $phi$ _ { $c$ _ { \ text { $start$ } , c _ { \ $text$ { $accept$ } 。 $T$ $}}.$ $c_{start}$ 서 $c_{start}$ 는 $DTM$ 의 시작 설정, $c_{\text{accept}}$ {\ $text {accept}$ 는 $c_{start}$ $c_{\text{accept}}$ DTM의 수락 설정, T는 DTM이 어떤 구성에서 다른 설정으로 이행하기 위해 필요한 최대 스텝 수입니다.T = O(exp(n))임을 알고 있습니다.여기서 n은 입력의 길이입니다.이는 관련 DTM의 가능한 총 구성 수를 제한하기 때문입니다.물론 루프에 들어가지 않는 한 DTM은 c $c_{\mathrm {accept} }$ $c_{\mathrm {accept} }$ $c_{\mathrm {accept} }$ $c_{\mathrm {accept} }$ $c_{\mathrm {accept} }$ _ { \ $mathrm$ { accept $c_{\mathrm {accept} }$ $}$ 에 $c_{\mathrm {accept} }$ 하기 위한 설정보다 더 많은 절차를 수행할 수 없습니다.이 경우 C $c_{\mathrm {accept} }$ { \ $display style$ c _ { \ $mathrm {$ accept } $}$ } 에는 도달하지 $c_{\mathrm {accept} }$ 않습니다.

이 증명 단계에서는 $입력식$ w(물론 $c_{\text{start}}$ $\$ 가 L에 있는지 여부에 대한 질문은 QBF b c $\phi _{c_{\text{start}},c_{\text{accept}},T}$ $\phi _{c_{\text{start}},c_{\text{accept}},T}$ , $\phi _{c_{\text{start}},c_{\text{accept}},T}$ \ $displaystyle \phi$ _ ${c_{\text{start}}$ 에 있는지 $여부$ 에 대한 $\phi _{c_{\text{start}},c_{\text{accept}},T}$ 질문으로 이미 줄였습니다. $T$ 즉 f $)\displaystyle$ f $(w$ 는 TQBF에 있습니다.이 증명의 나머지는 f가 다항식 시간으로 계산될 수 있다는 $것$ 을 증명한다.

t $t=1$ $({displaystyle$ t $=1$ 의 경우 $\phi _{c_{1},c_{2},t}$ $\phi _{c_{1},c_{2},t}$ t $(\displaystyle \phi$ _ ${c_{1}, c_{2$ }})의 $\phi _{c_{1},c_{2},t}$ 연산은 간단하며, 어느 하나의 구성이 다른 설정으로 변경되거나 변경되지 않습니다.우리의 공식이 나타내는 튜링 기계는 결정론적이기 때문에, 이것은 문제가 없다.

t $t>1$ > $t>1$ { $displaystyle$ $\phi _{c_{1},c_{2},t}$ t $> 1$ } $t>1$ 、 $\phi _{c_{1},c_{2},t}$ $\phi _{c_{1},c_{2},t}$ t { \ $displaystyle$ \ $phi$ _ ${$ c _ { c _ { 1} , c $_$ {2 $}$ }의 $\phi _{c_{1},c_{2},t}$ 계산에는 이른바 "중간점" $m_{1}$ { $displaystyle m$ _ { $1$ 을 찾는 재귀적 평가가 포함됩니다.이 경우 수식은 다음과 같이 고쳐 씁니다.

\displaystyle \phi _{1},c_{2},t}=\display m_{1}(\phi _{c_{1},m_{1},\lceil t/2\rceil}\display \phi _{1},c_{2},\lceil t/2\rceil}).}

이것에 의해, $({$ 1 $c_{1}$ })이 $c_{2}$ 으로 $c_{2}$ ({ $displaystyle$ $c_$ ${$ 2 $c_{2}$ })에 도달할 수 있는가 하는 질문이, $c_{2}$ $({$ $displaystyle$ $c_$ ${1$ $})$ 이 $c_{1}$ t $t/2$ $({$ t $/2})$ 으로 $t/2$ $m_{1}$ m1({ $displaystyle$ m_1 $})$ 에 $m_{1}$ $c_{2}$ 할 수 $c_{1}$ 하는 질문으로 변환됩니다. $ystyle c_{2}}:$ t $c_{2}$ $t/2$ / $t/2$ \ $displaystyle t$ /2 $t/2$ y y 。후자의 질문에 대한 답은 물론 전자에 대한 답을 준다.

이제 t는 입력 길이에서 지수적(따라서 다항식이 아님)인 T에 의해서만 경계가 됩니다.또한 각 재귀 레이어는 공식의 길이를 사실상 두 배로 늘립니다( $m_{1}$ $m_{1}$ ${$ $displaystyle m_{1}$ }은 $m_{1}$ 중간점 1개뿐입니다.t가 클수록 중간에 더 많은 스톱이 있습니다. $\phi _{c_{1},c_{2},t}$ c $\phi _{c_{1},c_{2},t}$ , $\phi _{c_{1},c_{2},t}$ , $(\$ _ ${c_{1}, c_{2}, t$ })를 $\phi_{c_1,c_2,t}$ 재귀적으로 평가하는 데 필요한 시간도 기하급수적으로 증가할 수 있습니다.단, 수식이 기하급수적으로 커질 수 있기 때문입니다.이 문제는 변수 $(\$ 및 $c_{3}$ $c_{4}$ c4 $(\$ 를 $c_4$ 사용하여 설정 쌍 $\{(c_{1},m_{1}),(m_{1},c_{2})\}$ 예를 $\{(c_{1},m_{1}),(m_{1},c_{2})\}$ { ( $\{(c_{1},m_{1}),(m_{1},c_{2})\}$ $\{(c_{1},m_{1}),(m_{1},c_{2})\}$ , $\{(c_{1},m_{1}),(m_{1},c_{2})\}$ ) $\{(c_{1},m_{1}),(m_{1},c_{2})\}$ } $\{(c_{1},m_{1}),(m_{1},c_{2})\}$ { $displaystyle$ \ { $c$ c {2} $\{(c_{1},m_{1}),(m_{1},c_{2})\}$ } )를 사용하여 공통적으로 수량화함으로써 해결됩니다.이러한 값은 다음과 같습니다.재귀 레이어로 이동합니다. $\phi _{c_{1},c_{2},t}$ 를 통해 c $\phi _{c_{1},c_{2},t}$ 1, $\phi _{c_{1},c_{2},t}$ 2, $\phi _{c_{1},c_{2},t}$ t {\ $displaystyle \phi$ _ ${c_{1}, c_{2}, t$ 의 해석이 다음과 같습니다.

\phi_{c_{1},c_{2},t}m_{1}\forall(c_{3},c_{4})\in \ᆯ(\phi_{c_{3},c_{4},\lceil t/2\rceil})=\exists.

이후의 어느 한 인스턴스를 다항 시간에서 계산할 수 있는 공식의 이 버전 실제로 다항 시간에, 계산할 수 있다.그 보편적으로 정량화된 주문했다 한쌍은 그저(c3c4){\displaystyle(c_{3},c_{4})}중 선택될 때,ϕ c1c2, t⟺ c3c4, ⌈ t/2⌉{\displaystyle \phi_{c_{1},c_{2},t}ϕ \iff\phi _{c_{3},c_{4},\lceil t/2\rceil}}우리에게 말해 준다.

따라서, ∀ L∈ PSPACE, L≤ pTQBF{\displaystyle\forall L\in{\mathsf{PSPACE}}}, 그렇게 TQBF은 PSPACE-hard _{p}\mathrm{TQBF},L\leq.함께 TQBF PSPACE에 위의 결과에, 이다는 증거를 TQBF은PSPACE-complete 언어를 완성시켰다.

(이 증거. Sipser 2006년을 대신하여 서명함 310–313 모든 본질적으로는 따른다.Papadimitriou 1994년 또한.)증거를 포함한다.

잡동사니

TQBF에서 중요한 하위 문제 중 하나는 부울 만족도 문제입니다.이 문제에서는 변수를 할당하여 특정 부울 공식 $"\displaystyle\phi"$ 를 $\phi$ 실현할 수 있는지 여부를 확인합니다.이는 기존 수량자만 사용하는 TQBF와 동일합니다. $\displaystyle \cdots x_{1}\cdots \cdots x_{n}\phi(x_{1},\ldots,x_{n})}$ 이는 NTM(Non-deterministic Turing machine)에 의해 받아들여진 언어의 증명에 대한 다항식 시간 검증자가 증명을 저장하기 위해 다항식 공간을 필요로 한다는 관찰로부터 직접 이어지는 더 큰 결과 NP p PSPACE의 한 예이다.
다항식 계층(PH)의 모든 클래스에는 어려운 문제로 TQBF가 있습니다.즉, 폴리타임 TM V가 존재하는 모든 언어 L을 포함하는 클래스에 대해 모든 입력 x 및 일부 상수 i에 대해 다음과 같이 검증한다. $\displaystyle x\in L\왼쪽 화살표\forall y_{2}\cdots Q_{i}y_{i}\V(x,y_{1},y_{2},\dots,y_{i}\=1}$ 특정 QBF 배합은 다음과 같이 지정됩니다. $\displaystyle \phi }$ $x$ x $\exists {\vec {x_{1}}}\forall {\vec {x_{2}}}\cdots Q_{i}{\vec {x_{i}}}\ \phi ({\vec {x_{1}}},{\vec {x_{2}}},\dots ,{\vec {x_{i}}})\ =\ 1$ $\exists {\vec {x_{1}}}\forall {\vec {x_{2}}}\cdots Q_{i}{\vec {x_{i}}}\ \phi ({\vec {x_{1}}},{\vec {x_{2}}},\dots ,{\vec {x_{i}}})\ =\ 1$ $\exists {\vec {x_{1}}}\forall {\vec {x_{2}}}\cdots Q_{i}{\vec {x_{i}}}\ \phi ({\vec {x_{1}}},{\vec {x_{2}}},\dots ,{\vec {x_{i}}})\ =\ 1$ $\exists {\vec {x_{1}}}\forall {\vec {x_{2}}}\cdots Q_{i}{\vec {x_{i}}}\ \phi ({\vec {x_{1}}},{\vec {x_{2}}},\dots ,{\vec {x_{i}}})\ =\ 1$ 2 $\exists {\vec {x_{1}}}\forall {\vec {x_{2}}}\cdots Q_{i}{\vec {x_{i}}}\ \phi ({\vec {x_{1}}},{\vec {x_{2}}},\dots ,{\vec {x_{i}}})\ =\ 1$ $\exists {\vec {x_{1}}}\forall {\vec {x_{2}}}\cdots Q_{i}{\vec {x_{i}}}\ \phi ({\vec {x_{1}}},{\vec {x_{2}}},\dots ,{\vec {x_{i}}})\ =\ 1$ $\exists {\vec {x_{1}}}\forall {\vec {x_{2}}}\cdots Q_{i}{\vec {x_{i}}}\ \phi ({\vec {x_{1}}},{\vec {x_{2}}},\dots ,{\vec {x_{i}}})\ =\ 1$ i $\exists {\vec {x_{1}}}\forall {\vec {x_{2}}}\cdots Q_{i}{\vec {x_{i}}}\ \phi ({\vec {x_{1}}},{\vec {x_{2}}},\dots ,{\vec {x_{i}}})\ =\ 1$ ( ( $\exists {\vec {x_{1}}}\forall {\vec {x_{2}}}\cdots Q_{i}{\vec {x_{i}}}\ \phi ({\vec {x_{1}}},{\vec {x_{2}}},\dots ,{\vec {x_{i}}})\ =\ 1$ $\exists {\vec {x_{1}}}\forall {\vec {x_{2}}}\cdots Q_{i}{\vec {x_{i}}}\ \phi ({\vec {x_{1}}},{\vec {x_{2}}},\dots ,{\vec {x_{i}}})\ =\ 1$ , $\exists {\vec {x_{1}}}\forall {\vec {x_{2}}}\cdots Q_{i}{\vec {x_{i}}}\ \phi ({\vec {x_{1}}},{\vec {x_{2}}},\dots ,{\vec {x_{i}}})\ =\ 1$ 2 $\exists {\vec {x_{1}}}\forall {\vec {x_{2}}}\cdots Q_{i}{\vec {x_{i}}}\ \phi ({\vec {x_{1}}},{\vec {x_{2}}},\dots ,{\vec {x_{i}}})\ =\ 1$ , ... , $\exists {\vec {x_{1}}}\forall {\vec {x_{2}}}\cdots Q_{i}{\vec {x_{i}}}\ \phi ({\vec {x_{1}}},{\vec {x_{2}}},\dots ,{\vec {x_{i}}})\ =\ 1$ i $\exists {\vec {x_{1}}}\forall {\vec {x_{2}}}\cdots Q_{i}{\vec {x_{i}}}\ \phi ({\vec {x_{1}}},{\vec {x_{2}}},\dots ,{\vec {x_{i}}})\ =\ 1$ ) $\exists {\vec {x_{1}}}\forall {\vec {x_{2}}}\cdots Q_{i}{\vec {x_{i}}}\ \phi ({\vec {x_{1}}},{\vec {x_{2}}},\dots ,{\vec {x_{i}}})\ =\ 1$ (\ $displaystyle \ vec$ { $x _$ { { 1} } \ $cdots Q_i$ } { \ $ph ）$ 。 $yle {vec {x_{i$ 는 부울 변수의 벡터입니다.
TQBF 언어는 진정한 정량화된 부울 공식의 집합으로 정의되지만, 약어 TQBF는 종종 완전히 정량화된 부울 공식(단순히 "완전" 또는 "정량화된" 것으로 이해되는 QBF)을 나타내기 위해 사용됩니다.문헌을 읽을 때 약어 TQBF의 두 가지 사용을 맥락적으로 구별하는 것이 중요하다.
TQBF는 두 플레이어 간에 번갈아 가면서 진행되는 게임이라고 생각할 수 있습니다.존재 수량화된 변수는 플레이어가 턴할 때 이동이 가능하다는 개념과 동일합니다.보편적으로 수량화된 변수는 게임의 결과가 플레이어가 그 턴에서 어떤 움직임을 취하느냐에 따라 달라지지 않는다는 것을 의미합니다.또, 제1의 정량자가 실재하는 TQBF는, 제1의 플레이어가 승리 전략을 가지는 공식 게임에 대응한다.
정량화된 공식이 2-CNF인 TQBF는 그 함축 그래프의 강한 접속성 해석을 수반하는 알고리즘에 의해 선형 시간 내에 풀릴 수 있다.2-만족도 문제는 이러한 공식에 대한 TQBF의 특수한 경우로, 모든 수량화자는 ^[17]^[18]실재합니다.
Hubie ^[19]Chen에 의한 설명서에 제시된 정량화된 부울 공식의 제한된 버전에 대한 체계적인 처리가 있다.
평면 SAT를 일반화한 평면 TQBF는 D에 의해 PSPACE-완전성이 입증되었다.리히텐슈타인^[20]

주 및 참고 자료

^ M. Garey & D. Johnson (1979). Computers and Intractability: A Guide to the Theory of NP-Completeness. W. H. Freeman, San Francisco, California. ISBN 0-7167-1045-5.
^ A. Chandra, D. Kozen, and L. Stockmeyer (1981). "Alternation". Journal of the ACM. 28 (1): 114–133. doi:10.1145/322234.322243.{{cite journal}}: CS1 maint: 여러 이름: 작성자 목록(링크)
^ Adi Shamir (1992). "Ip = Pspace". Journal of the ACM. 39 (4): 869–877. doi:10.1145/146585.146609. S2CID 315182.
^ Arora, Sanjeev; Barak, Boaz (2009), "Space complexity", Computational Complexity, Cambridge: Cambridge University Press, pp. 78–94, doi:10.1017/cbo9780511804090.007, ISBN 978-0-511-80409-0, retrieved 2021-05-26
^ ^a ^b ^c "QBFEVAL Home Page". www.qbflib.org. Retrieved 2021-02-13.
^ ^a ^b ^c "QBF Solvers Beyond NP". beyondnp.org. Retrieved 2021-02-13.
^ ^a ^b Balabanov, Valeriy; Roland Jiang, Jie-Hong; Scholl, Christoph; Mishchenko, Alan; K. Brayton, Robert (2016). "2QBF: Challenges and Solutions" (PDF). International Conference on Theory and Applications of Satisfiability Testing: 453–459. Archived (PDF) from the original on 13 February 2021 – via SpringerLink.
^ ^a ^b "QBFEVAL'20". www.qbflib.org. Retrieved 2021-05-29.
^ ^a ^b ^c ^d ^e ^f ^g ^h ⁱ Lonsing, Florian (December 2017). "An Introduction to QBF Solving" (PDF). www.florianlonsing.com. Retrieved 29 May 2021.{{cite web}}: CS1 maint :url-status (링크)
^ Rabe, Markus N. (2021-04-15), MarkusRabe/cadet, retrieved 2021-05-06
^ Tentrup, Leander (2021-05-06), ltentrup/caqe, retrieved 2021-05-06
^ "DepQBF Solver". lonsing.github.io. Retrieved 2021-05-06.
^ "sKizzo - a QBF solver". www.skizzo.site. Retrieved 2021-05-06.
^ ^a ^b ^c ^d Shukla, Ankit; Biere, Armin; Seidl, Martina; Pulina, Luca (2019). A Survey on Applications of Quantified Boolean Formulas (PDF). 2019 IEEE 31st International Conference on Tools for Artificial Intelligence. pp. 78–84. doi:10.1109/ICTAI.2019.00020. Retrieved 29 May 2021.
^ Shen, Zhihe. Using QBF Solvers to Solve Games and Puzzles (PDF) (Thesis). Boston College.
^ ^a ^b Janota, Mikoláš; Marques-Silva, Joao (2011). On Deciding MUS Membership with QBF. Principles and Practice of Constraint Programming – CP 2011. Vol. 6876. pp. 414–428. doi:10.1007/978-3-642-23786-7_32. ISBN 978-3-642-23786-7.
^ 를 클릭합니다Krom, Melven R. (1967). "The Decision Problem for a Class of First-Order Formulas in Which all Disjunctions are Binary". Zeitschrift für Mathematische Logik und Grundlagen der Mathematik. 13 (1–2): 15–20. doi:10.1002/malq.19670130104..
^ 를 클릭합니다Aspvall, Bengt; Plass, Michael F.; Tarjan, Robert E. (1979). "A linear-time algorithm for testing the truth of certain quantified boolean formulas" (PDF). Information Processing Letters. 8 (3): 121–123. doi:10.1016/0020-0190(79)90002-4..
^ Chen, Hubie (December 2009). "A Rendezvous of Logic, Complexity, and Algebra". ACM Computing Surveys. ACM. 42 (1): 1–32. arXiv:cs/0611018. doi:10.1145/1592451.1592453. S2CID 11975818.
^ Lichtenstein, David (1982-05-01). "Planar Formulae and Their Uses". SIAM Journal on Computing. 11 (2): 329–343. doi:10.1137/0211025. ISSN 0097-5397.

Portnow & Homer(2003)는 PSPACE 및 TQBF의 역사적 배경을 제공합니다.
Zhang(2003)은 부울 공식의 역사적 배경을 제공한다.
아로라, 산지예프(2001).COS 522: 계산의 복잡성.프린스턴 대학의 강의 노트입니다.2005년 10월 10일 취득.
포트나우, 랜스, 스티브 호머(2003년 6월).계산 복잡성의 짧은 역사.계산 복잡도 열, 80.2005년 10월 9일 취득.
파파디미트리우, C. H. (1994)계산의 복잡성읽기:애디슨 웨슬리.
시퍼, 마이클(2006).계산 이론의 입문보스턴:Thomson 코스 테크놀로지.
장, 린타오.(2003).진실을 찾는 중: 부울 공식을 만족시키기 위한 기술입니다.2005년 10월 10일 취득.

「」를 참조해 주세요.

SAT가 NP-완전임을 나타내는 쿡-레빈 정리
일반 지리학

외부 링크

정량화된 부울 공식 라이브러리(QBFLIB)
정량화된 부울 공식에 관한 국제 워크숍

[1] M. Garey & D. Johnson (1979). Computers and Intractability: A Guide to the Theory of NP-Completeness. W. H. Freeman, San Francisco, California. ISBN 0-7167-1045-5.

[2] A. Chandra, D. Kozen, and L. Stockmeyer (1981). "Alternation". Journal of the ACM. 28 (1): 114–133. doi:10.1145/322234.322243.{{cite journal}}: CS1 maint: 여러 이름: 작성자 목록(링크)

[3] Adi Shamir (1992). "Ip = Pspace". Journal of the ACM. 39 (4): 869–877. doi:10.1145/146585.146609. S2CID 315182.

[4] Arora, Sanjeev; Barak, Boaz (2009), "Space complexity", Computational Complexity, Cambridge: Cambridge University Press, pp. 78–94, doi:10.1017/cbo9780511804090.007, ISBN 978-0-511-80409-0, retrieved 2021-05-26

[:0-5] "QBFEVAL Home Page". www.qbflib.org. Retrieved 2021-02-13.

[:1-6] "QBF Solvers Beyond NP". beyondnp.org. Retrieved 2021-02-13.

[:2-7] Balabanov, Valeriy; Roland Jiang, Jie-Hong; Scholl, Christoph; Mishchenko, Alan; K. Brayton, Robert (2016). "2QBF: Challenges and Solutions" (PDF). International Conference on Theory and Applications of Satisfiability Testing: 453–459. Archived (PDF) from the original on 13 February 2021 – via SpringerLink.

[:3-8] "QBFEVAL'20". www.qbflib.org. Retrieved 2021-05-29.

[:4-9] ^ ^a ^b ^c ^d ^e ^f ^g ^h ⁱ Lonsing, Florian (December 2017). "An Introduction to QBF Solving" (PDF). www.florianlonsing.com. Retrieved 29 May 2021.{{cite web}}: CS1 maint :url-status (링크)

[10] Rabe, Markus N. (2021-04-15), MarkusRabe/cadet, retrieved 2021-05-06

[11] Tentrup, Leander (2021-05-06), ltentrup/caqe, retrieved 2021-05-06

[12] "DepQBF Solver". lonsing.github.io. Retrieved 2021-05-06.

[13] "sKizzo - a QBF solver". www.skizzo.site. Retrieved 2021-05-06.

[:5-14] Shukla, Ankit; Biere, Armin; Seidl, Martina; Pulina, Luca (2019). A Survey on Applications of Quantified Boolean Formulas (PDF). 2019 IEEE 31st International Conference on Tools for Artificial Intelligence. pp. 78–84. doi:10.1109/ICTAI.2019.00020. Retrieved 29 May 2021.

[15] Shen, Zhihe. Using QBF Solvers to Solve Games and Puzzles (PDF) (Thesis). Boston College.

[:6-16] Janota, Mikoláš; Marques-Silva, Joao (2011). On Deciding MUS Membership with QBF. Principles and Practice of Constraint Programming – CP 2011. Vol. 6876. pp. 414–428. doi:10.1007/978-3-642-23786-7_32. ISBN 978-3-642-23786-7.

[17] 를 클릭합니다Krom, Melven R. (1967). "The Decision Problem for a Class of First-Order Formulas in Which all Disjunctions are Binary". Zeitschrift für Mathematische Logik und Grundlagen der Mathematik. 13 (1–2): 15–20. doi:10.1002/malq.19670130104..

[18] 를 클릭합니다Aspvall, Bengt; Plass, Michael F.; Tarjan, Robert E. (1979). "A linear-time algorithm for testing the truth of certain quantified boolean formulas" (PDF). Information Processing Letters. 8 (3): 121–123. doi:10.1016/0020-0190(79)90002-4..

[19] Chen, Hubie (December 2009). "A Rendezvous of Logic, Complexity, and Algebra". ACM Computing Surveys. ACM. 42 (1): 1–32. arXiv:cs/0611018. doi:10.1145/1592451.1592453. S2CID 11975818.

[20] Lichtenstein, David (1982-05-01). "Planar Formulae and Their Uses". SIAM Journal on Computing. 11 (2): 329–343. doi:10.1137/0211025. ISSN 0097-5397.

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]

[12]

[13]

[14]

[15]

[16]

[17]

[18]

[19]

[20]

Search

참 수량화된 부울 공식

네임스페이스

더

목차

개요

프리넥스 정규형

QBF 솔러

순진한

최첨단

적용들

내선번호

PSPACE 완전성

잡동사니

주 및 참고 자료

「」를 참조해 주세요.

외부 링크

Search

참 수량화된 부울 공식

개요

프리넥스 정규형

QBF 솔러

순진한

최첨단

적용들

내선번호

PSPACE 완전성

잡동사니

주 및 참고 자료

「 」를 참조해 주세요.

외부 링크

「」를 참조해 주세요.