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 xQ$ ifadesi bütün x değişkenleri için Q formülü doğrudur anlamı taşımaktadır. Benzer bir şekilde; $\exists xQ$ 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.

1. Q hiç belirleyici içemiyorsa, bu durumda Q sadece sabitlerden oluşur. Q yu işleriz eğer doğruysa kabul et. Yoksa reddet.
2. Eğer $Q=\exists xG$ 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.
3. Eğer $Q=\forall xG$ 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. c₁ ve c₂ iki tane değişken listesi olsun. ve t>0 olan bir sayı. Öncelikle Q_c1,c2,t formülü kurarız. Eğer c₁ ve c₂ yi doğru bir şekilde kurarsak; formül, M makinası c₁ den c₂ ye en fazla t stepte giderse doğru olur. Bu durumda, Q_{cstart,caccept,h}, $h=2^{d}f(n)$ alırız. Böylece M n verisi üzerinde en fazla $2^{d}f(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, Q_c1,c2,t kolayca oluşturulabilir. Böyle bir durumda, ya c₁ c₂ ye eşittir ya da c₁ den c₂ ye M makinasında bir step vardır.

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

Q_c1,c2,t = $\exists$m₁[ Q_c1,m1,t/2$\land$Q_m1,c2,t/2 ]

m₁ bu arada M ye ait bir konfigurasyonu temsil eder. $\exists$m₁: $\exists$ x₁,......,x_l in kısaca yazılmış halidir. $l=O(n^{k})$ ve x₁,.....,x_l m₁ yi kodlayan değişkenlerdir. Q_c1,c2,t nin yaratılması şunu belirtir: M makinası c₁ den c₂ ye en fazla t stepte gider. Ve eğer m₁ ara stepi varsa, şöyle ki M c₁ den m₁ e t/2 stepte gidsin ve m₁ dan c₂ e t/2 stepde gidsin. Bu durumda, Q_c1,m1,t/2 ve Q_m1,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^{d}f(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:

Q_c1,c2,t = $\exists$m₁ $\forall$ (c₃,c₄) $\in$ {(c₁,m₁), (m₁,c₂)} [Q_c3,c4,t/2]

Yeni değikenlerin eklenmesi, iki tekrarlayan formülü teke indirdi. $\forall$ (c₃,c₄) $\in$ {(c₁,m₁), (m₁,c₂)} ifadesiyle, c₃ ve c₄ değişkenleri sırasıyla c₁,m₁ veya m₁,c₂ değerleri alabilir. Ve Q_c3,c4,t/2] her iki durumda da doğrudur.

Q_{cstart,caccept,h}, $h=2^{d}f(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^{d}f(n)$), $O(f(n))$ dır. Bu yüzden sonuç formülü: O$f^{2}(n)$ dır.

Kaynakça

• Michael Sipser: "Introduction to the Theory of Computation" Course Technology Press Second Edition, 2005.