💻 computer science

Compact SAT and MaxSAT Encodings for Business-to-Business Meeting Scheduling with Idle-Time Balancing

تقدم هذه الورقة ترميزات SAT وMaxSAT مدمجة لجدولة اجتماعات الأعمال بين الشركات، والتي تستخدم تصفية النطاق والمتغيرات المشتركة لتقليل عدد البنود واستهلاك الذاكرة بشكل كبير مع تقليل نطاقات وقت خمول المشاركين إلى الحد الأدنى، متفوقة بذلك على كل من صيغة MaxSAT المنشورة والمحلل التجاري Gurobi في كفاءة الحل.

المؤلفون الأصليون: Long Duc Nguyen, Tuyen Van Kieu, Khanh Van To

نُشر 2026-08-04

📖 5 دقيقة قراءة🧠 قراءة متعمّقة

CC BY 4.0

المؤلفون الأصليون: Long Duc Nguyen, Tuyen Van Kieu, Khanh Van To

البحث الأصلي مرخَّص بموجب CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ هذا شرح مولَّده بالذكاء الاصطناعي للبحث أدناه. لم يكتبه المؤلفون ولم يصادقوا عليه. وللتحقق من الدقة التقنية، يرجى الرجوع إلى البحث الأصلي. اقرأ إخلاء المسؤولية الكامل

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

لحل هذه المشكلة، يستخدم علماء الكمبيوتر نوعًا خاصًا من ألعاب المنطق تسمى SAT (الإرضاء). فكر في SAT كأنها محقق فائق الذكاء يتحقق مما إذا كانت مجموعة من القواعد يمكن أن تكون صحيحة في وقت واحد. إذا أخبرت المحقق: "الاجتماع (أ) يجب أن يكون قبل الاجتماع (ب)، ولكن الاجتماع (ب) يجب أن يكون قبل الاجتماع (أ)"، سيقول المحقق فورًا: "مستحيل!". ولكن إذا كانت القواعد معقدة ولكنها ممكنة، فسيجد المحقق جدولاً صالحاً. نسخة أخرى تسمى MaxSAT، وهي تشبه المحقق الذي لا يكتفي فقط بإيجاد جدول صالح، بل يحاول جعله "مثاليًا" عن طريق تقليل الوقت الذي يقضيه الناس في الانتظار. هذا البحث يتعمق في كيفية جعل هؤلاء المحققين المنطقيين أسرع وأذكى عند تنظيم هذه الفعاليات التجارية المعقدة.

المشكلة: شبكة متشابكة من الاجتماعات

في عالم اجتماعات الأعمال، تصبح الأمور فوضوية بسرعة. لديك قائمة اجتماعات، وقائمة فترات زمنية، وقائمة غرف. القواعد صارمة:

عدم التداخل: لا يمكن للشخص أن يتواجد في مكانين في آن واحد.
حدود الغرفة: لا يمكن للغرفة أن تستوعب أكثر من عدد الاجتماعات المسموح به.
الأسبقية: بعض الاجتماعات يجب أن تحدث قبل غيرها (مثل إيجاز صباحي قبل ورشة عمل بعد الظهر).
مشكلة "الوقت الضائع": الصداع الحقيقي هو "وقت الخمول". إذا كان لدى مشارك اجتماع في الساعة 9:00 صباحًا واجتماعه التالي ليس حتى الساعة 11:00 صباحًا، فلديه ساعتان من "وقت الخمول". الهدف من هذا البحث هو موازنة ذلك بحيث لا ينتظر أحد لساعات بينما ينتظر الآخرون بضع دقائق فقط. الأمر يتعلق بالعدالة والكفاءة.

الطريقة القديمة مقابل الطريقة الجديدة

لاحظ الباحثون طريقة موجودة بالفعل (تسمى ORG-MAXSAT) كانت جيدة تمامًا في الأصل. ومع ذلك، لاحظوا أنها تشبه محاولة تنظيم حفلة عن طريق كتابة كل تركيبة ممكنة للضيوف والأوقات، حتى تلك التي هي مستحيلة بوضاءة. كانت ضخمة، بطيئة، وتستهلك الكثير من ذاكرة الكمبيوتر.

قرر الفريق في جامعة VNU للهندسة والتكنولوجيا في فيتنام بناء نسخة "مدمجة". لقد قدموا ثلاث حيل لتقليص المشكلة:

فلتر "التحقق المسبق" (تصفية النطاق): قبل سؤال المحقق الكمبيوتري عن اللغز، أضافوا فلترًا ذكيًا. ينظر هذا الفلتر إلى القواعد ويستبعد فورًا الخيارات المستحيلة. على سبيل المثال، إذا كان اجتماع ما يجب أن يحدث بعد اجتماع آخر ينتهي في الساعة 2:00 ظهرًا، فإن الفلتر يحذف فورًا أي فترات زمنية قبل الساعة 2:00 من قائمة الاحتمالات. هذا يشبه تنظيف المكتب من الفوضى قبل محاولة العثور على قلم محدد. وقد أثبتوا أن هذا الفلتر لا يرمي أبدًا أي حل صالح؛ بل يزيل المهملات فقط.
"الدرج المشترك" (ترميز السعة المتناقصة المشتركة): عند التعامل مع قواعد "يحدث قبل"، كانت الطريقة القديمة تكتب ملاحظة منفصلة لكل زوج من الاجتماعات. إذا كان لديك 100 اجتماع، فهذا يعني آلاف الملاحظات. لاحظت الطريقة الجديدة أن العديد من هذه الملاحظات تقول الشيء نفسه. بدلًا من كتابة "الاجتماع (أ) قبل (ب)"، "الاجتماع (أ) قبل (ج)"، و"الاجتماع (أ) قبل (د)" بشكل منفصل، أنشأوا "درجًا" منطقيًا مشتركًا. إنهم يعيدون استخدام المتغيرات لمواقف متشابهة، مثل استخدام مفتاح رئيسي واحد لعدة أبواب بدلًا من صنع مفتاح جديد لكل قفل.
درجة "العدالة" (موازنة وقت الخمول): بدلاً من مجرد عد الفترات التي يقضيها الناس، ابتكروا طريقة جديدة لقياس "وقت الخمول". نظروا إلى الوقت بين أول اجتماع للشخص وآخر اجتماع له. إذا كان لدى شخص اجتماعات في الساعة 9:00 و11:00، فإن "مدته" هي ساعتان. إذا كان لديه اجتماع واحد فقط، فليس لديه وقت خمول. الهدف هو جعل الفرق بين أكثر شخص انشغالًا وأقل شخص انشغالًا في وقت الخمول أصغر ما يمكن.

ماذا وجدوا؟

اختبر الباحثون طريقتهم "المدمجة" الجديدة مقابل الطريقة القديمة وضد بعض البرامج التجارية القوية (مثل Gurobi وCPLEX) على 126 حالة اختبار رسمية و100 حالة "اختبار جهد" إضافية تحتوي على المزيد من الاجتماعات.

إليك النتائج، وهي مثيرة للإعجاب حقًا:

حجم أصغر: قللت الطريقة الجديدة عدد "البنود" المنطقية (القواعد التي يجب على الكمبيوتر فحصها) بنسبة 40.3% في المتوسط.
ذاكرة أقل: استخدمت ذاكرة أقل بنسبة 55.9% في ذروة الاستهلاك. تخيل أنك تحتاج إلى نصف ذاكرة الوصول العشوائي (RAM) لحل نفس اللغز.
سرعة أكبر: انخفض الوقت الإجمالي لحل المشكلات بنسبة 14.0%.
قوة التصفية: استخدام فلتر "التحقق المسبق" وحده قلل عدد المتغيرات بنسبة 24.1% والبنود بنسبة 16.2%.
قوة المشاركة: حيلة "الدرج المشترك" وفرت نسبة تتراوح بين 0.5% إلى 5.5% من البنود، اعتمادًا على مدى ازدحام الجدول الزمني.

الحكم النهائي

الجزء الأكثر إثارة هو أن طرق SAT وMaxSAT "المدمجة" الجديدة كانت قادرة على حل كل واحدة من الـ 126 حالة اختبار رسمية. والأفضل من ذلك، أنها فعلت ذلك بشكل أسرع من برنامج Guroi المتميز تجاريًا من حيث متوسط الوقت. بينما واجهت الأدوات التجارية الأخرى (مثل CPLEX وCP Optimizer) صعوبة في حل جميع الحالات ضمن المهلة الزمنية، تمكن النهج الجديد القائم على SAT من التعامل معها جميعًا.

لا يدعي البحث أنه حل مشاكل الجدولة في الكون للأبد، لكنه أظهر بالتأكيد أنه من خلال تنظيف القواعد ومشاركة العمل بذكاء أكبر، يمكننا جعل أجهزة الكمبيوتر أفضل بكثير في تنظيم حياتنا المزدحمة. إنه يحول عقدة الاجتماعات الضخمة والمتشابكة إلى جدول زمني مرتب ومتوازن حيث يحصل الجميع على حصتهم العادلة من الوقت، ولا يُترك أحد ينتظر في الممر لفترة طويلة.

ملخص تقني: ترميزات SAT و MaxSAT مدمجة لجدولة اجتماعات B2B مع موازنة وقت الفراغ

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

تتناول الورقة البحثية مسألة جدولة اجتماعات الأعمال إلى أعمال (B2B)، وهي مسألة تحسين توافقي حيث يجب تعيين الاجتماعات الثنائية المطلوبة لفتحات زمنية ومواقع محددة. يجب أن يستوفي الجدول عدة قيود:

عدم تداخل المشاركين: لا يمكن للمشارك حضور اجتماعين في وقت واحد.
سعة الموقع: لا يمكن أن يتجاوز عدد الاجتماعات في أي فتحة زمنية عدد المواقع المتاحة ( $K$ ).
التوافر والقيود: يجب أن تُعقد الاجتماعات ضمن الجلسات المطلوبة، أو الفتحات الثابتة، أو الفتحات المحظورة.
الأسبقية: تفرض الأقواس الموجهة $(i, j)$ أن يحدث الاجتماع $i$ قبل الاجتماع $j$ .

يختلف الهدف المقترح في هذا العمل عن الصيغ السابقة (التي غالبًا ما كانت تقلل "مجموعات الاستراحة" أو تحد من التفاوت في أعداد الاستراحات). بدلاً من ذلك، تهدف هذه الدراسة إلى تقليل نطاق إجمالي فترات الفراغ الداخلية ( $\Delta I$ ) بين المشاركين الذين لديهم اجتماعان على الأقل. تُعرَّف فترات الفراغ الداخلية بأنها الوقت غير المشغول الواقع تمامًا بين أول وآخر اجتماع تم تعيينه للمشارك. يميز هذا المقياس بين الانقطاعات القصيرة والانتظار الطويل، بهدف تحقيق توزيع متوازن للأعباء بشكل مشابه لمسألة المنهج الأكاديمي المتوازن (BACP). كما يتم الإبلاغ عن مقياس إجمالي وقت الفراغ ( $I_\Sigma$ ) كمقياس تكميلي.

المنهجية

يقترح المؤلفون ترميزًا مدمجًا لـ SAT (الإرضاء البولياني) و MaxSAT يدمج ثلاثة تحسينات رئيسية في النمذجة مقارنة بالصيغ المنشورة الحالية:

تصفية النطاق مع الحفاظ على الحل (المعالجة المسبقة):
قبل توليد الصيغة العادية المتقبة (CNF)، يطبق المؤلفون خوارزمية معالجة مسبقة (الخوارزمية 1) تزيل التعيينات غير المدعومة. ويتضمن ذلك:
- مرشحات حدود الأطراف: نشر قيود الأسبقية عبر المسارات (باستخدام الأقواس المباشرة أو الإغلاق المتعدي).
- المطابقة لكل مشارك: إزالة التعيينات التي لا يمكن أن تكون جزءًا من جدول خالٍ من التعارض لمشارك معين.
- نشر الفتحات المشبعة: استبعاد الفتحات حيث تكون السعة مستغلة بالكامل بالفعل بواسطة التعيينات القسرية.
- الادعاء: تحافظ هذه العملية على جميع الجداول الممكنة مع تقليل حجم النطاق، مما يقلل من عدد المتغيرات والبنود (clauses).
ترميز الأسبقية ذو اللاحقة المشتركة المتناثرة (SPARSESUFFIX):
بدلاً من ترميز علاقات الأسبقية باستخدام بنود زوجية (والتي يمكن أن تكون تربيعية بالنسبة لحجم النطاق)، يقدم المؤلفون ترميزًا متناثرًا.
- يقوم بتجسيد "نقاط القطع" المميزة فقط في نطاق السلف حيث يصبح القيد نشطًا.
- يعيد استخدام متغيرات مساعدة للقطع المتساوية عبر العلاقات المختلفة.
- ثبت أن هذا النهج مكافئ للبنود الزوجية ولكنه يقلل بشكل كبير من عدد البنود، خاصة عند دمجه مع تقليل النطاق.
هدف وقت الفراغ القائم على النطاق:
تقدم الورقة ترميزًا دقيقًا لتقليل نطاق فترات الفراغ الداخلية ( $\Delta I$ ).
- يشتق أول وآخر الفتحات المشغولة لكل مشارك.
- يستخدم عددًا خطيًا من المتغيرات المساعدة لحساب الفرق بين الحد الأقصى والحد الأدنى لأعداد الفراغ عبر جميع المشاركين المعنيين.

تقيم الدراسة هذه المكونات مقابل صيغة ORG-MAXSAT الأساسية (وهي تعديل لنموذج منشور) والمحللات التجارية (Gurobi، CPLEX، CP Optimizer). تغطي التقييمات 126 حالة اختبار رسمية و100 حالة "إجهاد" مشتقة مع كثافات أسبقية متفاوتة.

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

حدد البحث ثلاث مساهمات محددة:

إجراء المعالجة المسبقة: دمج مرشح يزيل التعيينات غير المدعومة قبل توليد CNF. تثبت المبرهنة 1 أن هذا يحافظ على الإمكانية، وتظهر النتائج التجريبية أنه يقلل متغيرات التعيين بنسبة 24.1% والبنود بنسبة 16.2%.
تمثيل اللاحقة المشتركة المتناثرة: ترميز دقيق (SPARSESUFFIX) يجسد فقط نقاط قطع نطاق السلف المطلوبة. تثبت المبرهنة 3 تكافؤه مع البنود الزوجية. توضح الدراسة أنه بينما يقلل تقليل النطاق من أعداد المتغيرات، فإن مشاركة اللاحقة يقلل بشكل مستقل من أعداد البنود.
هدف وقت الفراغ الخاص بـ B2B: هدف قائم على النطاق يقيس التفاوت في أوقات الانتظار الداخلية، وهو مُرمز بعدد خطي من المتغيرات المساعدة.

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

أُجريت التجارب على جهاز رباعي النواة مع حد زمني قدره 7,200 ثانية. تشمل النتائج الرئيسية ما يلي:

حجم الصيغة والذاكرة: مقارنةً بالأساس ORG-MAXSAT المعدل، قلل الترميز المدمج المقترح متوسط عدد البنود بنسبة 40.3% ومتوسط ذروة استخدام الذاكرة بنسبة 55.9%.
تأثير تقليل النطاق: قلل تصفية النطاق وحده متغيرات التعيين بنسبة 24.1% والبنود بنسبة 16.2%، مما ساهم بالحصة الأكبر من تقليل حجم الصيغة.
ترميز الأسبقية: قلل ترميز SPARSESUFFIX متوسط عدد البنود بنسبة 0.5%–1.0% في حالات الأسبقية الرسمية وما يصل إلى 5.5% في حالات الإجهاد المشتقة ذات الكثافة الأعلى (عند دمجه مع الإغلاق المتعدي).
أداء المحلل (Solver):
- حلت جميع طرق SAT/MaxSAT الثلاث المقترحة (Incremental SAT، Non-Incremental SAT، و UWrMaxSAT) جميع الحالات الرسمية الـ 126.
- مقارنة بـ Gurobi (المحلل التجاري الوحيد الذي حل جميع الحالات)، حققت طرق SAT/MaxSAT المقترحة أوقات إجمالية وسيطة أقل.
- حقق Incremental SAT أدنى وقت وسيط (0.227 ثانية) بين الطرق الكاملة.
- حقق CP Optimizer أدنى وقت وسيط (0.110 ثانية) ولكنه فشل في حل 11 حالة ضمن الحد الزمني.

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

تزعم الورقة أن الترميز المدمج المقترح يوفر تحسنًا كبيرًا في الكفاءة مقارنة بالصيغ البوليانية الموجودة لجدولة اجتماعات B2B. ومن خلال فصل تصفية النطاق عن تمثيل الأسبقية، يوضح المؤلفون أن تقليل النطاق هو المحرك الرئيسي لتقليل حجم الصيغة، بينما يوفر ترميز اللاحقة المشتركة المتناثرة تقليلًا إضافيًا في البنود بشكل مستقل عن مجموعة العلاقات.

وتؤكد الدراسة أن هدف نطاق وقت الفراغ الجديد يوفر مقياسًا أكثر دقة لجودة الجدول مقارنة بمقاييس "مجموعات الاستراحة" السابقة، حيث يميز بين الانقطاعات القصيرة والانتظار الطويل. علاوة على على ذلك، تشير النتائج إلى أن محللات SAT و MaxSAT الحديثة، عندما تُجهز بهذه الترميزات المدمجة، يمكنها التفوق على أفضل محللات MIP و CP التجارية من حيث وقت الحل الوسيط لهذا النوع المحدد من المسائل، حيث تحل جميع حالات الاختبار التي فشلت بعض المحلات التجارية في حلها بسبب انتهاء الوقت.

يظل المؤلفون متواضعين فيما يتعلق بالعمل المستقبلي، مشيرين إلى أن الدراسة الحالية تركز على توقيت التشغيل الواحد، وأن الأبحاث المستقبلية يمكن أن تستكشف تشغيلات التوقيت المتكررة والأهداف المعجمية (تقليل $\Delta I$ قبل $I_\Sigma$ ).