💻 computer science

Solving Fuzzy Satisfiability via Mixed-Integer Non-Linear Programming

تقدم هذه الورقة SATFuL، وهو برنامج جديد لحل مشكلات التبعية (SAT solver) للمنطق الضبابي، يستفيد من البرمجة غير الخطية ذات الأعداد الصحيحة المختلطة (MINLP) لتحقيق السلامة والكمال والقدرة الواسعة على التطبيق عبر مختلف أنظمة المنطق الضبابي، مما يظهر أداءً يضاهي أو يتفوق على الأدوات الحالية الرائدة.

المؤلفون الأصليون: Pablo F. Castro

نُشر 2026-04-20

📖 4 دقيقة قراءة☕ قراءة في استراحة قهوة

CC BY 4.0

المؤلفون الأصليون: Pablo F. Castro

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

تخيل أنك تحاول حل لغز ضخم ومعقد. في عالم الحواسيب التقليدية، يتكون هذا اللغز من مفاتيح إضاءة: إما مفتوح (1) أو مغلق (0). يُسمى هذا "المنطق البولياني" (Boolean Logic)، ولدينا روبوتات فائقة السرعة والذكاء (تُسمى SAT solvers) يمكنها حل هذه الألغاز في لمح البصر.

ولكن ماذا لو لم يكن لغزك مكوناً من مجرد مفاتيح بسيطة؟ ماذا لو كان بإمكان هذه المفاتيح أن تخفت؟ هل يمكن أن تكون بنسبة 10%، أو 50%، أو 99.9%؟ هذا هو عالم المنطق الضبابي (Fuzzy Logic). وهو يُستخدم في أشياء مثل السيارات ذاتية القيادة (هل الطريق "زلق قليلاً" أم "زلق جداً"؟)، والذكاء الاصطناعي، ومعالجة الصور.

المشكلة هي أننا لا نملك روبوتات جيدة لحل ألغاز "المفاتيح الخافتة" هذه بعد. فالأدوات الموجودة حالياً إما بطيئة جداً، أو تعمل فقط لأنواع محددة من الألغاز، أو تخطئ أحياناً في الإجابة.

إليكم SATFuL: "رئيس الطهاة" لألغاز المنطق الضبابي

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

إليك التشبيه:

اللغز: لديك وصفة تحتوي على تعليمات غامضة مثل "أضف القليل من الملح" أو "اطبخ حتى ينضج الطعام غالباً".
الطريقة القديمة: حاولت الأدوات السابقة تخمين الإجابة عن طريق تذوق الطعام مراراً وتكراراً. أحياناً يصيبون، وأحياناً يستسلمون، وأحياناً يقدمون لك طعاماً محترقاً معتقدين أنه مثالي.
طريقة SATFuL: يقوم SATFuL بترجمة وصفتك الغامضة إلى معادلة رياضية دقيقة. يقول: "حسناً، 'القليل من الملح' يعني بالضبط 0.3 جرام، و'نضج الطعام غالباً' يعني أن درجة الحرارة يجب أن تكون بين 180 و190 درجة".
النتيجة: يسلم هذه المعادلة الدقيقة إلى آلة حاسبة ضخمة وصناعية (محرك MINLP مثل Gurobi أو SCIP) مشهورة بحل المسائل الرياضية المعقدة فوراً.

لماذا يعد هذا أمراً هاماً؟

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

ضد "المتخصص الإيطالي" (fuzzySAT)، كان SATFuL بنفس السرعة، ولكنه كان أفضل بك mucho في إثبات متى يكون اللغز مستحيلاً للحل.
ضد "المتخصص الفرنسي" (MNiBLoS)، حقق SATFuL انتصاراً ساحقاً، حيث حل المسائل بشكل أسرع بكثير ودون ارتكاب أخطاء.

كيف يعمل من الداخل؟

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

"ساطع إلى حد ما" تصبح متغيراً $x$ بين 0 و1.
"مظلم غالباً" تصبح علاقة بين $x$ ومتغير آخر.
يربط كل هذه القواعد معاً في مسألة رياضية واحدة ضخمة ومعقدة.
ثم يسأل محرك رياضيات قوياً: "هل هناك أي طريقة لضبط هذه المتغيرات بحيث تكون جميع القواعد صحيحة؟"

إذا وجد المحرك الرياضي حلاً، يقول SATFuL: "SAT" (قابل للتحقق/نعم). وإذا قال المحرك إن القواعد متناقضة، يقول SATFuL: "UNSAT" (غير قابل للتحقق/لا).

الخلاصة

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

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

إليك ملخص تقني مفصل لورقة البحث "حل قابلية الإرضاء الضبابي عبر البرمجة غير الخطية ذات الأعداد الصحيحة المختلطة" للباحث بابلو ف. كاسترو.

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

تتناول الورقة مشكلة قابلية الإرضاء (Satisfiability - SAT) للمنطق الضبابي. على عكس مسألة SAT البولينية، حيث تُقيم الصيغ بـ "صحيح" (1) أو "خطأ" (0)، فإن صيغ المنطق الضبابي تُقيم بقيم ضمن الفترة المستمرة $[0, 1]$ .

السياق: بينما تُعد أدوات حل مسألة Boolean SAT ناضجة ومستخدمة على نطاق واسع (مثل أدوات SMT والتحقق من النماذج)، فإن أدوات حل المسائل الضبابية (Fuzzy SAT) لا تزال غير متطورة بما يكفي.
التحديات:
- تنوع المنطقيات: تختلف المنطقيات الضبابية بناءً على تعريف الـ t-norm (الاقتران). تركز الورقة على منطقيات Łukasiewicz و Product و Gödel. غالبًا ما تكون الأدوات الموجودة مخصصة لمنطقيات معينة (مثل Łukasiewicz فقط) وتواجه صعوبة في التعميم.
- القابلية للتوسع والاكتمال: تعاني أدوات الحل الضبابية الحالية من مشكلات في القابلية للتوسع. يعتمد بعضها على الاختزال إلى منطقيات ذات قيم محدودة (مما يؤدي لفقدان الدقة) أو استراتيجيات تطورية (غير مكتملة).
- قيود محددة: غالبًا ما تستخدم أدوات منطق Product الحالية (مثل MNiBLoS) تحويلات غير مكتملة للحسابات غير الخطية، مما قد يؤدي لتصنيف خاطئ للبنود غير القابلة للإرضاء على أنها قابلة للإرضاء.

2. المنهجية: SATFuL

يقترح المؤلفون SATFuL، وهو أداة جديدة لحل مسائل SAT عبر ترجمة مسائل القابلية للإرضاء الضبابية إلى مسائل برمجة غير خطية ذات أعداد صحيحة مختلطة (MINLP).

النهج الجوهري

بدلاً من استخدام استدلالات (heuristics) متخصصة للمنطق الضبابي، يستفيد SATFuL من قوة أدوات حل MINLP الحديثة (تحديداً Gurobi و SCPI) للتعامل مع القيود الحسابية المتأصلة في المنطق الضبابي.

الخوارزمية

يعمل الحل على مرحلتين رئيسيتين:

الإجراء (toMINLP):
- تقوم الخوارزمية بالمرور بشكل متكرر (recursively) على الصيغة الضبابية.
- لكل صيغة فرعية $\phi'$ ، يتم إدخال متغير جديد ذو قيمة حقيقية $x_{\phi'} \in [0, 1]$ .
- تولد الخوارزمية مجموعة من القيود الخطية وغير الخطية ( $I$ ) والمتغيرات الصحيحة ( $Z$ ) التي تفرض دلالات العمليات الضبابية رياضياً.
- التعامل مع العمليات الأساسية:
  - منطق Łukasiewicz: يستخدم قيوداً خطية لعمليات الاقتران/التشتت (conjunction/disjunction) ويُدخل متغيرات ثنائية للتعامل مع عامل الاستلزام ( $x \Rightarrow_L y$ ).
  - منطق Product: يتعامل مع الضرب غير الخطي ( $x \cdot y$ ) بشكل مباشر. ومن الأهمية بمكان أنه ينمذج الاستلزام ( $x \Rightarrow_\Pi y$ ) والنفي باستخدام متغيرات ثنائية مساعدة وقيود غير خطية لضمان الدقة، متجنباً التقريبات المستخدمة في الأدوات السابقة.
  - منطق Gödel: لم يتم ترميزه كعمليات منفصلة لأنه يمكن التعبير عنه باستخدام عمليات Łukasiewicz ضمن هذا الإطار.
الإجراء (SAT):
- يتم تحويل مجموعة البنود إلى مسألة MINLP واحدة $\langle I, Z, M \rangle$ ، حيث تمثل $I$ القيود، و $Z$ المتغيرات الصحيحة، و $M$ دالة الهدف (تقليل مجموع المتغيرات، رغم أن الهدف الأساسي هو التحقق من الإمكانية/Feasibility).
- تقوم الأداة باستدعاء برنامج حل MINLP خارجي.
- إذا وجد البرنامج حلاً ممكناً، تكون الصيغة قابلة للإرضاء (SAT)؛ وإلا فهي غير قابلة للإرضية (UNSAT).

الضمانات النظرية

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

بنية الأداة

SATFuL هي أداة مفتوحة المصدر بلغة Python تتكون من ثلاث وحدات:

المعالجة المسبقة (Preprocessing): تقوم بتحليل المدخلات وبناء شجرة بناء الجملة المجردة (AST).
وحدة MINLP: تنفذ خوارزمية الترجمة المتكررة باستخدام نمط الزائر (visitor pattern).
وحدة الحل (Solver Module): تتصل ببرنامج Gurobi أو SCIP لحل مسألة MINLP الناتجة.

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

التعميم: على عكس الأدوات السابقة المقيدة بمنطقيات محددة، يتعامل SATFuL مع منطقيات Łukasiewicz و Product و Gödel ضمن إطار عمل واحد.
الدقة لمنطق Product: يوفر اختزالاً سليماً ومكتملاً لمنطق Product، مما يعالج مشكلات عدم الاكتمال في الحلول السابقة مثل MNiBLoS (التي تقوم بخرائط الحسابات غير الخطية إلى حسابات سالبة، مما قد يتسبب في أخطاء).
الاستفادة من تطورات MINLP: يستفيد من التطورات الأخيرة في برامج حل MINLP التجارية (Gurobi) والأكاديمية (SCIP)، والتي أصبحت أقوى بكثير وقابلة للتوسع مقارنة بالنهج المعتمد على MILP الذي جُرِّب سابقاً.
القابلية للتوسع: التصميم الوحدوي (modular) يسمح بإضافة عمليات ضبابية أو منطقيات جديدة بسهولة عبر مجرد تعريف القيود الرياضية المقابلة لها.

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

قام المؤلفون بتقييم SATFuL مقابل المنافسين الرائدين:

المنافسون:
- fuzzySAT: حل متطور لمنطق Łukasiewicz (يختزل إلى CSP).
- MNiBLoS: حل لمنطق Product يستخدم برنامج SMT وهو Z3.
الإعداد: أُجريت التجارب على جهاز MacBook M2 (ذاكرة 16 جيجابايت) باستخدام اختبارات مرجعية من [16].
النتائج:
- منطق Łukasiewicz:
  - باستخدام Gurobi، تفوق SATFuL باستمرار على fuzzySAT في كل من حالات SAT و UNSAT.
  - باستخدام SCIP، كان SATFuL مقارباً لـ fuzzySAT في حالات SAT، ولكنه كان متفوقاً بشكل كبير في حالات UNSAT (حيث كان fuzzySAT يستغرق وقتاً طويلاً جداً، بينما حل SATFuL جميع الحالات).
- منطق Product:
  - تفوق SATFuL (باستخدام Gurobi و SCIP) على MNiBLoS في جميع الحالات (سواء SAT أو UNSAT).
  - يؤكد هذا أن نهج MINLP أكثر متانة وقابلية للتوسع من الاختزال المعتمد على SMT المستخدم في MNiBLoS.

5. الأهمية

سد الفجوة: يقلص SATFuL الفجوة في الأداء بين حلول الـ Fuzzy SAT وحلول Boolean SAT عالية الكفاءة.
الموثوقية: من خلال توفير اختزال سليم ومكتمل لمنطق Product، فإنه يلغي خطر التصنيفات الخاطئة لقابلية الإرضاء التي كانت موجودة في النهج السابقة.
الفائدة العملية: توفر الأداة منصة موحدة، سهلة الصيانة والتوسيع للتحقق من الأنظمة التي تتضمن الاستدلال الضبابي (مثل الشبكات العصبية، معالجة الصور، الأنظمة متعددة الوكلاء) دون الحاجة لإعادة كتابة الحلول لكل نوع من أنواع المنطق.
الإمكانات المستقبلية: يشير نجاح هذا النهج إلى أن البرمجة غير الخطية ذات الأعداد الصحيحة المختلطة (MINLP) هي خلفية (backend) حيوية وقوية لحل مسائل المنطق متعدد القيم المعقدة، مما يفتح الباب لمزيد من التوسعات (مثل المتغيرات العشوائية أو العلاقات).