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. פתור את הנוסחה והצב את התוצאה בהפענוח נכשל (SVG (אפשר להפעיל MathML בעזרת הרחבת דפדפן): תשובה בלתי־תקינה ("Math extension cannot connect to Restbase.") מהשרת "https://wikimedia.org/api/rest_v1/":): {\displaystyle y_F}
3. אם הכמת של x הוא "לכל":
   1. החזר הפענוח נכשל (SVG (אפשר להפעיל MathML בעזרת הרחבת דפדפן): תשובה בלתי־תקינה ("Math extension cannot connect to Restbase.") מהשרת "https://wikimedia.org/api/rest_v1/":): {\displaystyle y_T \land y_F}
4. אם הכמת של x הוא "קיים":
   1. החזר הפענוח נכשל (SVG (אפשר להפעיל MathML בעזרת הרחבת דפדפן): תשובה בלתי־תקינה ("Math extension cannot connect to Restbase.") מהשרת "https://wikimedia.org/api/rest_v1/":): {\displaystyle y_T \lor y_F}

ניתוח סיבוכיות מקום: הפונקציה המתארת את סיבוכיות המקום של האלגוריתם היא הפענוח נכשל (SVG (אפשר להפעיל MathML בעזרת הרחבת דפדפן): תשובה בלתי־תקינה ("Math extension cannot connect to Restbase.") מהשרת "https://wikimedia.org/api/rest_v1/":): {\displaystyle f(n) = 1 + f(n-1) = O(n)} , מכיוון שבזמן הקריאה הרקורסיבית, אנחנו שומרים כמות זיכרון קבועה. סיבוכיות הזמן היא אקספוננציאלית

שלמות של QBF

נרצה להראות שהשפה QBF שלמה ב-PSPACE תחת רדוקציית קארפ פולינומית, כלומר הפענוח נכשל (SVG (אפשר להפעיל MathML בעזרת הרחבת דפדפן): תשובה בלתי־תקינה ("Math extension cannot connect to Restbase.") מהשרת "https://wikimedia.org/api/rest_v1/":): {\displaystyle \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|)}

או, בכתיב חסכני, הפענוח נכשל (SVG (אפשר להפעיל MathML בעזרת הרחבת דפדפן): תשובה בלתי־תקינה ("Math extension cannot connect to Restbase.") מהשרת "https://wikimedia.org/api/rest_v1/":): {\displaystyle \forall L \in PSPACE, \ \ L \leq_m^p QBF}

לשם כך נגדיר ראשית את גרף הקונפיגורציות הפענוח נכשל (SVG (אפשר להפעיל MathML בעזרת הרחבת דפדפן): תשובה בלתי־תקינה ("Math extension cannot connect to Restbase.") מהשרת "https://wikimedia.org/api/rest_v1/":): {\displaystyle G_M } של מכונת טיורינג M:

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

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

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

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

קל לראות שאם קלט x נמצא בשפה אזי קיים מסלול בין המצב ההתחלתי שלו הפענוח נכשל (SVG (אפשר להפעיל MathML בעזרת הרחבת דפדפן): תשובה בלתי־תקינה ("Math extension cannot connect to Restbase.") מהשרת "https://wikimedia.org/api/rest_v1/":): {\displaystyle C_{start}^{M,x}} למצב המקבל שלו $C_{accpet}^{M,x}$.

נגדיר פונקציה הפענוח נכשל (SVG (אפשר להפעיל MathML בעזרת הרחבת דפדפן): תשובה בלתי־תקינה ("Math extension cannot connect to Restbase.") מהשרת "https://wikimedia.org/api/rest_v1/":): {\displaystyle \psi(C, C')} , אשר מחזירה אמת אם ורק אם קיים מסלול בין C ל-C' בגרף.

ניסיון: נגדיר את הנוסחה באופן הבא: הפענוח נכשל (SVG (אפשר להפעיל MathML בעזרת הרחבת דפדפן): תשובה בלתי־תקינה ("Math extension cannot connect to Restbase.") מהשרת "https://wikimedia.org/api/rest_v1/":): {\displaystyle \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'

הנוסחה הנ"ל באורך אקספוננציאלי. נגדיר פונקציה חדשה: הפענוח נכשל (SVG (אפשר להפעיל MathML בעזרת הרחבת דפדפן): תשובה בלתי־תקינה ("Math extension cannot connect to Restbase.") מהשרת "https://wikimedia.org/api/rest_v1/":): {\displaystyle \psi_i(C, C')} הוא אמת אם ורק קיים מסלול בין C ל-C' באורך לכל היותר הפענוח נכשל (SVG (אפשר להפעיל MathML בעזרת הרחבת דפדפן): תשובה בלתי־תקינה ("Math extension cannot connect to Restbase.") מהשרת "https://wikimedia.org/api/rest_v1/":): {\displaystyle 2^i } .

נשים לב שמתקיים: הפענוח נכשל (SVG (אפשר להפעיל MathML בעזרת הרחבת דפדפן): תשובה בלתי־תקינה ("Math extension cannot connect to Restbase.") מהשרת "https://wikimedia.org/api/rest_v1/":): {\displaystyle \psi_{i+1}(C, C') = \exists C'' \ \ \psi_i(C, C'') \land \psi_i(C'', C')}

משמעות הנוסחה למעלה: קיים מסלול בין הפענוח נכשל (SVG (אפשר להפעיל MathML בעזרת הרחבת דפדפן): תשובה בלתי־תקינה ("Math extension cannot connect to Restbase.") מהשרת "https://wikimedia.org/api/rest_v1/":): {\displaystyle C} ל-הפענוח נכשל (SVG (אפשר להפעיל MathML בעזרת הרחבת דפדפן): תשובה בלתי־תקינה ("Math extension cannot connect to Restbase.") מהשרת "https://wikimedia.org/api/rest_v1/":): {\displaystyle C'} אם ורק אם קיימת קונפיגורציה הפענוח נכשל (SVG (אפשר להפעיל MathML בעזרת הרחבת דפדפן): תשובה בלתי־תקינה ("Math extension cannot connect to Restbase.") מהשרת "https://wikimedia.org/api/rest_v1/":): {\displaystyle C''} כך שיש מסלול בין $C$ ל-הפענוח נכשל (SVG (אפשר להפעיל MathML בעזרת הרחבת דפדפן): תשובה בלתי־תקינה ("Math extension cannot connect to Restbase.") מהשרת "https://wikimedia.org/api/rest_v1/":): {\displaystyle C''} ובין הפענוח נכשל (SVG (אפשר להפעיל MathML בעזרת הרחבת דפדפן): תשובה בלתי־תקינה ("Math extension cannot connect to Restbase.") מהשרת "https://wikimedia.org/api/rest_v1/":): {\displaystyle C''} ל-הפענוח נכשל (SVG (אפשר להפעיל MathML בעזרת הרחבת דפדפן): תשובה בלתי־תקינה ("Math extension cannot connect to Restbase.") מהשרת "https://wikimedia.org/api/rest_v1/":): {\displaystyle C'} .

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

הפענוח נכשל (SVG (אפשר להפעיל MathML בעזרת הרחבת דפדפן): תשובה בלתי־תקינה ("Math extension cannot connect to Restbase.") מהשרת "https://wikimedia.org/api/rest_v1/":): {\displaystyle \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)}

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

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

הפענוח נכשל (SVG (אפשר להפעיל MathML בעזרת הרחבת דפדפן): תשובה בלתי־תקינה ("Math extension cannot connect to Restbase.") מהשרת "https://wikimedia.org/api/rest_v1/":): {\displaystyle A(x) = \psi \in QBF \iff x \in L}

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

ראו גם

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

הערות שוליים

.

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

27636466TQBF