הצגת המקור של הדף "TQBF"

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

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

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

<math>(x_1 \lor x_2) \land (\neg x_1 \lor x_3)</math>

ועבור ההצבה <math>x_1 = T, x_2 = F, x_3 = T </math> הנוסחה מקבלת ערך אמת בעוד עבור <math>x_1 = F, x_2 = F, x_3 = T </math> הנוסחה מקבלת ערך שקר.

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

<math>\exists x_1 \exists x_2 \exists x_3 ((x_1 \lor x_2) \land (\neg x_1 \lor x_3))</math>

וערכה הוא אמת, מכיוון שקיימים <math>x_1, x_2, x_3 </math> עבורם יש הצבות אמת.

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

==סקירה==
בתורת הסיבוכיות, השפה '''QBF''' היא הכללה של השפה '''SAT''' בה לכל משתנה מוצמד כמת. מכיוון ש-QBF נמצאת ב-PSPACE, אין חובה לכתוב את הנוסחאות בצורת [[CNF]] מכיוון שזה ודאי לא הופך את השפה ל"קלה" יותר, אך גם לא הופך אותה לקשה יותר. מאחר שלכל משתנה מוצמד כמת, לנוסחה יש ערך אמת או שקר, והשפה QBF היא של הנוסחאות שמקבלות ערך אמת. פורמלית : <math>QBF = \{ \phi \ | \ \phi \text{ is a quantified boolean formula that evaluates to true} \}</math>
דוגמה:
: <math> \psi = \forall x_1 \exist x_2 \exist x_3 (x_1 \land x_2 \land \neg x_3) \lor x1 \lor (\neg x_1 \land x_2 \land x_3)</math>
מתקיים <math> \psi \in QBF </math>.

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

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

ל-QBF מספר צורות נורמליות. אחת הצורות החשובות היא [[הצורה הנורמלית של פרנקס]] אם היא מהצורה
: <math>\exists x_1 \forall x_2 \exists x_3 ... Q_n x_n \phi(x_1,x_2,...,x_n).</math>
הצורה הזאת חשובה במיוחד בגלל הקשר שלה ל[[ההיררכיה הפולינומית|היררכיה הפולינומית]]. כידוע,
: <math>PH = \bigcup_{i=_1}^\infty \Sigma_i = \bigcup_{i=_1}^\infty \Pi_i</math>
וגם המחלקה <math>\Sigma_i</math> מוגדרת כל השפות A עבורן קיים מוודא פולינומי <math>V</math> ופולינום <math>P(\cdot) </math> כך ש-
: <math>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</math>,
והנוסחה למעלה ניתנת לרדוקציה טריוויאלית ל-QBF.

===PH ו-PSPACE===
ההנחה הרווחת כיום היא ש <math>PH \not = PSPACE</math>, מכיוון שאם PH=PSPACE, אזי QBF נמצא באחת מדרגות ההיררכיה הפולינומית ולכן ההיררכיה קורסת בדרגה זאת, אף על פי שמקובל להניח שזה לא קורה{{הערה|Prof. Salil Vadhan, [https://people.seas.harvard.edu/~salil/cs221/fall02/scribenotes/Oct21.pdf] |כיוון=שמאל}}.

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

[[אלגוריתם]] לפתרון:
#אם הנוסחה ריקה, החזר אמת.
#עבור המשתנה הראשון x בנוסחה בצע:
## הצב T ב<math>x </math>
### פתור את הנוסחה והצב את התוצאה ב<math>y_T</math>
## הצב F ב<math>x </math>
### פתור את הנוסחה והצב את התוצאה ב<math>y_F</math>
# אם הכמת של x הוא "לכל":
## החזר <math>y_T \land y_F</math>
# אם הכמת של x הוא "קיים":
## החזר <math>y_T \lor y_F</math>

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

==שלמות של QBF==
נרצה להראות שהשפה QBF שלמה ב-PSPACE תחת רדוקציית קארפ פולינומית, כלומר
<math>\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|)</math>

או, בכתיב חסכני, <math>\forall L \in PSPACE, \ \ L \leq_m^p QBF</math>

לשם כך נגדיר ראשית את גרף הקונפיגורציות <math>G_M </math> של מכונת טיורינג M:

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

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

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

קל לראות שאם [[קלט]] x נמצא בשפה אזי קיים מסלול בין המצב ההתחלתי שלו <math>C_{start}^{M,x}</math> למצב ה'''מקבל''' שלו <math>C_{accpet}^{M,x}</math>.

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

כעת נרצה לבנות נוסחה המבטאת את <math>\psi(C_{start}^{M,x}, C_{accpet}^{M,x})</math>. המשתנים הם כמו בהוכחת [[משפט קוק לוין]], שמראה גם איך אפשר לקודד את <math>\psi(C, C')</math> אם יש ביניהם מסלול באורך 1 (כלומר המכונה עוברת מ-C ל-C' בצעד חוקי אחד).

ניסיון: נגדיר את הנוסחה באופן הבא:
<math>\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})</math>-C'

הנוסחה הנ"ל באורך אקספוננציאלי. נגדיר [[פונקציה]] חדשה: <math>\psi_i(C, C')</math> הוא אמת אם ורק קיים מסלול בין C ל-C' באורך לכל היותר <math>2^i </math>.

נשים לב שמתקיים: <math>\psi_{i+1}(C, C') = \exists C'' \ \ \psi_i(C, C'') \land \psi_i(C'', C')</math>

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

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

<math>\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)</math>

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

כעת, כאשר נפתח לפי הנוסחה הנ"ל, נקבל נוסחה בוליאנית עם כמתים שאורכה פולינומי באורך הקלט, וכן מתקיים
: <math>A(x) = \psi \in QBF \iff x \in L</math>

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

==ראו גם==
* [[PSPACE]]
* [[ההיררכיה הפולינומית]]

==הערות שוליים==
{{הערות שוליים|יישור=ימין}}.

[[קטגוריה:אלגברה בוליאנית]]