TQBF

בתורת הסיבוכיות, השפה TQBF (קיצור ל-True quantified boolean formulas; או: QBF, QSAT) היא שפה פורמלית במחלקה PSPACE. השפה TQBF היא השפה של כל הנוסחות הבוליאניות עם כמתים שמוערכות לאמת. ניתן לראות את TQBF כהכללה ל-SAT. השפה ידועה בהיותה שפה PSPACE-Complete, כלומר לכל שפה ב-PSPACE קיימת רדוקציה פולינומית ל-TQBF.

בניגוד ל-SAT בה השאלה היא האם קיימת הצבת אמת, ב-TQBF לכל נוסחה יש ערך אמת או שקר יחיד, מכיוון שאין משתנים חופשיים.

הסבר - נוסחת SAT נראית כך:

$(x_{1}\lor x_{2})\land (\neg x_{1}\lor x_{3})$

ועבור ההצבה $x_{1}=T,x_{2}=F,x_{3}=T$ הנוסחה מקבלת ערך אמת בעוד עבור $x_{1}=F,x_{2}=F,x_{3}=T$ הנוסחה מקבלת ערך שקר.

הנוסחה השקולה ב-QBF נראית כך:

$\exists x_{1}\exists x_{2}\exists x_{3}((x_{1}\lor x_{2})\land (\neg x_{1}\lor x_{3}))$

וערכה הוא אמת, מכיוון שקיימים $x_{1},x_{2},x_{3}$ עבורם יש הצבות אמת.

ניתן לחשוב על TQBF כעל משחק בין שני שחקנים, המשחקים בתורות. משתנים המופיעים בנוסחה עם כמת "קיים" תואמים לקיום מהלך עבור שחקן בתור כלשהו, ומשתנים המופיעים בנוסחה עם כמת "לכל" תואמים לכך שתוצאת המשחק אינה תלויה במהלך ששחקן מבצע (כלומר, כל מהלך יכול להוביל לניצחון). נוסחת TQBF שהכמת הראשון בה הוא "קיים" תואמת לנוסחת משחק בה לשחקן הראשון אסטרטגיה מנצחת (כיוון שקיים מהלך של השחקן עבורו לכל מהלך אחר של היריב, השחקן ינצח).

סקירה

בתורת הסיבוכיות, השפה QBF היא הכללה של השפה SAT בה לכל משתנה מוצמד כמת. מכיוון ש-QBF נמצאת ב-PSPACE, אין חובה לכתוב את הנוסחאות בצורת CNF מכיוון שזה ודאי לא הופך את השפה ל"קלה" יותר, אך גם לא הופך אותה לקשה יותר. מאחר שלכל משתנה מוצמד כמת, לנוסחה יש ערך אמת או שקר, והשפה QBF היא של הנוסחאות שמקבלות ערך אמת. פורמלית : $QBF=\{\phi \ |\ \phi {\text{ is a quantified boolean formula that evaluates to true}}\}$ דוגמה:

$\psi =\forall x_{1}\exists x_{2}\exists x_{3}(x_{1}\land x_{2}\land \neg x_{3})\lor x1\lor (\neg x_{1}\land x_{2}\land x_{3})$

מתקיים $\psi \in QBF$.

QBF היא בעיה שלמה של המחלקה PSPACE, המחלקה של הבעיות הניתנות לפתרון על ידי מכונת טיורינג דטרמיניסטית או לא דטרמיניסטית בסיבוכיות מקום פולינומית וזמן שאינו מוגבל. נוסחה ב-QBF ניתנת לפתרון טריוויאלי המשתמש בסיבוכיות מקום ליניארית וסיבוכיות זמן אקספוננציאלית.

ההוכחה לתוצאה המפתיעה IP = PSPACE נעשתה על ידי הצגת הוכחה אינטראקטיבית ל-QBF.

ל-QBF מספר צורות נורמליות. אחת הצורות החשובות היא הצורה הנורמלית של פרנקס אם היא מהצורה

$\exists x_{1}\forall x_{2}\exists x_{3}...Q_{n}x_{n}\phi (x_{1},x_{2},...,x_{n}).$

הצורה הזאת חשובה במיוחד בגלל הקשר שלה להיררכיה הפולינומית. כידוע,

$PH=\bigcup _{i=_{1}}^{\infty }\Sigma _{i}=\bigcup _{i=_{1}}^{\infty }\Pi _{i}$

וגם המחלקה $\Sigma _{i}$ מוגדרת כל השפות A עבורן קיים מוודא פולינומי $V$ ופולינום $P(\cdot )$ כך ש-

$x\in A\iff \exists y_{1}\forall y_{2}\exists y_{3}...Q_{k}y_{k}:\forall 1\leq i\leq k.\ |y_{i}|\leq P(|x|),V(x,y_{1},y_{2},...,y_{k})=1$,

והנוסחה למעלה ניתנת לרדוקציה טריוויאלית ל-QBF.

PH ו-PSPACE

ההנחה הרווחת כיום היא ש $PH\not =PSPACE$, מכיוון שאם PH=PSPACE, אזי QBF נמצא באחת מדרגות ההיררכיה הפולינומית ולכן ההיררכיה קורסת בדרגה זאת, אף על פי שמקובל להניח שזה לא קורה.

פתירת QBF

ל-QBF פתרון טריוויאלי בסיבוכיות מקום ליניארית.

אלגוריתם לפתרון:

1. אם הנוסחה ריקה, החזר אמת.
2. עבור המשתנה הראשון x בנוסחה בצע:
   1. הצב T ב$x$
      1. פתור את הנוסחה והצב את התוצאה ב$y_{T}$
   2. הצב F ב$x$
      1. פתור את הנוסחה והצב את התוצאה ב$y_{F}$
3. אם הכמת של x הוא "לכל":
   1. החזר $y_{T}\land y_{F}$
4. אם הכמת של x הוא "קיים":
   1. החזר $y_{T}\lor y_{F}$

ניתוח סיבוכיות מקום: הפונקציה המתארת את סיבוכיות המקום של האלגוריתם היא $f(n)=1+f(n-1)=O(n)$, מכיוון שבזמן הקריאה הרקורסיבית, אנחנו שומרים כמות זיכרון קבועה. סיבוכיות הזמן היא אקספוננציאלית

שלמות של QBF

נרצה להראות שהשפה QBF שלמה ב-PSPACE תחת רדוקציית קארפ פולינומית, כלומר $\forall L\in PSPACE,\ \ \exists A,p(\cdot )\forall x{\text{ s.t. }}(A(x)\in QBF\iff x\in L)\land t(A(x))\leq p(|x|)$

או, בכתיב חסכני, $\forall L\in PSPACE,\ \ L\leq _{m}^{p}QBF$

לשם כך נגדיר ראשית את גרף הקונפיגורציות $G_{M}$ של מכונת טיורינג M:

גרף הקונפיגורציות של מכונת טיורינג M הוא גרף אשר כל קודקוד בו הוא קונפיגורציה של המכונה, ובין קודקוד לקודקוד יש קשת אם ורק אם ניתן להגיע מקונפיגורציה אחת לשנייה.

קונפיגורציה של מכונת טיורינג היא המצב הנוכחי של המכונה, דהיינו

1. תוכן סרט העבודה
2. מיקום המכונה על הסרט
3. מצב המכונה

נשים לב, שמכיוון שהמכונה שלנו פולינומית במקום, קונפיגורציה בודדת שלה היא גם פולינומית במקום.

קל לראות שאם קלט x נמצא בשפה אזי קיים מסלול בין המצב ההתחלתי שלו $C_{start}^{M,x}$ למצב המקבל שלו $C_{accpet}^{M,x}$.

נגדיר פונקציה $\psi (C,C')$, אשר מחזירה אמת אם ורק אם קיים מסלול בין C ל-C' בגרף.

ניסיון: נגדיר את הנוסחה באופן הבא: $\exists C_{start}^{M},\exists C_{1}\ldots \exists C_{accept}^{M}\ \ \psi (C_{start}^{M},C_{1}^{M})\land \ldots \land \psi (C_{n-1}^{M},C_{end}^{M})$-C'

הנוסחה הנ"ל באורך אקספוננציאלי. נגדיר פונקציה חדשה: $\psi _{i}(C,C')$ הוא אמת אם ורק קיים מסלול בין C ל-C' באורך לכל היותר $2^{i}$.

נשים לב שמתקיים: $\psi _{i+1}(C,C')=\exists C''\ \ \psi _{i}(C,C'')\land \psi _{i}(C'',C')$

משמעות הנוסחה למעלה: קיים מסלול בין $C$ ל-$C'$ אם ורק אם קיימת קונפיגורציה $C''$ כך שיש מסלול בין $C$ ל-$C''$ ובין $C''$ ל-$C'$.

הנוסחה עדיין אקספוננציאלית. נקצר אותה עם הכמת לכל.

$\psi _{i+1}(C,C')=\exists w\forall a\forall b\ \ (a=C\land b=w)\lor (a=w\land b=C')\implies \psi _{i}(a,b)$

הנוסחה הנ"ל שקולה בדיוק לנוסחה למעלה, אך היא גדלה בקצב פולינומי ולא אקספוננציאלי.

כעת, כאשר נפתח לפי הנוסחה הנ"ל, נקבל נוסחה בוליאנית עם כמתים שאורכה פולינומי באורך הקלט, וכן מתקיים

$A(x)=\psi \in QBF\iff x\in L$

ולכן השפה QBF היא PSPACE שלמה.

ראו גם

• PSPACE
• ההיררכיה הפולינומית

הערות שוליים

.

הערך באדיבות ויקיפדיה העברית, קרדיט,
רשימת התורמים
רישיון cc-by-sa 3.0

27636466TQBF