Türkçe Bilgi logo TürkçeBilgi

Tqbf Problemi

Kısaca: 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şke ...devamı ☟

Boolean Formülü içerisinde; boolean değişkenleri, sabitler ve işlemler 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 den oluşur. Örnek olarak: Q=\forall x \exists y \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= 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 sonrada 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 sadace 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. Şöyleki: Qc1,c2,t = \existsm1 Qc1,m1,t/2\landQm1,c2,t/2 m1 buarada 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, şöyleki 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 birde \forall ekleriz.Şöyleki: Qc1,c2,t = \existsm1 \forall (c3,c4) \in [1] Yeni değikenlerin eklenmesi, iki tekrarlayan formülü teke indirdi. \forall (c3,c4) \in 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. * Michael Sipser: "Introduction to the Theory of Computation" Course Technology Press Second Edition, 2005.

Kaynaklar

Vikipedi

Bu konuda henüz görüş yok.
Görüş/mesaj gerekli.
Markdown kullanılabilir.