ملخص تقني: ترميزات SAT لتلوين عرض النطاق الترددي

تعريف المشكلة

تعد مشكلة تلوين عرض النطاق الترددي (BCP) تعميماً لمشكلة تلوين الرسم البياني (GCP)، حيث تحمل الحواف أوزانًا صحيحة موجبة $d(u, v)$. والهدف هو تعيين لون $c(v) \in \mathbb{N}$ لكل رأس $v$ بحيث يتم استيفاء قيد المسافة $|c(u) - c(v)| \ge d(u, v)$ لكل حافة $\{u, v\} \in E$. والهدف هو تقليل المدى (span)، والذي يُعرف بأنه الحد الأقصى للون المعين لأي رأس.

تنشأ مشكلة BCP بشكل طبيعي في مشكلات تخصيص التردد (FAP) لشبكات الاتصالات اللاسلكية والخلوية، حيث تمثل الرؤوس أجهزة الإرسل وتمثل أوزان الحواف الحد الأدنى من الفصل الترددي المطلوب لتجنب التداخل الكهرومغناطيسي. وبينما توجد طرق استكشافية (metaheuristic)، إلا أنها تفتقر إلى ضمانات المثالية. وقد تمت دراسة الطرق الدقيقة القائمة على البرمجة الخطية الصحيحة (ILP) والبرمجة بالقيود (CP)، لكن صياغات ILP غالباً ما تعاني من نمو عدد القيود مع أوزان الحواف. مؤخراً، ظهرت النهج القائمة على SAT كأحدث التقنيات للحل الدقيق، ومع ذلك، لا يزال مجال التصميم الخاص بترميزات SAT المصممة خصيصاً لـ BCP غير مستكشف إلى حد كبير.

المنهجية

تقدم الورقة دراسة تصميم منهجية لترميزات SAT لـ BCP، حيث تقترح إطار عمل موحداً يستكشف ست طرق ترميز متميزة منظمة في ثلاث فئات. يقيم الإطار تأثير ثلاثة ميزات قابلة للضبط: الحل التزايدي (incremental solving)، كسر التماثل (symmetry breaking)، واستراتيجيات عرض الكتلة (block width strategies).

1. فئات الترميز

ينفذ الإطار ويقارن طرق الترميز التالية:

• ترميزات المتغير الواحد (1G, 1L): تستخدم متغيرات الترتيب لتعريف تعيينات الألوان بشكل ضمني.
  • 1G (الأكبر من): يستخدم متغيرات $y_{u,j}$ حيث $y_{u,j} = \text{true} \iff c(u) \ge j$.
  • 1L (الأصغر من): يستخدم متغيرات $y_{u,j}$ حيث $y_{u,j} = \text{true} \iff c(u) \le j$.
  • تمتلك هذه الطرق عدداً تقاربياً من البنود (clauses) بمقدار $O(k(n+m))$، وهي مستقلة عن أوزان الحواف.
• ترميزات المتغيرين (2G, 2L): تحافظ هذه الطرق صراحةً على كل من متغيرات التعيين ($x_{u,j}$) ومتغيرات الترتيب ($y_{u,j}$) للسماح بقيود مسافة أكثر مباشرة.
  • 2G/2L: تمتلك دلالات مشابهة لـ 1G/1L ولكنها تتضمن قيود قناة (channeling constraints) تربط بين متغيرات $x$ و $y$.
• ترميزات الكتلة (X, Xa): تقوم هذه الطريقة بتقسيم نطاق الألوان إلى كتل ذات عرض ثابت واستخدام متغيرات النطاق المساعدة ($R_{u,a,b}$) لتمثيل مجموع متغيرات التعيين داخل الكتل.
  • X: تقوم بترميز عمليات الطرح (المطلوبة لجمع النطاقات داخل الكتل) مباشرة دون متغيرات مساعدة.
  • Xa: تقدم متغيرات مساعدة لتمثيل حدود الطرح، مما يسمح بإعادة استخدام البنود.
  • تهدف ترميزات الكتلة إلى تقليل عدد البنود لقيود المسافة، خاصة عندما تكون أوزان الحواف كبيرة.

2. الميزات القابلة للضبط

• الحل التزايدي: يختبر الإطار ما إذا كان إعادة استخدام البنود المتعلمة عبر التكرارات (مع تناقص الحد الأعلى للمدى) يحسن الأداء. يتم تنفيذ ذلك باستخدام افتراضات SAT.
• كسر التماثل: يتم تطبيق تقنية قائمة على الانعكاس على الرأس ذو الدرجة الأعلى، مما يقيد لونه إلى النصف الأدنى من نطاق المدى ($c(h) \le \lfloor k/2 \rfloor$). هذا يستغل خاصية أنه إذا كان $c$ تلويناً صالحاً، فإن $c'(v) = k+1-c(v)$ هو أيضاً تلوين صالح.
• استراتيجيات عرض الكتلة: بالنسبة لترميزات الكتلة، يقارن الإطار بين الكتل ثابتة العرض (الافتراضي $w=8$) والكتل متغيرة العرض (حيث يتم تحديد العرض بناءً على أقصى وزن حافة متصل بالرأس).

3. الإعداد التجريبي

تقيم الدراسة 36 تكويناً متميزاً (مجموعات من طرق الترميز الست والميزات) على 5 sets من 51 حالة مرجعية:

• مجموعة GEOM: 33 رسماً بيانياً عشوائياً هندسياً (GEOM20 إلى GEOM120).
• مجموعة MS-CAP: 18 حالة مشتقة من مشكلات تخصيص التردد في الشبكات الخلوية.
• المحلل (Solver): CaDiCaL 1.9.5 مع حد زمني قدره 3600 ثانية لكل حالة.
• الأساس (Baseline): تتم المقارنات مع ترميزات SAT المتطورة POP-S-B و POPH-S-B (Faber et al., 2024).

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

الأداء العام

يحقق الإطار المقترح أداءً يضاهي أحدث ما توصل إليه العلم. حقق أفضل تكوين في الأداء، وهو ترميز الكتلة Xa (مع عرض ثابت، حل تزايدي، وكسر التماثل)، حل جميع الـ 51 حالة بإجمالي وقت قدره 2721.3 ثانية. ويمثل هذا انخفاضاً بنسبة 6.3% في إجمالي الوقت مقارنة بالأسلوب السابق المتطور POPH-S-B (2904.6 ثانية) وانخفاضاً بنسبة 17.7% مقارنة بـ POP-S-B (3307.5 ثانية).

أداء الحالات الصعبة (GEOM120b)

هناك نتيجة حاسمة تتعلق بالحالة الأكثر صعوبة، GEOM120b:

• فشلت الطرق السابقة (POPH-S-B و POP-S-B) في حل GEOM120b للوصول إلى المثالية المثبتة ضمن الحد الزمني لساعة واحدة.
• نجحت ترميزات الكتلة (X و Xa) المقترحة في حل GEOM120b إلى المثالية في حوالي 1000 ثانية (تحديداً، حل تكوين Xa الأساسي الحالة في 851.4 ثانية، بينما حل Xa المحسن بالكامل الحالة في 1011.6 ثانية).
• يوضح هذا عامل تسريع قدره 2 ضعف تقريباً مقارنة بأفضل مناهج SAT السابقة لهذه الحالة المحددة.

تأثيرات التفاعل

تكشف الدراسة عن تأثيرات تفاعل كبيرة بين اختيار الترميز وتكوينات المحلل:

• الحل التزايدي: يوفر تسريعاً كبيراً لـ ترميزات الكتلة (على سبيل المثال، تحسن بنسبة 24.4% لـ Xa) لأن هيكل الكتلة المتدرج يظل مستقراً إلى حد كبير مع تناقص المدى. وعلى العكس من ذلك، لا يقدم أي فائدة (أو قد يؤدي إلى تدهور) لـ ترميزات المتغير الواحد (1G, 1L) لأن قيود الترتيب يتم إعادة تعريفها بالنسبة للحد الأعلى الجديد، مما يبطل البنود المتعلمة.
• كسر التماثل: تعتمد فعاليته بشكل كبير على نوع الترميز. فهو يحسن الأداء بشكل كبير لـ POP-S-B (تسريع بنسبة 24.5%) و 1L (تسريع بنسبة 13.2%)، ولكنه يقلل من الأداء لـ 2G (تباطؤ بنسبة 11.9%) و POPH-S-B (تباطؤ بنسبة 11.4%).
• عرض الكتلة: كان الاختيار بين عرض الكتلة الثابت والمتغير له تأثير ضئيل (أقل من 1.2% فرق) على الـ 50 حالة القياسية، مما يشير إلى أن تعلم بنود المحلل يتكيف جيداً مع كلتا الاستراتيجيتين.

حجم الترميز مقابل الكفاءة

على عكس الحدس بأن عدد أقل من المتغيرات والبنود يؤدي إلى حل أسرع، فإن ترميز Xa (الذي يولد 7 أضعاف المتغيرات و5.5 أضعاف البنود مقارنة بترميز 1G الأكثر إيجازاً) حقق أسرع أوقات حل. وهذا يدعم مبدأ أن المتغيرات المساعدة يمكن أن تعزز الانتشار الوحدوي (unit propagation)، مما يخلق "اختصارات" للمحلل لاستنتاج التبعات بشكل أكثر كفاءة.

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

تدعي الورقة أن دراسة التصميم المنهجية التي قدمتها تملأ فجوة في الأدبيات المتعلقة بترميزات SAT لـ BCP. وبينما تمت دراسة كسر التماثل والحل التزايدي لـ GCP، فإن تطبيقهما وتفاعلهما مع ترميزات BCP المحددة لم يكن محل بحث سابقاً.

تتمثل المساهمات الرئيسية فيما يلي:

1. حل ما لم يُحل: يعد الإطار الأول الذي يحل حالة GEOM120b المرجعية للوصول إلى المثالية المثبتة ضمن إطار زمني معقول، وهي مهمة لم تتمكن الطرق الدقيقة السابقة من إكمالها في ساعة واحدة.
2. إطار عمل موحد: يوفر دراسة مقارنة شاملة لست طرق ترميز وميزاتها القابلة للضبط، موضحاً أن ترميزات الكتلة هي الأفضل للحالات الأكثر صعوبة، بينما توفر ترميزات الترتيب (مثل 2L و 1G) مقايضة مواتية بين تعقيد التنفيذ والأداء للحالات العامة.
3. رؤى التفاعل: تسلط الورقة الضوء على أن ميزات الترميز لا تعمل بشكل مستقل. وتحديداً، يجب اختيار الحل التزايدي وكسر التماثل بعناية بناءً على نوع الترميز المحدد، حيث يمكن أن تؤدي إلى تأثيرات تآزرية أو تضادية.

خلص المؤلفون إلى أنه بينما توفر ترميزات الكتلة أفضل أداء في الحالات الأكثر تحدياً، فإن الاستكشاف المنهجي لخيارات تصميم الترميز أمر ضروري لتطوير حلول BCP دقيقة. ويُقترح كعمل مستقبلي توسيع الإطار ليشمل مشكلة تلوين تعدد الألوان لعرض النطاق الترددي (BMCP) وتطوير آليات اختيار التكوين التكيفية.