ملخص تقني: حساب المقتضيات القصيرة لـ SAT عبر ترميزات Ising/QUBO

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

تتطلب العديد من مهام الاستنتاج، بما في ذلك التفسير، والتشخيص، وضغط النماذج، تعيينات جزئية مرضية قصيرة (المقتضيات/implicants) بدلاً من التعيينات الكلية. في هذه السياقات، تعمل المتغيرات غير المعينة كقيم "لا تهم" (don't-cares) حقيقية، وغالباً ما يكون جزء فقط من المتغيرات (المتغيرات المرئية) ذا صلة دلالية، بينما تعمل المتغيرات الأخرى كدعم خفي.

بينما تقوم أدوات حل SAT الحديثة بحساب التعيينات الكلية المرضية بكفاءة، فإن استخراج المقتضيات القصيرة يتطلب عادةً استدعاءات متكررة لـ SAT أو معالجة لاحقة مخصصة. وبالمثل، فإن صياغات SAT-to-Ising/QUBO القياسية محدودة بطبيعتها: فهي تربط صيغ CNF بدوال طاقة تربيعية حيث تتوافق الحالات الأرضية مع التعيينات الكلية. يخصص نموذج Ising/QUBO قيمة لكل سبين (spin)، ويفتقر إلى تمثيل أصيل للمتغيرات "غير المعينة". بناءً على ذلك، ظل حساب المقتضيات القصيرة تاريخياً متروكاً لخوارزميات خارجية بدلاً من التقاطه داخل نموذج التحسين التربيعي نفسه.

2. المنهجية

يقترح المؤلفون إطار عمل للتحسين الموحد يدعم أصيلاً التعيينات الجزئية ثلاثية القيم (صواب، خطأ، غير معين) ضمن نموذج Ising/QUBO تربيعي.

2.1 التمثيل ثنائي القطبية

لتمثيل المتغيرات غير المعينة، يقدم إطار العمل ترميزاً ثنائي القطبية. لكل متغير قضائي $A_i$، يتم استخدام سبينات ثنائية $(p_i, n_i)$:

• $(1, 0) \implies A_i = \top$ (صواب)
• $(0, 1) \implies A_i = \bot$ (خطأ)
• $(0, 0) \implies A_i$ غير معين (لا يهم)
• $(1, 1) \implies حالة غير متسقة (محظورة)

يتم إضافة عقوبة اتساق دلالي $M \cdot p_i n_i$ لمنع الحالة غير المتسقة.

2.2 ترميز البنود (Clause Encoding)

يتم ترميز البنود باستخدام دوال عقوبة تربيعية قياسية. بالنسبة لبند $C_k = (\ell_1 \lor \ell_2 \lor \ell_3)$، يتم ربط الحروف (literals) بسبينات القطبية المقابلة لها. وللحفاظ على الشكل التربيعي، يتم إدخال متغير مساعد $c_k$ لالتقاط الحالة التي يكون فيها أول حرفين خطأ. تقوم دالة الطاقة بمعاقبة التكوينات التي تكون فيها جميع الحروف خطأ (أي جميع السبينات المقابلة هي 0).

2.3 التشتت ودالة الهدف

يتم إضافة حد تشتت (sparsity term) إلى دالة الطاقة: $E_{sparse} = \gamma \sum (p_i + n_i)$. يعمل هذا الحد على معاقبة السبينات النشطة، مما يوجه المحسن نحو التكوينات ذات المتغيرات المعينة الأقل (المقتضيات الأقصر).
دالة الطاقة الإجمالية هي:
$$E_F = \sum M p_i n_i + \sum E_{clause}(k) + \gamma \sum (p_i + n_i)$$

2.4 أنظمة الأوزان (Weight Regimes)

يحدد البحث شروطاً نظرية على الأوزان ($\lambda$ لعقوبات البنود، $M$ للاتساق، $\gamma$ للتشتت) لضمان الصحة. تحديداً، إذا كان $\lambda > n\gamma$ و $M > n\gamma$ (حيث $n$ هو عدد المتغيرات)، فإن الحالات الأرضية لدالة الطاقة تتوافق تماماً مع المقتضيات ذات الحد الأدنى من الكاردينالية (minimum-cardinality implicants).

2.5 التقلص والإسقاط

• تقلص المقتضيات (Implicant Shrinking): بالنظر إلى تعيين كلي مرضٍ، يقوم إطار العمل بتقييد مساحة البحث عن طريق تثبيت سبينات القطبية "المعاكسة" عند 0. يسم la هذا للمحسن فقط إسقاط الحروف من التعيين الحالي، مما يجد أقصر تعيين فرعي يظل مقتضىً صالحاً.
• الإسقاط (Projection): للتركيز على مجموعة فرعية من المتغيرات المرئية $P$، يتم تطبيق عقوبة التشتت فقط على المتغيرات في $P$. تظل المتغيرات الخفية $H$ غير مقيدة بالتشتت، وتعمل كدعم مساعد حر. يسمح هذا للنموذج بإيجاد تعيينات قصيرة فوق $P$ مع تلبية الصيغة عبر $H$.

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

1. ترميز أصيل ثلاثي القيم: ترميز SAT-to-Ising/QUBO يمثل أصيلاً التعيينات الجزئية (صواب/خطأ/غير معين) عبر دلالات القطبية المزدوجة، مما يلغي الحاجة إلى معالجة لاحقة خارجية لتفسير حالات "غير المعين".
2. متغيرات الهدف المرنة: صياغات QUBO حيث يتم تحقيق تقلص المقتضيات عبر قيود القطبية، ويتم تحقيق الإسقاط عبر تقييد عقوبات التشتت للمتغيرات المرئية، وكل ذلك ضمن هيكل نموذج تربيعي ثابت واحد.
3. الضمانات النظرية: تحديد أنظمة أوزان محددة ($\lambda > n\gamma, M > n\gamma$) تضمن أن الحالات الأرضية تتوافق مع المقتضيات ذات الحد الأدنى من الكاردينالية. يوفر البحث معياراً للتعرف على المقتضيات الصالحة مباشرة من قيمة الطاقة النهائية.
4. التحقق التجريبي: تقييم باستخدام التلدين المحاكي (Simulated Annealing) على نماذج 3-SAT عشوائية وصيغ غير CNF، مما يثبت قدرة الترميز على إنتاج تعيينات جزئية قصيرة وتحقيق الحد الأدنى من خلال التحسين المتكرر.

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

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

• 3-SAT عشوائي: نماذج قابلة للإرضاء بكثافة منخفضة للبند إلى المتغير ($m/n = 1.5$).
• صيغ غير CNF: صيغ بولينية تم تحويلها إلى CNF عبر تحويلات Tseitin/Plaqtisted-Greenbaum، مما خلق بيئة مسقطة مع متغيرات مساعدة خفية.

النتائج الرئيسية:

• التراص (Compactness): في 3-SAT العشوائي، يترك الترميز حوالي ثلث المتغيرات غير معينة في المتوسط مع الحفاظ على الإرضاء.
• الحد الأدنى (Minimality): بينما يجد SA الأساسي غالباً تعيينات ذات حد أدنى من الكاردينالية في النماذج الصغيرة إلى المتوسطة، فإن معدلات النجاح تنخفض مع زيادة حجم المشكلة بسبب النهايات الصغرى المحلية. ومع ذلك، فإن التحسين المتكرر (تجميد أفضل حل وإعادة تشغيل SA للتقلص أكثر) يحسن النتائج بشكل كبير.
• الحد الأدنى مقابل الحد الأدنى من الكاردينالية: يحقق التحسين المتكرر الحد الأدنى من الاحتواء (المقتضيات الأولية) باحتمالية عالية. أما تحقيق الحد الأدنى من الكاردينالية (الحد الأدنى العالمي للحجم) فهو أصعب ولكنه يُلاحظ تكراراً، خاصة في اختبارات غير CNF حيث تسمح البنية باكتمالات خفية موحدة.
• البيئة المسقطة: في وضع الإسقاط، نجح الأسلوب في استعادة تعيينات الحد الأدنى من الكاردينالية فوق المتغيرات المرئية، حتى مع وجود نسبة عالية من المتغيرات المساعدة الخفية (65-70% من إجمالي المتغيرات).

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

يزعم البحث أن هذا الإطار يقدم نهج تحسين موحد لحساب التعيينات الجزئية القصيرة، مستبدلاً الحاجة إلى برامج فرعية للتقلص في عمليات AllSAT أو سلاسل التفسير.

• الأهمية النظرية: يجسر الفجوة بين الطبيعة "الكلية للتعيين" لنماذج Ising ومتطلبات "التعيين الجزئي" للعديد من مهام الاستنتاج عبر تقديم تمثيل ثنائي القطبية مع أنظمة أوزان مثبتة للحد الأدنى.
• الأهمية العملية: يعمل الترميز كـ "بديل جاهز للاستخدام" لخطوات التقلص في تدفقات العمل الحالية. يؤكد المؤلفون أن النهج قوي تحت محركات التحسين العامة (مثل التلدين المحاكي) ولا يتطلب أجهزة متخصصة لإثبات الصلاحية الدلالية، رغم إشارتهم إلى أن الملدنات الكمومية أو آلات Ising المتخصصة قد تعطي نتائج أفضل.
• القيود: يقر المؤلفون بتواضع بأن المحسنات الاستدلالية (Heuristic optimizers) قد تقع في نهايات صغرى محلية، رغم أن الترميز يضمن نظرياً حالات أرضية ذات حد أدنى من الكاردينالية. علاوة على ذلك، في البيئة المسقطة، يفرض الترميز "شاهداً موحداً" (تعيين خفي واحد لجميع التكميلات المرئية)، وهو مطلب أكثر صرامة من دلالات المقتضى المسقط القياسية، لكن المؤلفين يجادلون بأن هذا ينطبق على العديد من تحويلات غير CNF العملية.

يضع هذا العمل نفسه كتحقق دلالي من الترميزات التربيعية للتعليل الجزئي، موضحاً أنه مع ضبط المعلمات والتحسين المتكرر، يمكن لنماذج Ising/QUBO حساب المقتضيات الدنيا والحد الأدنى من الكاردينالية بفعالية.