صيغة منطقية كمية حقيقية

📅 آخر تحديث: ٣١ يوليو ٢٠٢٦
✍️ نُشر في: ٣١ يوليو ٢٠٢٦
📷 يحتوي على 43 صور
الموسوعة الحرة

في نظرية التعقيد الحسابي ، تُعدّ لغة TQBF لغةً رسميةً تتألف من الصيغ المنطقية الكمية الصحيحة . الصيغة المنطقية الكمية (بشكل كامل) هي صيغة في منطق القضايا الكمية (المعروف أيضًا بمنطق القضايا من الرتبة الثانية ) حيث يتم تحديد كمية كل متغير (أو تقييده ) باستخدام مُكمِّمات وجودية أو شاملة في بداية الجملة. هذه الصيغة تُكافئ إما الصواب أو الخطأ (لعدم وجود متغيرات حرة ). إذا كانت نتيجة هذه الصيغة صحيحة، فإنها تنتمي إلى لغة TQBF. تُعرف هذه اللغة أيضًا باسم QSAT (المسألة الكمية SAT ).

ملخص

في نظرية التعقيد الحسابي، تُعدّ مسألة الصيغة البوليانية الكمية ( QBF ) تعميمًا لمسألة قابلية الإرضاء البولياني، حيث يمكن تطبيق كل من المُكمِّمات الوجودية والمُكمِّمات الشاملة على كل متغير. بعبارة أخرى، تسأل هذه المسألة عما إذا كانت الصيغة الجملية الكمية لمجموعة من المتغيرات البوليانية صحيحة أم خاطئة. على سبيل المثال، فيما يلي مثال على مسألة الصيغة البوليانية الكمية:

∀x ∃y ∃z ((x∨z)∧y){\displaystyle \forall x\ \exists y\ \exists z\ ((x\lor z)\land y)}

تُعدّ مسألة QBF المسألة الكاملة النموذجية لفئة PSPACE ، وهي فئة المسائل التي يمكن حلّها بواسطة آلة تورينغ حتمية أو غير حتمية في فضاء متعدد الحدود وزمن غير محدود. [ 1 ] وبإعطاء الصيغة على شكل شجرة بناء جملة مجردة ، يمكن حلّ المسألة بسهولة بواسطة مجموعة من الإجراءات المتكررة المتبادلة التي تُقيّم الصيغة. تستخدم هذه الخوارزمية مساحة تتناسب مع ارتفاع الشجرة، وهي مساحة خطية في أسوأ الحالات، ولكنها تستخدم زمنًا أُسّيًا بالنسبة لعدد المُكمِّمات.

بافتراض أن MA ⊊ PSPACE، وهو ما يُعتقد على نطاق واسع، لا يمكن حل مسألة QBF، ولا يمكن حتى التحقق من صحة أي حل مُعطى، سواء في وقت متعدد الحدود حتمي أو احتمالي (في الواقع، على عكس مسألة الإرضاء، لا توجد طريقة معروفة لتحديد حل بإيجاز). يمكن حلها باستخدام آلة تورينج متناوبة في وقت خطي، لأن AP = PSPACE، حيث AP هي فئة المسائل التي يمكن للآلات المتناوبة حلها في وقت متعدد الحدود. [ 2 ]

عندما تم إثبات النتيجة الأساسية IP = PSPACE (انظر نظام البرهان التفاعلي )، تم ذلك من خلال عرض نظام برهان تفاعلي قادر على حل QBF عن طريق حل عملية حسابية محددة للمسألة. [ 3 ]

تتضمن صيغ QBF عددًا من الأشكال القياسية المفيدة. على سبيل المثال، يمكن إثبات وجود اختزال متعدد الحدود ذي زمن متعدد الحدود ينقل جميع المحددات الكمية إلى بداية الصيغة ويجعلها تتناوب بين المحددات الكمية الكلية والوجودية. وهناك اختزال آخر أثبت جدواه في برهان IP = PSPACE، حيث لا يُوضع أكثر من محدد كمي كلي واحد بين استخدام كل متغير والمحدد الكمي الذي يربط ذلك المتغير. وكان هذا الأمر بالغ الأهمية في الحد من عدد نواتج الضرب في بعض التعبيرات الفرعية للحساب.

نموذج برينكس الطبيعي

يمكن افتراض أن الصيغة المنطقية الكمية بالكامل لها شكل محدد للغاية، يُسمى الشكل الطبيعي المسبق . وهي تتكون من جزأين أساسيين: جزء يحتوي على مُكمِّمات فقط، وجزء يحتوي على صيغة منطقية غير كمية، ويُشار إليها عادةً بـϕ{\displaystyle \displaystyle \phi }إذا كان هناكن{\displaystyle \displaystyle n}بالنسبة للمتغيرات المنطقية، يمكن كتابة الصيغة الكاملة على النحو التالي:

∃x1∀x2∃x3⋯سؤالنxنϕ(x1،x2،x3،...،xن){\displaystyle \displaystyle \exists x_{1}\forall x_{2}\exists x_{3}\cdots Q_{n}x_{n}\phi (x_{1},x_{2},x_{3},\dots ,x_{n})}

حيث يقع كل متغير ضمن نطاق مُكمِّم ما. وبإدخال متغيرات وهمية، يمكن تحويل أي صيغة في شكلها الطبيعي السابق إلى جملة تتناوب فيها المُكمِّمات الوجودية والكلية. باستخدام المتغير الوهميy1{\displaystyle \displaystyle y_{1}}،

∃x1∃x2ϕ(x1،x2)↦∃x1∀y1∃x2ϕ(x1،x2){\displaystyle \displaystyle \exists x_{1}\exists x_{2}\phi (x_{1},x_{2})\quad \mapsto \quad \exists x_{1}\forall y_{1}\exists x_{2}\phi (x_{1},x_{2})}

الجملة الثانية لها نفس قيمة الصواب، لكنها تتبع الصيغة المقيدة. يُعدّ افتراض أن الصيغ المنطقية الكمية بالكامل تكون في شكلها الطبيعي المسبق سمة شائعة في البراهين.

حلول QBF

ساذج

توجد خوارزمية تكرارية بسيطة لتحديد ما إذا كانت QBF تنتمي إلى TQBF (أي أنها صحيحة). بفرض وجود QBF ما

سؤال1x1سؤال2x2⋯سؤالنxنϕ(x1،x2،...،xن).{\displaystyle Q_{1}x_{1}Q_{2}x_{2}\cdots Q_{n}x_{n}\phi (x_{1},x_{2},\dots ,x_{n}).}

إذا لم تحتوي الصيغة على أي محددات كمية، فيمكننا ببساطة إرجاع الصيغة. وإلا، فإننا نزيل المحدد الكمي الأول ونتحقق من القيمتين المحتملتين للمتغير الأول:

أ=سؤال2x2⋯سؤالنxنϕ(0،x2،...،xن)،{\displaystyle A=Q_{2}x_{2}\cdots Q_{n}x_{n}\phi (0,x_{2},\dots ,x_{n}),}
ب=سؤال2x2⋯سؤالنxنϕ(1،x2،...،xن).{\displaystyle B=Q_{2}x_{2}\cdots Q_{n}x_{n}\phi (1,x_{2},\dots ,x_{n}).}

لوسؤال1=∃{\displaystyle Q_{1}=\exists }ثم العودةأ∨ب{\displaystyle A\lor B}. لوسؤال1=∀{\displaystyle Q_{1}=\forall }ثم العودةأ∧ب{\displaystyle A\land B}[ 4 ]​

ما مدى سرعة تنفيذ هذه الخوارزمية؟ لكل مُكمِّم في مسألة QBF الأولية، تُجري الخوارزمية استدعاءين متكررين على مسألة فرعية أصغر خطيًا فقط. وهذا يُعطي الخوارزمية زمن تشغيل أُسِّيًا O(2^ n ) .

ما مقدار المساحة التي تستخدمها هذه الخوارزمية؟ في كل استدعاء للخوارزمية، تحتاج إلى تخزين النتائج الوسيطة لحساب A وB. كل استدعاء تكراري يُزيل مُكمِّمًا واحدًا، لذا فإن العمق التكراري الكلي خطي بالنسبة لعدد المُكمِّمات. يمكن تقييم الصيغ التي تفتقر إلى المُكمِّمات في مساحة لوغاريتمية بالنسبة لعدد المتغيرات. كانت صيغة QBF الأولية مُكمَّمة بالكامل، لذا يوجد على الأقل عدد من المُكمِّمات يساوي عدد المتغيرات. وبالتالي، تستخدم هذه الخوارزمية مساحة O ( n + log n ) = O ( n ). هذا يجعل لغة TQBF جزءًا من فئة تعقيد PSPACE .

مثال رائع من الفن

على الرغم من أن مسألة QBF مصنفة ضمن فئة PSPACE-complete، فقد طُوّرت العديد من الخوارزميات لحل هذه الحالات (وهذا مشابه لحالة SAT ، وهي نسخة المُكمِّم الوجودي الأحادي؛ فعلى الرغم من أنها مصنفة ضمن فئة NP-complete ، إلا أنه لا يزال من الممكن حل العديد من حالات SAT باستخدام الاستدلال). [ 5 ] [ 6 ] وقد حظيت الحالة التي يوجد فيها مُكمِّمان فقط، والمعروفة باسم 2QBF، باهتمام خاص. [ 7 ]

تُقام مسابقة QBFEVAL لحل مسائل QBF بشكل شبه سنوي منذ عام 2004؛ [ 5 ] [ 6 ] ويُشترط على برامج الحل قراءة البيانات بصيغة QDIMACS، بالإضافة إلى إحدى صيغتي QCIR أو QAIGER. [ 8 ] وتستخدم برامج حل مسائل QBF عالية الأداء عادةً QDPLL (وهي تعميم لـ DPLL ) أو CEGAR. [ 5 ] [ 6 ] [ 7 ] بدأ البحث في حل مسائل QBF بتطوير DPLL التراجعي لها في عام 1998، تلاه إدخال تعلم البنود وحذف المتغيرات في عام 2002؛ [ 9 ] وبالتالي، بالمقارنة مع حل مسائل SAT، الذي يجري تطويره منذ ستينيات القرن الماضي، يُعد مجال QBF مجالًا بحثيًا حديثًا نسبيًا حتى عام 2017. [ 9 ]

تتضمن بعض برامج حل QBF البارزة ما يلي:

  • برنامج CADET، الذي يحل الصيغ البوليانية الكمية المقيدة بتناوب كمي واحد (مع القدرة على حساب دوال سكوليم )، استنادًا إلى التحديد التزايدي والقدرة على إثبات إجاباته. [ 10 ]
  • CAQE - برنامج حل قائم على CEGAR للصيغ المنطقية الكمية؛ الفائز في الإصدارات الأخيرة من QBFEVAL اعتبارًا من عام 2021. [ 11 ]
  • DepQBF - أداة حل قائمة على البحث للصيغ المنطقية الكمية [ 12 ]
  • sKizzo - أول برنامج حل يستخدم skolemization الرمزي، ويستخرج شهادات الإرضاء، ويستخدم محرك استدلال هجين ، وينفذ التفرع المجرد، ويتعامل مع الكميات المحدودة، ويحصي التعيينات الصالحة، والفائز بجائزة QBFEVAL 2005 و2006 و2007. [ 13 ]

التطبيقات

يمكن تطبيق خوارزميات حل QBF على التخطيط (في مجال الذكاء الاصطناعي)، بما في ذلك التخطيط الآمن؛ وهو أمر بالغ الأهمية في تطبيقات الروبوتات. [ 14 ] كما يمكن تطبيق خوارزميات حل QBF على التحقق من النماذج المحدودة ، لأنها توفر ترميزًا أقصر مما هو مطلوب لخوارزمية حل SAT. [ 14 ]

يمكن اعتبار تقييم QBF بمثابة لعبة ثنائية اللاعبين بين لاعب يتحكم في متغيرات كمية وجودية ولاعب يتحكم في متغيرات كمية شاملة. وهذا ما يجعل QBFs مناسبة لترميز مسائل التركيب التفاعلي . [ 14 ] وبالمثل، يمكن استخدام حلول QBF لنمذجة الألعاب التنافسية في نظرية الألعاب . على سبيل المثال، يمكن استخدام حلول QBF لإيجاد استراتيجيات رابحة لألعاب الجغرافيا ، والتي يمكن لعبها تلقائيًا بشكل تفاعلي. [ 15 ]

يمكن استخدام حلول QBF للتحقق من التكافؤ الرسمي ، ويمكن استخدامها أيضًا لتوليد الدوال المنطقية. [ 14 ]

تشمل أنواع المشاكل الأخرى التي يمكن ترميزها كـ QBFs ما يلي:

  • الكشف عما إذا كانت جملة في صيغة غير قابلة للإرضاء في شكل عادي ترابطي تنتمي إلى مجموعة فرعية غير قابلة للإرضاء بشكل أدنى [ 9 ] [ 16 ] وما إذا كانت جملة في صيغة قابلة للإرضاء تنتمي إلى مجموعة فرعية قابلة للإرضاء بشكل أقصى [ 16 ].
  • ترميزات التخطيط المتوافق [ 9 ]
  • المشاكل المتعلقة بـ ASP [ 9 ]
  • الحجاج المجرد [ 9 ]
  • التحقق من نموذج المنطق الزمني الخطي [ 9 ]
  • تضمين لغة الأوتوماتون المحدودة غير الحتمية [ 9 ]
  • توليف وموثوقية الأنظمة الموزعة [ 9 ]

الإضافات

تُعدّ مسألة الإرضاء العشوائي (المعروفة اختصاراً بـ SSAT) امتداداً لمسألة TQBF، حيث تُضيف مُكمِّماً عشوائياً R، وتعتبر التكميم الشامل بمثابة تصغير، والتكميم الوجودي بمثابة تعظيم، وتسأل عما إذا كان الاحتمال المُمثَّل بالصيغة يتجاوز عتبة مُحدَّدة. [ 17 ]

يمكن أيضًا توسيع QBF ليشمل محددات هينكين الكمية . [ 8 ]

اكتمال PSPACE

تُعتبر لغة TQBF في نظرية التعقيد مثالًا نموذجيًا لمسألة PSPACE-complete . وتعني PSPACE-complete أن اللغة تنتمي إلى فئة PSPACE وأنها أيضًا PSPACE-hard . تُظهر الخوارزمية أعلاه أن TQBF تنتمي إلى PSPACE. ويتطلب إثبات أن TQBF هي PSPACE-hard إثبات إمكانية اختزال أي لغة في فئة التعقيد PSPACE إلى TQBF في وقت متعدد الحدود.

∀ل∈PSPأجهـ،ل≤صتيسؤالبF.{\displaystyle \forall L\in {\mathsf {PSPACE}},L\leq _{p}\mathrm {TQBF} .}

هذا يعني أنه بالنسبة للغة PSPACE L، يمكن تحديد ما إذا كان المدخل x ينتمي إلى L عن طريق التحقق مما إذاو(x){\displaystyle f(x)}في إطار TQBF، بالنسبة لدالة f التي يجب أن تعمل في وقت متعدد الحدود (نسبةً إلى طول المدخلات). رمزياً،

x∈ل⟺و(x)∈تيسؤالبF.{\displaystyle x\in L\iff f(x)\in \mathrm {TQBF} .}

إثبات أن TQBF صعب في PSPACE يتطلب تحديد f .

لنفترض أن L هي لغة PSPACE. هذا يعني أنه يمكن تحديد L بواسطة آلة تورينغ حتمية ذات مساحة متعددة الحدود (DTM). يُعد هذا الأمر بالغ الأهمية لاختزال L إلى TQBF، لأن تكوينات أي آلة تورينغ من هذا النوع يمكن تمثيلها بصيغ منطقية، حيث تمثل المتغيرات المنطقية حالة الآلة ومحتويات كل خلية على شريط آلة تورينغ، ويتم ترميز موضع رأس آلة تورينغ في الصيغة من خلال ترتيبها. على وجه الخصوص، سيستخدم اختزالنا المتغيراتج1{\displaystyle c_{1}}وج2{\displaystyle c_{2}}، والتي تمثل تكوينين محتملين لـ DTM لـ L، وعدد طبيعي t، في بناء QBFϕج1،ج2،ت{\displaystyle \phi _{c_{1},c_{2},t}}وهذا صحيح إذا وفقط إذا كان بإمكان DTM الخاص بـ L الانتقال من التكوين المشفر فيج1{\displaystyle c_{1}}إلى التكوين المشفر فيج2{\displaystyle c_{2}}في خطوات لا تتجاوز t. وبالتالي، ستقوم الدالة f بإنشاء QBF من DTM لـ Lϕجيبدأ،جيقبل،تي{\displaystyle \phi _{c_{\text{start}},c_{\text{accept}},T}}، أينجsتأرت{\displaystyle c_{start}}هذا هو التكوين الابتدائي لـ DTM،جيقبل{\displaystyle c_{\text{accept}}}يمثل التكوين المُستقبِل لـ DTM، وT هو الحد الأقصى لعدد الخطوات التي قد يحتاجها DTM للانتقال من تكوين إلى آخر. نعلم أن T = O (exp( nk ) ) لبعض قيم k ، حيث n هو طول المُدخل، لأن هذا يُحدِّد العدد الإجمالي للتكوينات المُمكنة لـ DTM ذي الصلة. بالطبع، لا يُمكن أن يتطلب DTM خطوات أكثر من عدد التكوينات المُمكنة للوصول إليها.جأججهـصت{\displaystyle c_{\mathrm {accept} }}إلا إذا دخلت في حلقة تكرارية، وفي هذه الحالة لن تصل أبدًاجأججهـصت{\displaystyle c_{\mathrm {accept} }}على أي حال.

في هذه المرحلة من البرهان، قمنا بالفعل بتقليص مسألة ما إذا كانت صيغة الإدخال w (المشفرة، بالطبع، فيجيبدأ{\displaystyle c_{\text{start}}}) يتعلق بمسألة ما إذا كان QBFϕجيبدأ،جيقبل،تي{\displaystyle \phi _{c_{\text{start}},c_{\text{accept}},T}}، أي،و(w){\displaystyle f(w)}، في TQBF. يثبت الجزء المتبقي من هذا البرهان أنه يمكن حساب f في وقت متعدد الحدود.

لت=1{\displaystyle t=1}، حسابϕج1،ج2،ت{\displaystyle \phi _{c_{1},c_{2},t}}الأمر بسيط - إما أن يتغير أحد التكوينين إلى الآخر في خطوة واحدة أو لا يتغير. وبما أن آلة تورينج التي تمثلها معادلتنا حتمية، فإن هذا لا يمثل أي مشكلة.

لت>1{\displaystyle t>1}، حسابϕج1،ج2،ت{\displaystyle \phi _{c_{1},c_{2},t}}يتضمن ذلك تقييمًا متكررًا، يبحث عن ما يسمى "نقطة المنتصف".م1{\displaystyle m_{1}}في هذه الحالة، نعيد كتابة الصيغة على النحو التالي:

ϕج1،ج2،ت=∃م1(ϕج1،م1،⌈ت/2⌉∧ϕم1،ج2،⌈ت/2⌉).{\displaystyle \phi _{c_{1},c_{2},t}=\exists m_{1}(\phi _{c_{1},m_{1},\lceil t/2\rceil }\wedge \phi _{m_{1},c_{2},\lceil t/2\rceil }).}

هذا يحول مسألة ما إذاج1{\displaystyle c_{1}}يمكن الوصولج2{\displaystyle c_{2}}في خطوات نحو مسألة ما إذاج1{\displaystyle c_{1}}يصل إلى نقطة وسطىم1{\displaystyle m_{1}}فيت/2{\displaystyle t/2}الدرجات، التي تصل بدورها إلىج2{\displaystyle c_{2}}فيت/2{\displaystyle t/2}خطوات. بالطبع، الإجابة على السؤال الأخير تعطي الإجابة على السؤال الأول.

الآن، قيمة t محدودة فقط بالقيمة T، وهي دالة أسية (وبالتالي ليست متعددة الحدود) بالنسبة لطول المدخلات. بالإضافة إلى ذلك، تُضاعف كل طبقة تكرارية طول الصيغة تقريبًا. (المتغيرم1{\displaystyle m_{1}}هي مجرد نقطة منتصف واحدة - فكلما زادت قيمة t، زادت المحطات على طول الطريق، إن صح التعبير. لذا فإن الوقت اللازم للتقييم المتكررϕج1،ج2،ت{\displaystyle \phi _{c_{1},c_{2},t}}بهذه الطريقة، قد يكون النمو أُسّيًا أيضًا، ببساطة لأن الصيغة قد تصبح كبيرة أُسّيًا. تُحل هذه المشكلة من خلال التحديد الكمي الشامل باستخدام المتغيرات.ج3{\displaystyle c_{3}}وج4{\displaystyle c_{4}}على أزواج التكوين (على سبيل المثال،{(ج1،م1)،(م1،ج2)}{\displaystyle \{(c_{1},m_{1}),(m_{1},c_{2})\}}مما يمنع تمدد طول الصيغة بسبب الطبقات المتكررة. وهذا يؤدي إلى التفسير التالي لـϕج1،ج2،ت{\displaystyle \phi _{c_{1},c_{2},t}}:

ϕج1،ج2،ت=∃م1∀(ج3،ج4)∈{(ج1،م1)،(م1،ج2)}(ϕج3،ج4،⌈ت/2⌉).{\displaystyle \phi _{c_{1},c_{2},t}=\exists m_{1}\forall (c_{3},c_{4})\in \{(c_{1},m_{1}),(m_{1},c_{2})\}(\phi _{c_{3},c_{4},\lceil t/2\rceil }).}

يمكن بالفعل حساب هذه الصيغة في وقت متعدد الحدود، حيث يمكن حساب أي حالة منها في وقت متعدد الحدود. ويخبرنا الزوج المرتب الكمي الشامل ببساطة أنه مهما كان اختيارنا لـ(ج3،ج4){\displaystyle (c_{3},c_{4})}تم صنعه،ϕج1،ج2،ت⟺ϕج3،ج4،⌈ت/2⌉{\displaystyle \phi _{c_{1},c_{2},t}\iff \phi _{c_{3},c_{4},\lceil t/2\rceil }}.

هكذا،∀ل∈PSPأجهـ،ل≤صتيسؤالبF{\displaystyle \forall L\in {\mathsf {PSPACE}},L\leq _{p}\mathrm {TQBF} }إذن، تُعتبر لغة TQBF لغة صعبة في فضاء PSPACE. وبالإضافة إلى النتيجة السابقة التي تُثبت أن TQBF تنتمي إلى فضاء PSPACE، يكتمل بذلك برهان أن TQBF لغة كاملة في فضاء PSPACE.

(يتبع هذا البرهان Sipser 2006 الصفحات  310-313 في جميع الأساسيات. يتضمن Papadimitriou 1994 أيضًا برهانًا.)

يمكن تنفيذ هذا البناء في فضاء لوغاريتمي، مما يعني أن TQBF كاملة في فضاء PSPACE بمعنى اختزال متعدد إلى واحد في فضاء لوغاريتمي . [ 18 ]

المنوعات

  • تُعدّ مسألة إرضاء الصيغة المنطقية إحدى المسائل الفرعية المهمة في TQBF . في هذه المسألة، نرغب في معرفة ما إذا كانت صيغة منطقية معينة صحيحة أم لا.ϕ{\displaystyle \phi }يمكن تحقيق ذلك بتعيين بعض المتغيرات. وهذا يُعادل نظرية TQBF باستخدام المُكمِّمات الوجودية فقط.∃x1⋯∃xنϕ(x1،...،xن){\displaystyle \exists x_{1}\cdots \exists x_{n}\phi (x_{1},\ldots ,x_{n})}هذا أيضًا مثال على النتيجة الأكبر NP ⊆ PSPACE التي تتبع مباشرة من الملاحظة أن مدقق الوقت متعدد الحدود لإثبات لغة مقبولة بواسطة NTM ( آلة تورينج غير الحتمية ) يتطلب مساحة متعددة الحدود لتخزين الإثبات.
  • أي فئة في التسلسل الهرمي متعدد الحدود ( PH ) تُعتبر مسألة TQBF فيها مسألة صعبة. بعبارة أخرى، بالنسبة للفئة التي تضم جميع اللغات L التي يوجد لها آلة تورينج V متعددة الزمن، وهي أداة تحقق، بحيث يكون لكل مدخل x وثابت i ما،x∈ل⇔∃y1∀y2⋯سؤالأناyأنا V(x،y1،y2،...،yأنا) = 1{\displaystyle x\in L\Leftrightarrow \exists y_{1}\forall y_{2}\cdots Q_{i}y_{i}\ V(x,y_{1},y_{2},\dots ,y_{i})\ =\ 1} which has a specific QBF formulation that is given as ∃ϕ{\displaystyle \exists \phi } such that ∃x1→∀x2→⋯Qixi→ ϕ(x1→,x2→,…,xi→) = 1{\displaystyle \exists {\vec {x_{1}}}\forall {\vec {x_{2}}}\cdots Q_{i}{\vec {x_{i}}}\ \phi ({\vec {x_{1}}},{\vec {x_{2}}},\dots ,{\vec {x_{i}}})\ =\ 1} where the xi→{\displaystyle {\vec {x_{i}}}}'s are vectors of Boolean variables.
  • It is important to note that while TQBF the language is defined as the collection of true quantified Boolean formulas, the abbreviation TQBF is often used (even in this article) to stand for a totally quantified Boolean formula, often simply called a QBF (quantified Boolean formula, understood as "fully" or "totally" quantified). It is important to distinguish contextually between the two uses of the abbreviation TQBF in reading the literature.
  • A TQBF can be thought of as a game played between two players, with alternating moves. Existentially quantified variables are equivalent to the notion that a move is available to a player at a turn. Universally quantified variables mean that the outcome of the game does not depend on what move a player makes at that turn. Also, a TQBF whose first quantifier is existential corresponds to a formula game in which the first player has a winning strategy.
  • A TQBF for which the quantified formula is in 2-CNF may be solved in linear time, by an algorithm involving strong connectivity analysis of its implication graph. The 2-satisfiability problem is a special case of TQBF for these formulas, in which every quantifier is existential.[19][20]
  • There is a systematic treatment of restricted versions of quantified Boolean formulas (giving Schaefer-type classifications) provided in an expository paper by Hubie Chen.[21]
  • Planar TQBF, generalizing Planar SAT, was proved PSPACE-complete by D. Lichtenstein.[22]

Notes and references

  1. ↑M. Garey & D. Johnson (1979). Computers and Intractability: A Guide to the Theory of NP-Completeness. W. H. Freeman, San Francisco, California. ISBN 0-7167-1045-5.
  2. ↑A. Chandra, D. Kozen, and L. Stockmeyer (1981). "Alternation". Journal of the ACM. 28 (1): 114–133. doi:10.1145/322234.322243. S2CID 238863413.{{cite journal}}: CS1 maint: multiple names: authors list (link)
  3. ↑Adi Shamir (1992). "Ip = Pspace". Journal of the ACM. 39 (4): 869–877. doi:10.1145/146585.146609. S2CID 315182.
  4. ↑ أرورا، سانجيف؛ باراك، بواز (2009)، "تعقيد المساحة" ، التعقيد الحسابي ، كامبريدج: مطبعة جامعة كامبريدج، ص 78-94 ، doi : 10.1017/cbo9780511804090.007 ، ISBN  978-0-511-80409-0، S2CID 262800930 ، تم استرجاعه بتاريخ 26-05-2021 
  5. 1 2 3 "الصفحة الرئيسية لـ QBFEVAL" . www.qbflib.org . تم الاطلاع عليه بتاريخ 13 فبراير 2021 .
  6. 1 2 3 "حلول QBF | ما وراء NP" . beyondnp.org . تم الاطلاع عليه بتاريخ 13 فبراير 2021 .
  7. 1 2 بالابانوف، فاليري؛ رولاند جيانغ، جي-هونغ؛ شول، كريستوف؛ ميشينكو، آلان؛ ك. برايتون، روبرت (2016). "2QBF: التحديات والحلول" (ملف PDF) . المؤتمر الدولي حول نظرية وتطبيقات اختبار الإرضاء : 453-459 . مؤرشف (ملف PDF) من الأصل في 13 فبراير 2021 - عبر SpringerLink.
  8. 1 2 "QBFEVAL'20" . www.qbflib.org . تم الاطلاع عليه بتاريخ 29-05-2021 .
  9. 1 2 3 4 5 6 7 8 9 لونسينغ، فلوريان (ديسمبر 2017). "مقدمة في حل QBF" (ملف PDF) . www.florianlonsing.com . تاريخ الاطلاع: 29 مايو 2021 .
  10. ^ راب ، ماركوس ن. (15/04/2021)، ماركوس راب / كاديت ، استرجاعها 2021/05/06
  11. ^ تنتروب ، ليندر (06/05/2021)، ltentrup/caqe ، استرجاعها 2021/05/06
  12. ↑ "DepQBF Solver" . lonsing.github.io . تم ​​الاطلاع عليه بتاريخ 2021-05-06 .
  13. ↑ "Skizzo - برنامج لحل مسائل QBF" . www.skizzo.site . تم الاطلاع عليه بتاريخ 2021-05-06 .
  14. 1 2 3 4 شوكلا، أنكيت؛ بير، أرمين؛ سيدل، مارتينا؛ بولينا، لوكا (2019). دراسة استقصائية حول تطبيقات الصيغ المنطقية الكمية (ملف PDF) . المؤتمر الدولي الحادي والثلاثون لأدوات الذكاء الاصطناعي لعام 2019، معهد مهندسي الكهرباء والإلكترونيات. الصفحات 78-84 . doi : 10.1109/ICTAI.2019.00020 . تاريخ الاسترجاع: 29 مايو 2021 . 
  15. ↑ شين، تشيهي. استخدام خوارزميات حل QBF لحل الألعاب والألغاز (ملف PDF) (أطروحة). كلية بوسطن.
  16. 1 2 جانوتا، ميكولاش؛ ماركيز سيلفا، جواو (2011). حول تحديد عضوية MUS باستخدام QBF . مبادئ وممارسات البرمجة المقيدة - CP 2011. المجلد 6876. الصفحات 414-428 . doi : 10.1007/978-3-642-23786-7_32 . ISBN   978-3-642-23786-7.
  17. ↑ كريستور باباديميتريو. ألعاب ضد الطبيعة، مجلة علوم الحاسوب والأنظمة 31، الصفحات 288-301، 1985.
  18. ↑ "CS 221: التعقيد الحسابي" (ملف PDF) . مؤرشف من النسخة الأصلية (ملف PDF) بتاريخ 20-07-2010.
  19. ^ كروم ، ملفين ر. (1967). “مشكلة القرار لفئة من صيغ الدرجة الأولى التي تكون فيها جميع الانفصالات ثنائية”. Zeitschrift für Mathematische Logik und Grundlagen der Mathematik . 13 ( 1 – 2): 15 – 20. دوي : 10.1002/malq.19670130104 ..
  20. ↑ أسبفال، بنغت؛ بلاس، مايكل ف.؛ تارجان، روبرت إي. (1979). "خوارزمية خطية لاختبار صحة بعض الصيغ المنطقية الكمية" (ملف PDF) . رسائل معالجة المعلومات . 8 (3): 121-123 . doi : 10.1016/0020-0190(79)90002-4 ..
  21. ↑ تشين، هوبي (ديسمبر 2009). "لقاء المنطق والتعقيد والجبر". مجلة ACM Computing Surveys . 42 (1). ACM: 1–32 . arXiv : cs/0611018 . doi : 10.1145/1592451.1592453 . S2CID 11975818 . 
  22. ↑ ليختنشتاين، ديفيد (1982-05-01). "الصيغ المستوية واستخداماتها" . مجلة SIAM للحوسبة . 11 (2): 329-343 . doi : 10.1137/0211025 . ISSN 0097-5397 . S2CID 207051487 .  
  • يقدم كتاب فورتناو وهومر (2003) بعض الخلفية التاريخية لـ PSPACE و TQBF.
  • يقدم تشانغ (2003) بعض الخلفية التاريخية للصيغ المنطقية.
  • أرورا، سانجيف. (2001). COS 522: التعقيد الحسابي . محاضرات، جامعة برينستون. تم الاطلاع عليه بتاريخ 10 أكتوبر 2005.
  • فورتناو، لانس وستيف هومر. (يونيو 2003). تاريخ موجز للتعقيد الحسابي . نشرة الرابطة الأوروبية لعلوم الحاسوب النظرية ، عمود التعقيد الحسابي، 80. تم الاطلاع عليه في 14 مايو 2024.
  • باباديميتريو، سي إتش (1994). التعقيد الحسابي. ريدينغ: أديسون-ويسلي.
  • سيبسر، مايكل. (2006). مقدمة في نظرية الحوسبة. بوسطن: تومسون كورس تكنولوجي.
  • تشانغ، لينتاو. (2003). البحث عن الحقيقة: تقنيات إرضاء الصيغ المنطقية . تم الاسترجاع في 10 أكتوبر 2005.

انظر أيضاً