TQBF Problemi

**Boolean Formülü** içerisinde; boolean değişkenleri, sabitler {0,1} ve işlemler {\land,  \lor,  \lnot} içeren formüllerdir. Bu formüller,  \forall (bütün hepsi) ve   \exists (en az bir) belirleyicilerinin eklenmesiyle daha genel bir yapıya sokulabilir.  \forall x Q  ifadesi bütün *x* değişkenleri için *Q* formülü doğrudur anlamı taşımaktadır. Benzer bir şekilde; \exists x Q  ifadesi ise bazı *x* değişkenleri için *Q* formülü doğrudur anlamı taşımaktadır.

Örnek olarak, doğal sayılar kümesinde \forall x |x+1 > x |  ifadesi doğrudur. Çünkü, bütün doğal sayıların bir fazlası sayının kendisinden büyüktür. Fakat, \exists y |y + y = 3|  ifadesi doğal sayılar kümesi için yanlıştır. Çünkü; hiçbir doğal sayının iki katı 3'e eşit değildir. Ancak biz örek uzay olarak doğal sayıları değil de gerçek sayılar alınsaydı bu ifade doğru olurdu.

Boolean formüllerin belirleyicilerle gösterilmesine, *belirleyici boolean formülü* denir. Burada kullanılan uzay {0,1} den oluşur. Örnek olarak:

Q=\forall x  \exists y [(x \lor y) \land (\lnot x \lor \lnot y)]
ifadesi bir *belirleyici boolean formül* dür. Burada *Q* ifadesi doğrudur. Fakat; \forall x  ile \exists y ifadeleri yer değiştirseydi *Q* yanlış olurdu.

Eğer bir *belirleyici boolean formülde* bütün değişken isimleri belirleyici listesinde yer alırsa buna *tamamen belirlenmiş boolean formül* denir. *Tamamen Belirlenmiş Boolean Formüllere* cümle denir ve formülü işleme sokarsak daima doğru ya da yanlış sonuç üretir. Yukarıdaki örnek bir *tamamen belirlenmiş boolean formüldür*. Çünkü, bütün değişkenler (*x*,*y*) belirleyici olarak yer alır. Eğer \forall x ifadesini çıkarsaydık, yukarıdaki örnek *tamamen belirlenmiş boolean formül* olmazdı.

## Problem Tanımı
TQBF problemi bir *tamamen belirlenmiş boolen formül* ün doğru ya da yanlış olduğunu belirleyebilmektir. Bunun için şöyle bir dil tanımlanır.

TQBF={ | Q bir doğru olan tamamen belirlenmiş boolen formül }

## Teori
TQBF PSPACE-complete'dir.

## Çözüm Önerisi
TQBF'in bir PSPACE-Complete olduğunu göstermek için, cümle içindeki değişkenlere değer atan bir formül bulup tekrarlayan bir şekilde değişken değerlerini inceleyip formülün doğru ya da yanlış olacağı bulunur.

PSPACE de tanımlı bütün A dillerinin TQBF e indirgendiğini göstermek için, polinomial yer ile sınırlı A ya ait bir Turing makinesi ile başlayacağız. Daha sonra, boolean formül ile kodlanarak ve A diline ait makina ile çalışacak bir kelime ile polynomial zamana indirgemeye çalışacağız. Şöyle ki, formül ancak ve ancak makina gönderilen kelimeyi kabul ederse doğru olacak.

Burada formülü oluştutmak için Savitch Teoremi kullanacağız. Yaratılacak yeni formül, ana formülü parçalara bölecek ve her bir belirleyiciyi formülde yerine koyarak daha küçük formüller yaratacak.

## Çözüm
TQBF i belirleyen bir polinomsal yer algoritması oluşturacağız.

T=  verisini kullanan bir *tamamen belirlenmiş boolean formül*.

# *Q* hiç belirleyici içemiyorsa, bu durumda *Q* sadece sabitlerden oluşur. *Q* yu işleriz eğer doğruysa kabul et. Yoksa reddet.
# Eğer Q = \exists x G ye eşitse, tekrarlarla *T* yi *G* üzerinde çalıştır. Önce x değişkeni yerine 0 koy, daha sonra da x değişkeni yerine 1 koy. Eğer iki sonuçtan biri doğruysa kabul et yoksa reddet.
# Eğer Q = \forall x G ye eşitse, tekrarlarla *T* yi *Q* üzerinde çağır. Önce x değişkeni için 0 koy sonra 1 koy. Eğer iki sonuçta doğruysa kabul et yoksa reddet.

T algoritması TQBF i belirler.

Bu algoritmanın yer karmaşıklığını analiz ettiğimizde şunu gözlemleriz: Formül, içerisindeki değişken sayısı kadar çağrılır. Her seviyede sadece bir değişken değerini tutarız. Bu yüzden toplam kullanılacak yer O(m), m = toplam değişken sayısı, dır. Buradan *T* nin Lineer zamanda bittiğini gözlemleriz.

A, M Turing Makinesi tarafından n^k polinomsal yerde tanımlanan bir dil olsun. Şimdi A'dan TQBF e Polinomsal zaman indirgemeye çalışacağız. Bu indirgeme için bir 'w' kelimesi kullanılsın. Söyle ki; *Q* ancak, M makinası 'w' yi kabul ettiğinde doğru olsun.

*Q* yu nasıl oluşturacağımızı göstermek için daha genel bir problemi çözülür. c1 ve c2 iki tane değişken listesi olsun. ve t>0 olan bir sayı. Öncelikle Qc1,c2,t formülü kurarız. Eğer c1 ve c2 yi doğru bir şekilde kurarsak; formül, M makinası c1 den c2 ye en fazla t stepte giderse doğru olur. Bu durumda, Qcstart,caccept,h, h=2^df(n) alırız. Böylece *M* *n* verisi üzerinde en fazla 2^df(n) değişik konfigürasyona sahip olur. Burada f(n)=n^k ve *t* 2 nin katı olacak şekilde alalım.

Eğer t=1 ise, Qc1,c2,t kolayca oluşturulabilir. Böyle bir durumda, ya c1 c2 ye eşittir ya da c1 den c2 ye M makinasında bir step vardır.

Eğer t>1 ise, Qc1,c2,t formülü tekrarlarla kurulur. Şöyle ki:

Qc1,c2,t = \existsm1[
Qc1,m1,t/2\landQm1,c2,t/2 ]

m1 bu arada *M* ye ait bir konfigurasyonu temsil eder. \existsm1: \exists x1,......,xl in kısaca yazılmış halidir. l=O(n^k) ve x1,.....,xl m1 yi kodlayan değişkenlerdir. 
Qc1,c2,t nin yaratılması şunu belirtir: M makinası c1 den c2 ye en fazla t stepte gider. Ve eğer m1 ara stepi varsa, şöyle ki M c1 den m1 e t/2 stepte gidsin ve m1 dan c2 e t/2 stepde gidsin. Bu durumda, Qc1,m1,t/2 ve Qm1,c2,t/2 formülleri oluşturulabilir. Fakat bu şekilde genel formülü çıkarmaya kalkarsak, çıkacak formül çok uzun olur. Çünkü, her tekrarda biz formülü 2'ye bölüyoruz. Ve her step geçtikten sonra genel formül 2 ye katalanıyor. Başlangıçta t=2^df(n) aldığımız için exponential bir formül ortaya çıkar.

Formülün boyutunu kısaltmak için \exists in yanına bir de \forall ekleriz. Şöyle ki:

Qc1,c2,t = \existsm1 \forall (c3,c4) \in {(c1,m1), (m1,c2)} [Qc3,c4,t/2]

Yeni değikenlerin eklenmesi, iki tekrarlayan formülü teke indirdi. \forall (c3,c4) \in {(c1,m1), (m1,c2)} ifadesiyle, c3 ve c4 değişkenleri sırasıyla c1,m1 veya m1,c2 değerleri alabilir. Ve Qc3,c4,t/2] her iki durumda da doğrudur.

Qcstart,caccept,h, h=2^df(n) nin uzunluğunu hesaplarken şunu söyleyebiliriz: tekrarlayan her step genel formüle bir eleman ekler bu yüzden formülün tamamı lineer uzunluktadır.

Toplam uzunluk ise:O(f(n)) dır. Tekrarlardaki step sayısı: log(2^df(n)), O(f(n)) dır. Bu yüzden sonuç formülü: Of^2(n) dır.

## Kaynakça
* Michael Sipser: "Introduction to the Theory of Computation" Course Technology Press Second Edition, 2005.