في عالم الكمبيوتر، تعد مشاكل تسمية الحد الأدنى للمدى (Minimum Span Antibandwidth) وعدم التداخل (Antibandwidth) من التحديات التي تواجه الباحثين والمطورين. فهذه المشاكل تم تصنيفها على أنها NP-hard، مما يعني أنها تتطلب تقنيات متقدمة للغاية لحلها.

تتمحور هذه المشاكل حول تعيين تسميات لأعلى وأدنى النقاط (vertices) في الرسم البياني (graph) بحيث يتم تحقيق أقصى مسافة (distance) بين التسميات المخصصة للنقاط المجاورة. على الرغم من الأبحاث العميقة التي أجريت حول هذه القضايا، إلا أن منظور الحد الأدنى للمدى - حيث يتم تحديد مسافة دنيا ثابتة ويتم السعي لتقليل نطاق التسميات - لم يحظَ بالاهتمام الكافي.

في هذا المقال، نقوم بتقديم إطار عمل موحد يعتمد على المنطق البوليني (Boolean Satisfiability, SAT) لمعالجة مشاكل تسمية الحد الأدنى للمدى وعدم التداخل (MSABL/MSCABL). حيث يتم صياغة هذه المشاكل كسلسلة من مسائل القرار وتتطلب استراتيجيات محددة لتسريع عملية البحث.

تتضمن هذه الاستراتيجيات حل SAT المتوازي، الذي يقوم بفحص نطاقات مرشحة متعددة في وقت واحد، وحل SAT التزايدي، الذي يعيد استخدام حالة SAT واحدة مع تقييد متقدم لمجال التسميات.

لقد أظهرت النتائج المستندة إلى أمثلة مرجعية من مجموعة مصفوفات هارويل-بوينغ (Harwell-Boeing Sparse Matrix Collection) أن الأساليب المعتمدة على SAT تنافس بقوة من حيث جودة الحل، حيث حقق الحل المتوازي أفضل أداء لMSCABL، بينما كان الحل التزايدي الأفضل لـMSABL.

كما أظهرت النتائج أن الأساليب الجديدة تتنافس بقوة مع CPLEXCP، وتتفوق بشكل ملحوظ على CPLEXMIP وGurobi في سياق MSCABL. إن هذه النتائج تؤكد على فعالية استخدام حلول SAT كمنهج دقيق لمشاكل MSABL وMSCABL.