ملخص تقني: ما وراء الترميزات الجشعة: نهج مستقل عن النظرية لتعداد ليمات النظرية (T-lemmas) في SMT

1. بيان المشكلة

في مجال إرضاء التبعية مع نظريات (Satisfiability Modulo Theories - SMT)، يتطلب رفع تقنيات الاستنتاج البولياني (Boolean reasoning) غالباً توليد ليّمات نظرية (T-lemmas). هذه هي عبارات صالحة نظرياً (T-valid) تستبعد التعيينات التي تكون مرضية بوليانياً ولكنها غير متسقة مع النظرية (T-inconsistent).

بينما تقوم أدوات حل SMT القياسية بتوليد هذه الليمات "بشكل كسلان" (lazily) عند الطلب أثناء البحث، فإن بعض مهام SMT المعقدة — مثل استخراج الحد الأدنى لجوهر عدم الإرضاء (minimal unsat-core extraction)، و MaxSMT، وتجميع (compilation) الـ T-OBDDs أو الـ T-SDDs — تتطلب الحساب المسبق "الجشع" (eager) لمجموعة كاملة من ليمات النظرية مسبقاً.

تعتبر ترميزات SMT "الكلاسيكية" الجشعة الحالية غير كافية لهذا الغرض لأنها:

1. محددة لعدد قليل من النظريات البسيطة (مثل EUF، DL، LRA).
2. لا تلتزم بالجمع بين النظريات (theory combination).
3. غالباً ما تنتج أعداداً مفرطة من الليمات غير الضرورية.

حالياً، هناك نقص في الطرق المستقلة عن النظرية (theory-agnostic) لتعداد مجموعات كاملة من ليمات النظرية (T-lemmas) لصيغ عشوائية، لا سيما لتطبيقات تجميع المعرفة (Knowledge Compilation - KC) حيث يتم دفع العبء الحسابي إلى مرحلة "خارج الخط" (offline) لتمكين الاستعلامات في الوقت الفعلي ذات الوقت متعدد الحدود.

2. المنهجية

يقترح المؤلفون إطار عمل لتعداد ليمات النظرية (T-lemmas) يكون مستقلاً عن النظرية الأساسية. يبني النهج على طريقة أساسية تستخدم AllSMT (تعداد جميع التعيينات المتسقة مع النظرية) ويقدم ثلاثة تحسينات متعامدة وقابلة للتركيب لتعزيز القابلية للتوسع:

2.1 الأساس: تعداد AllSMT الكلي

يقوم النهج الأساسي (الخوارزمية 2) بإجراء تعداد AllSMT كلي وغير مسقط (non-projected) على الصيغة المدخلة $\phi[\alpha]$. يقوم بشكل تكراري بإيجاد التعيينات الكلية المتسقة مع النظرية، ثم يحظرها، ويجمع ليمات النظرية التي تعلمها الحل حتى تصبح الصيغة غير مرضية.

• القصور: يعتمد هذا النهج على تعداد التعيينات الكلية. وكما هو موضح في المثال 2، فإن التعداد الجزئي الساذج قد يفشل في توليد ليمات النظرية الضرورية لأن الحل قد لا يستكشف أبداً التعيين الكلي المحدد غير المتسق مع النظرية والذي يؤدي إلى تعارض (conflict). ومع ذلك، فإن تعداد جميع التعيينات الكلية غالباً ما يكون مستعصياً حسابياً بسبب الانفجار التوليفي.

2.2 التحسين 1: فرق تسد (Divide-and-Conquer - D&C)

للتخفيف من تكلفة التعداد الكلي، يقترح المؤلفون استراتيجية فرق تسد (الخوارزمية 3):

1. إجراء تعداد AllSMT جزئي لتفكيك فضاء البحث البولياني إلى مجموعة من التعيينات الجزئية المتسقة مع النظرية والمنفصلة ($M_{\alpha}^p$).
2. لكل تعيين جزئي $\mu \in M_{\alpha}^p$، إجراء تعداد AllSMT كلي على الصيغة المقيدة $\phi \land \mu$.
3. يتم تنفيذ عمليات التعداد الكلي بالتوازي.

• المنطق: هذا يحول عملية تعداد كلي واحدة ضخمة ومستعصية إلى خطوة تفكيك واحدة أرخص تليها العديد من عمليات التعداد الكلي الأصغر والقابلة للإدارة.

2.3 التحسين 2: التعداد المسقط (Projected Enumeration)

يلاحظ المؤلفون أن عدم الاتساق مع النظرية يتحدد حصرياً من خلال التعيين لـ ذرات النظرية ($\alpha_T$)، وليس الذرات البوليانية ($\alpha_B$).

• الطريقة: إجراء تعداد AllSMT مسقط فقط على $\alpha_T$ (الخوارزمية 4).
• الأساس النظري: يثبت المبرهنة 1 أن إسقاط التعداد على ذرات النظرية (T-atoms) ينتج مجموعة كاملة من ليمات النظرية.
• الفائدة: هذا يقلل بشكل كبير من أبعاد البحث. التعيين الواحد المتسق مع النظرية على $\alpha_T$ يمثل ما يصل إلى $2^k$ من التعيينات الكلية على مجموعة الذرات الكاملة (حيث $k$ هو عدد الذرات البوليانية)، مما يقلل بشكل كبير من استخدام الذاكرة وحجم عبارة الحظر (blocking clause).

2.4 التحسين 3: التقسيم المدفوع بالنظرية (Theory-Driven Partitioning)

إذا كان بالإمكان تقسيم مجموعة الذرات في $\phi$ إلى مجموعات منفصلة ($\alpha_1, \dots, \alpha_n$) بحيث لا تشترك أي ذرة في مجموعة واحدة في متغيرات أو رموز غير مفسرة مع ذرات في مجموعة أخرى، فيمكن تفكيك المشكلة بشكل أكبر (الخوارما 5).

• الطريقة: بناءً على الخاصية 1 والمبرهنة 2، يمكن تعداد ليمات النظرية بشكل مستقل لكل قسم. تقوم الخوارزمية بتقسيم الذرات تكرارياً، وتعداد الليمات لكل قسم مسقطاً على ذرات ذلك القسم، وتجميع النتائج.
• الفائدة: يسمح هذا بتفكيك تعداد كلي واحد إلى $n$ من عمليات التعداد المسقط المستقلة، مما يوفر تسريعاً محتملاً أسياً للمشكلات ذات المكونات المنفصلة.

3. المساهمات الرئيسية

1. إطار عمل مستقل عن النظرية: أول عرض صريح لطرق تعداد مجموعات كاملة من ليمات النظرية لأي نظريات، متجاوزاً الترميزات الجشعة المحددة بنظرية معينة.
2. تقنيات القابلية للتوسع: تقديم ثلاث تقنيات متعامدة:
   • فرق تسد: يوازي البحث عن طريق تفكيك الفضاء البولياني.
   • التعداد المسقط: يقلل أبعاد البحث بالتركيز على ذرات النظرية.
   • التقسيم: يستغل الانفصال الهيكلي في الصيغة لحل المشكلات الفرعية بشكل مستقل.
3. الضمانات النظرية: براهٍ رسمية (المبرهنتان 1 و 2) تثبت أن هذه التحسينات تحافظ على اكتمال مجموعة ليمات النظرية المطلوبة لاستبعاد جميع التعيينات غير المتسقة مع النظرية.
4. التكامل مع تجميع المعرفة: يعمل هذا العمل كتقنية تمكينية لرفع طرق تجميع المعرفة (تحديداً المخططات القرارية مثل OBDDs و SDDs) إلى مستوى SMT، معالجةً بذلك عنق الزجاجة المتمثل في تعداد ليمات النظرية.

4. النتائج التجريبية

تم تقييم التقنيات على مجموعتين من الاختبارات المرجعية:

• نماذج SMT(LRA) اصطناعية: 450 مشكلة تم إنشاؤها عشوائياً من [16].
• نماذج التخطيط الزمني (Temporal Planning): 90 ترميزاً لـ SMT لمجالات تخطيط "الرسام" (Painter domain).

مقاييس الأداء:

• كفاءة الوقت:
  • في الاختبارات الاصطناعية، حسّن فرق تسد (D&C) الأداء بما يصل إلى مرتبتين عشريتين مقارنة بالأساس، حيث حل 17 مشكلة إضافية ضمن المهلة الزمنية.
  • إضافة الإسقاط (Projection) حسّنت النتائج بشكل أكبر، حيث حلت 30 مشكلة أكثر من D&C وحدها وقللت الوقت بشكل كبير للحالات التي تم حلها مسبقاً.
  • التقسيم (Partitioning) لم يظهر تحسناً في البيانات الاصطناعية (نظراً لقلة المشكلات ذات الأقسام المنفصلة) ولكنه كان فعالاً للغاية في مشاكل التخطيط.
  • في مشاكل التخطيط، كان التقسيم هو العامل المهيمن، مما مكن من حل مشكلات بأفق (horizon) 5 كانت مستعصية سابقاً، محققاً تسريعاً بعدة مراتب عشرية.
• عدد الليمات:
  • مال D&C إلى إنتاج ليمات أكثر قليلاً بسبب التكرار المتوازي.
  • قلل الإسقاط والتقسيم عموماً من عدد الليمات المعدودة من خلال الحد من الاستكشاف المكرر وتوليد ليمات أقوى وأصغر.
• حجم الليمة:
  • أدى التقسيم في مشاكل التخطيط إلى ليمات نظرية أصغر بكثير (أقل عدداً في الليترالات)، ويرجع ذلك على الأرجح إلى التقليم المبكر للفروع غير المتسقة مع النظرية والتي تتضمن أقساماً محددة فقط.

5. الأهمية والادعاءات

يدعي البحث أن هذه التقنيات تعزز بشكل كبير كفاءة وقابلية توسع تعداد ليمات النظرية مقارنة بنهج AllSMT الأساسي.

• الدور التمكيني: الأهمية الرئيسية هي تمكين التطبيق العملي لتجميع المعرفة في SMT. يشير المؤلفون في عملهم السابق [16] إلى أن تعداد ليمات النظرية كان "عنق الزجاجة الرئيسي" لتجميع المخططات القرارية. ومن خلال حل هذا العنق، تمهد الطرق المقترحة الطريق لتوسيع نطاق تقنيات التجميع هذه لتشمل حالات معقدة من العالم الحقيقي.
• التواضع: يشير المؤلفون بحذر إلى أن التحسينات تعتمد على السياق. فعلى سبيل المثال، لم يساعد الإسقاط في مشاكل التخطيط لأن تعيينات ذرات النظرية كانت نتائج حتمية للتعيينات البوليانية في تلك الترميزات المحددة. وبالمثل، لم يحقق التقسيم فوائد إلا عندما سمحت بنية المشكلة طبيعياً بأقسام منفصلة.

باختصار، يوفر البحث مجموعة أدوات قوية ومستقلة عن النظرية لتعداد ليمات النظرية الجشع، محولاً خطوة كانت سابقاً مستعصية إلى عملية قابلة للتوسع، مما يسهل تطبيقات SMT المتقدمة مثل MaxSMT وتجميع المعرفة.