تقدم هذه الورقة خوارزمية جديدة لحل مسائل QBF تعتمد على تعميم تعداد المجموعات الضاربة الضمنية، وتثبت من خلال التجارب أنها تنافس وتتفوق غالباً على الحلول المتطورة الحالية.
تخيل لعبة كونية عملاقة من "نعم أو لا" تُلعَب باستخدام مجموعة من أوراق اللعب، حيث يسيطر خصم مشاكس على بعض الأوراق، بينما يسيطر بطل ذكي على الأوراق الأخرى. هذا هو عالم "صيغ بولين الكمية" (QBF)، وهو فرع من علوم الحاسوب يقع خلف ألغاز "الاشباع" (SAT) الشهيرة مباشرة. وبينما تسأل لغز "الاشباع" التقليدي: "هل يمكننا قلب هذه المفاتيح لجعل الآلة بأكملها تضيء؟"، تضيف صيغ (QBF) طبقة من الدراما: "هل يمكن للبطل أن يفوز دائمًا، بغض النظر عن كيفية محاولة الخصم تخريب المفاتيح؟". هذا ليس مجرد لغز ذهني؛ بل هو المحرك الرياضي وراء التحقق مما إذا كانت السيارات ذاتية القيادة ستتصادم، أو ما إذا كانت الروبوتات قادرة على تخطيط مهام معقدة، أو ما إذا كانت الألعاب التي يلعبها شخصان تمتلك استراتيجية فوز مضمونة. ولأن هذه المشكلات صعبة للغاية، فإن حلها يشبه محاولة العثور على إبرة في كومة قش يتغير شكلها باستمرار.
هنا يأتي فريق جديد من الباحثين الذين قرروا مواجهة هذه الفوضى ليس ببناء آلة أكبر وأكثر تعقيدًا، بل بلعب لعبة ذكية من "اختيار البنود". فكر في اللغز كأنه قائمة ضخمة من القواعد (البنود). أدرك الباحثون أنه بدلًا من محاولة حل الأمر برمته دفعة واحدة، يمكنهم استخدام "حلّال" (solver) قياسي لأسئلة "نعم/لا" (حلّال SAT) كحكم لمساعدتهم في اختيار وتحديد أي القواعد يجب الاحتفاظ بها أو التخلص منها في كل خطوة من خطوات اللعبة. طريقتهم الجديدة، التي تسمى "QESTO"، تعامل المشكلة كمعركة استراتيجية حيث الهدف هو العثد على مجموعة من القواعد التي يمكن للبطل تحقيقها مهما فعل الخصم.
تقدم الورقة البحثية خوارزمية "QESTO"، وهي خوارزمية مبتكرة مصممة لحل هذه الألغاز المنطقية المعقدة. قام المؤلفون أولاً بتفكيك المشكلة إلى نسخة مبسطة من لاعبين اثنين (خصم واحد وبطل واحد)، وأظهروا أن طريقتهم مرتبطة رياضيًا بمفهوم يسمى "مجموعات الضرب الضمنية" (implicit hitting sets) — وهي طريقة منمقة للقول بأنهم يبحثون عن أصغر مجموعة من القواعد التي، إذا كُسرت، ستؤدي إلى فشل النظام بأكمله. ثم وسعوا هذه الفكرة للتعامل مع الألغاز التي تحتوي على أي عدد من اللاعبين وطبقات من سيناريوهات "ماذا لو".
في تجاربهم، بنى الفريق نموذجًا أوليًا لـ "QESTO" واختبروه مقابل أفضل الحلّالات الموجودة حاليًا باستخدام مجموعة من المعايير القياسية. تشير النتائج إلى أن "QESTO" تنافسي للغاية. ففي مجموعة محددة من ألغاز اللاعبين الاثنين، تمكن نموذجهم الأولي بالفعل من حل أكبر عدد من الحالات، متفوقًا بذلك على الأدوات الرائدة الأخرى. وفي مجموعة أوسع وأكثر تعقيدًا من المعايير، جاء في المركز الثاني، خلف الحلّال الذي لا يستخدم تنسيق "قائمة القواعد" القياسي مباشرة. ويشير المؤلفون إلى أن هذا النهج قوي بشكل خاص لأنه يعتمد على حلّال (SAT) يعمل كـ "صندوق أسود"، مما يعني أنه إذا اخترع شخص ما حلّال (SAT) أفضل غدًا، فإن "QESTO" سيصبح أفضل تلقائيًا دون الحاجة إلى إعادة كتابته. ورغم أن الورقة لا تدعي أنها حلت كل مشكلات (QBF) الموجودة، إلا أن عمليات المحاكاة تشير إلى أن هذه الطريقة الجديدة في اختيار وإلغاء اختيار القواعد هي اتجاه قوي وواعد لمستقبل الاستدلال الآلي.
ملخص تقني: حل مسألة QBF عن طريق اختيار الـ Clauses
بيان المشكلة تتناول الورقة البحثية مشكلة حل صيغ بول (QBF)، وتحديداً تلك التي تأتي في الصيغة الطبيعية المسبقة لـ Conjunctive Normal Form (PQCNF). إن تقرير صحة صيغ QBF هو مسألة من فئة PSPACE-complete، وتغطي تطبيقات مثل التحقق من النماذج (model checking)، والتخطيط، والألعاب ذات اللاعبين. وبينما حقق حل مسائل SAT نجاحاً كبيراً، لا يزال حل مسائل QBF يمثل تحدياً. تنقسم النهج الحالية عموماً إلى فئتين: التعلم القائم على الصراع/الحل (توسيع تعلم الـ clause في SAT)، والأسالق القائمة على التوسيع (تحويل QBFs إلى مسائل SAT). يقترح المؤلفون نهجاً جديداً يستفيد من ثنائية المجموعات الضاربة (hitting sets) وتعداد المجموعات الضاربة الضمنية لحل مسائل QBF.
المنهجية المنهجية الأساسية، المسماة QESTO (محلل اختيار الـ clause لـ Qbf)، تعامل حل QBF كلعبة بين لاعب عالمي (universal player) ولاعب وجودي (existential player). تعمل الخوارزمية من خلال اختيار وإلغاء اختيار الـ clauses بشكل متكرر عند مستويات كمية مختلفة باستخدام محلل SAT كأداة استعلام (oracle).
QBF ذو مستويين (∀∃): طور المؤلفون أولاً خوارزمية للصيغ ذات مستويين من الكميات. لقد أقاموا رابطاً بين حل ∀X∃Y.ϕ وتعداد المجموعات الضاربة الضمنية.
الآلية: تحافظ الخوارزمية على مجموعة من متغيرات الاختيار sC لكل clause C. يُستخدم محلل SAT لإيجاد مجموعة من الـ clauses (المشار إليها بـ S) التي يمكن "اختيارها" (أي يمكن جعل متغيراتها العالمية false).
التحقق: إذا كان الجزء الوجودي من الـ clauses المختارة غير قابل للإرضاء (unsatisfiable)، فإن اللاعب العالمي يفوز (الصيغة خاطئة). إذا كان قابلاً للإرضاء، تتعلم الخوارزمية من التعيين المرضي لمنع الاختيارات المستقبلية لمجموعات فرعية من الـ clauses التي تم إرضاؤها، مما يؤدي فعلياً للبحث عن مجموعة غير مرضية دنيا (Minimal Unsatisfiable Set - MUS) للجزء الوجودي المقيد بالقواعد العالمية.
العلاقة بالنظرية: تبيّن أن هذه العملية هي تطبيق لمبدأ ثنائية المجموعة الضاربة، حيث تتنقل الخوارزمية عبر المجموعات المرضية القصوى (Maximally Satisfiable Sets - MSSes) لإيجاد الـ MUSes.
QBF عام (بادئات عشوائية): تم تعميم النهج على بادئات كمية عشوائية (Q1X1…QnXn.ϕ).
الرؤية من منظور نظرية الألعاب: تحاكي الخوارزمية لعبة مكونة من n من الجولات. في كل مستوى i، يقوم اللاعب Qi باختيار أو إلغاء اختيار الـ clauses بناءً على قواعد محددة:
يمكن اختيار clause في المستوى k فقط إذا تم اختياره في جميع المستويات السابقة وكانت جميع متغيراته في المستوى k مضبوطة على false.
يمكن إلغاء اختيار clause إذا تم إلغاء اختياره سابقاً أو إذا تم ضبط متغير في المستوى k على true.
منطق اختيار الـ clause: تحافظ الخوارزمية على شروط Ci لكل مستوى لمنع الخيارات التي تؤدي إلى خسارة اللاعب الحالي.
تحليل الصراع: عندما يصبح الشرط غير قابل للإرضاء (مما يشير إلى خسارة أحد اللاعبين)، تقوم الخوارزمية بإجراء "تحليل خسارة" باستخدام الـ conflict clause النهائي من محلل SAT.
الخسارة الوجودية: إذا خسر اللاعب الوجودي، تحدد الخوارزمية مجموعة من الـ clauses المختارة التي تسببت في عدم الإرضاء، وتقوم بالتراجع (backtrack) إلى أعلى مستوى كمي لمتغير وجودي ضمن تلك الـ clauses لفرض إلغاء الاختيار.
الخسارة العالمية: إذا خسر اللاعب العالمي (إلغاء اختيار جميع الـ clauses)، تتراجع الخوارزمية إلى أعلى مستوى استطاع فيه اللاعب العالمي منع إلغاء الاختيار.
التعلم: تتعلم الخوارزمية قيوداً جديدة (clauses) لمنع تكرار نفس التكوين الخاسر، بشكل مشابه لتعلم الصراع المدفوع في SAT ولكن مع ربطه بمتغيرات الاختيار.
المساهمات الرئيسية
خوارزمية مبتكرة (QESTO): تقدم الورقة QESTO، وهو محلل QBF يستخدم محلل SAT كأداة (black-box oracle) لاختيار أو إلغاء اختيار الـ clauses عند كل مستوى كمي.
الربط النظري بالمجموعات الضاربة: أثبتت الورقة وجود صلة رسمية بين حل QBF وتعداد المجموعات الضاربة الضمنية، مما يعمم مبدأ ثنائية المجموعة الضاربة (المستخدم عادة في حساب MUS و MaxSAT) إلى مجال PSPACE.
الارتباط بـ CEGAR: تم ربط نسخة المستويين بأساليب التحسين المستند إلى المثال المضاد (Counter-Example Guided Abstraction Refinement - CEGAR)، وتحديداً AReQS، رغم أن التعميم (QESTO) يختلف بشكل كبير عن التعميمات التكرارية مثل RAReQS من خلال تجنب إدخال متغيرات جديدة والحفاظ على عدد ثابت من المحللات.
الميزة الهندسية: يعتمد النهج كلياً على محاللات SAT الموجودة. إذا تم تطوير محلل SAT أفضل، يمكن استبداله مباشرة في التنفيذ دون تعديل منطق QBF.
النتائج التجريبية قام المؤلفون بتنفيذ نموذج أولي بلغة ++C باستخدام MiniSat 2.2 وتم تقييمه باستخدام مجموعة اختبارات QBFLIB (2014) ومسار 2QBF (2010).
اختبارات 2QBF: حل QESTO أكبر عدد من الحالات (53 من أصل 65)، متفوقاً على DepQBF (30) و GhostQ (43). كان قريباً جداً من AReQS (52)، وهو أمر متوقع نظراً لعلاقتهما النظرية.
اختبارات QBFLIB: سيطر GhostQ (محلل غير قائم على CNF) على النتائج (137 حالة)، يليه QESTO (133). حل كل من DepQBF و RAReQS نحو 128 و 129 حالة على التوالي.
ملاحظة: تشير النتائج إلى أنه بينما يعد QESTO تنافسياً وقوياً، فإن تمثيل مسائل QBF حصرياً بصيغة CNF قد يكون عائقاً مقارنة بالأساليب غير القائمة على CNF مثل GhostQ.
الأهمية والادعاءات تدعي الورقة أن QESTO يمثل نهجاً جديداً لحل مسائل QBF وهو نهج ذو أهمية نظرية وتنافسية عملية.
نظرياً: يمدد مبدأ ثنائية المجموعة الضاربة من NP (الخاص بـ MUS/MSS) إلى PSPACE (الخاص بـ QBF)، مما يوفر منظوراً جديداً لبنية المسألة.
عملياً: الخوارزمية "تنافس، وغالباً ما تتفوق على أحدث التقنيات" في مجالات محددة (خاصة 2QBF).
التواضع: يقر المؤلفون بأن نهجهم القائم على CNF قد تفوق عليه محلل GhostQ غير القائم على CNF في مجموعة QBFLIB العامة. وقد ذكروا صراحة أن العمل المستقبلي يجب أن يبحث في تطبيق QESTO على صيغ غير قائمة على CNF ودمج تحسينات مثل المتغيرات النقية (pure literals) أو تبعيات المتغيرات. هم لا يدعون أن QESTO هو الأفضل مطلقاً لجميع حالات QBF، بل هو بديل قوي ومبتكر يربط بين نماذج الحل المختلفة.