True quantified Boolean formula

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

In computational complexity theory, the language TQBF is a formal language consisting of the true quantified Boolean formulas. A (fully) quantified Boolean formula is a formula in quantifiedpropositional logic (also known as Second-order propositional logic) where every variable is quantified (or bound), using either existential or universal quantifiers, at the beginning of the sentence. Such a formula is equivalent to either true or false (since there are no free variables). If such a formula evaluates to true, then that formula is in the language TQBF. It is also known as QSAT (Quantified SAT).

Overview

In computational complexity theory, the quantified Boolean formula problem (QBF) is a generalization of the Boolean satisfiability problem in which both existential quantifiers and universal quantifiers can be applied to each variable. Put another way, it asks whether a quantified sentential form over a set of Boolean variables is true or false. For example, the following is an instance of QBF:

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

QBF is the canonical complete problem for PSPACE, the class of problems solvable by a deterministic or nondeterministic Turing machine in polynomial space and unlimited time.[1] Given the formula in the form of an abstract syntax tree, the problem can be solved easily by a set of mutually recursive procedures which evaluate the formula. Such an algorithm uses space proportional to the height of the tree, which is linear in the worst case, but uses time exponential in the number of quantifiers.

Provided that MA ⊊ PSPACE, which is widely believed, QBF cannot be solved, nor can a given solution even be verified, in either deterministic or probabilistic polynomial time (in fact, unlike the satisfiability problem, there's no known way to specify a solution succinctly). It can be solved using an alternating Turing machine in linear time, since AP = PSPACE, where AP is the class of problems alternating machines can solve in polynomial time.[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}والتي لها صيغة QBF محددة معطاة على النحو التالي∃ϕ{\displaystyle \exists \phi } بحيث∃x1→∀x2→⋯سؤالأناxأنا→ ϕ(x1→،x2→،...،xأنا→) = 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}حيثxأنا→{\displaystyle {\vec {x_{i}}}}'s عبارة عن متجهات من المتغيرات المنطقية.
  • من المهم ملاحظة أنه على الرغم من أن لغة TQBF تُعرَّف بأنها مجموعة من الصيغ المنطقية الكمية الحقيقية، إلا أن الاختصار TQBF يُستخدم غالبًا (حتى في هذه المقالة) للدلالة على الصيغة المنطقية الكمية تمامًا، والتي تُسمى عادةً QBF (الصيغة المنطقية الكمية، والتي تُفهم على أنها كمية "كليًا"). من المهم التمييز سياقيًا بين استخدامي الاختصار TQBF عند قراءة المراجع.
  • يمكن اعتبار لعبة TQBF بمثابة لعبة بين لاعبين، يتناوبان فيها على اتخاذ القرارات. المتغيرات الكمية الوجودية تُعادل فكرة أن لكل لاعب دورًا متاحًا لاتخاذ قرار. أما المتغيرات الكمية الشاملة فتعني أن نتيجة اللعبة لا تعتمد على القرار الذي يتخذه اللاعب في ذلك الدور. كذلك، فإن لعبة TQBF التي يكون مُكمِّمها الأول وجوديًا تُقابل لعبة صيغة يكون فيها للاعب الأول استراتيجية رابحة.
  • يمكن حلّ مسألة TQBF التي تكون صيغتها الكمية في إطار 2-CNF في زمن خطي ، باستخدام خوارزمية تتضمن تحليلًا قويًا للاتصال في مخطط الاستلزام الخاص بها . تُعدّ مسألة الإرضاء من الدرجة الثانية حالة خاصة من مسألة TQBF لهذه الصيغ، حيث يكون كل مُكمِّم وجوديًا. [ 19 ] [ 20 ]
  • يوجد معالجة منهجية للإصدارات المقيدة من الصيغ المنطقية الكمية (التي تعطي تصنيفات من نوع شيفر) مقدمة في ورقة توضيحية لهوبي تشين. [ 21 ]
  • تم إثبات أن مسألة Planar TQBF، التي تعمم مسألة Planar SAT ، كاملة من حيث PSPACE بواسطة د. ليختنشتاين. [ 22 ]

ملاحظات ومراجع

  1. ↑ م. غاري ود. جونسون (1979). الحواسيب والاستعصاء: دليل لنظرية اكتمال NP . دبليو إتش فريمان، سان فرانسيسكو، كاليفورنيا. ISBN 0-7167-1045-5.
  2. ↑ أ. تشاندرا، د. كوزين، ول. ستوكمير (1981). "التناوب" . مجلة ACM . 28 (1): 114-133 . doi : 10.1145/322234.322243 . S2CID 238863413 . {{cite journal}}: صيانة CS1: أسماء متعددة: قائمة المؤلفين ( رابط )
  3. ↑ آدي شامير (1992). "Ip = Pspace" . مجلة 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.

انظر أيضاً