مسألة استيفاء منطقية

مسألة الاستيفاء منطقية، في المنطق وعلوم الحاسوب، (تسمى أحيانًا مسألة الاستيفاء الافتراضية وتختصر إلى الاستيفاء أو إس إيه تي أو بي-إس إيه تي) هي مسألة تحديد وجود ترجمة تفسيرية استيفاء صيغة منطقية معينة. بمعنى آخر، تستعلم ما إذا كان يمكن استبدال متغيرات صيغة منطقية معينة باستمرار بالقيم TRUE (صح) أو FALSE (خطأ) بطريقة تكون نتيجة الصيغة TRUE. إذا طبقت هذه الحالة، تسمى الصيغة مرضية. من ناحية أخرى، في حالة عدم وجود تعيين كهذا، تكون الوظيفة المعبر عنها بواسطة الصيغة FALSE لجميع تعيينات المتغيرات المحتملة وتكون الصيغة غير مرضية. مثلًا، تعد الصيغة «a AND NOT b (إيه و نفي بي) مرضية لأنه يمكن إيجاد قيمتين a = TRUE و b = FALSE، تحققان الصيغة (a AND NOT b = TRUE). في المقابل، تعد الصيغة «a AND NOT a» غير مُرضية.

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

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

 تعريفات ومصطلحات أساسية 
تبنى الصيغة المنطقية الافتراضية، وتسمى أيضًا تعبيرًا منطقيًا، من المتغيرات، وعمليات AND (وَ، العطف يُشار إليها أيضًا بـ∧)، و OR( أو، الفصل، ∨)، NOT (ليس، النفي، ¬)، والأقواس. يقال أن الصيغة مرضية إذا كان ممكنًا جعلها صحيحة عن طريق تعيين القيم المنطقية المناسبة (مثل TRUE، FALSE) لمتغيراتها. تعطى مسالة الاستيفاء المنطقية بمعادلة للتحقق ما إذا كانت مرضية. تعتبر مسألة القرار هذه ذات أهمية مركزية في العديد من مجالات علوم الحاسوب بما فيها علوم الحاسوب النظرية، ونظرية التعقيد، Here: p.86 Here: p.403 والخوارزميات، والتشفير والذكاء الاصطناعي.

توجد العديد من الحالات الخاصة لمسألة الاستيفاء المنطقية تتطلب أن يكون للصيغ بنية معينة. يعد الحرف إما متغير ويسمى حرف موجب، أو نفي متغير ويسمى حرف سالب. تعد العبارة فصل لعدة أحرف (أو حرف واحد). تسمى العبارة عبارة هورن إذا احتوت على أكثر من حرف موجب واحد. تكون الصيغة نموذج عطف طبيعي (سي إن إف) إذا عطفت عدة جمل (أو جملة واحدة)، فمثلًا إذا كان  x1حرف موجب، وx2¬ حرف سالب، تعد x1 ∨ ¬x2 عبارة. تعد الصيغة (x1 ∨ ¬x2) ∧ (¬x1 ∨ x2 ∨ x3) ∧ ¬x1) نموذج عطف طبيعي؛ تعد العبارتان الأولى والثالثة عبارتي هورن، لكن العبارة الثانية ليست كذلك. وبالتالي تكون الصيغة مرضية، باختيار x1 = FALSE ، وx2 = FALSE ، و x3كيفيًا، تنتهي العبارة (FALSE ∨ ¬FALSE) ∧ (¬FALSE ∨ FALSE ∨ x3) ∧ ¬FALSE إلى (FALSE ∨ TRUE) ∧ (TRUE ∨ FALSE ∨ x3) ∧ TRUE، وبالتالي إلى TRUE ∧ TRUE ∧ TRUE (أي إلى TRUE). على النقيض من ذلك، فإن صيغة نموذج عطف طبيعي a ∧ ¬a، التي تتكون من جملتين من حرف واحد، غير مرضية، نظرًا لأنه إذا كان لـ a = TRUE أو a = FALSE ستنتهي إلى  TRUE ∧ ¬TRUE (أي FALSE) أو FALSE ∧ ¬FALSE (أي، FALSE  مرة أخرى)، على التوالي.

من المفيد بالنسبة لبعض نسخ مسائل الاستيفاء تحديد مفهوم صيغة نموذج العطف الطبيعي المعمم، بمعنى كعطف للعديد من العبارات المعممة كيفيًا، يكون الأخير من النموذج  R(l1,...,ln) لبعض المعاملات المنطقية R والحروف (العادية) li. تؤدي المجموعات المختلفة من المعاملات المنطقية المسموح بها إلى نسخ مختلفة من المسائل. كمثال، تعد (R (¬x,a, b عبارة معممة، وR(¬x,a,b) ∧ R(b,y,c) ∧ R(c,d,¬z) عبارة نموذج عطف طبيعي معممة. تستخدم هذه الصيغة أدناه، بحيث يكون R هو المعامل الثلاثي الذي يكون TRUE فقط عندما تكون إحدى وسيطاته TRUE.

يمكن تحويل كل صيغة منطقية افتراضية إلى نموذج عطف طبيعي مكافئ، باستخدام قوانين الجبر المنطقي، والذي قد يكون، رغم ذلك، أطول بكثير، يعطي مثلًا تحويل الصيغة(x1∧y1) ∨ (x2∧y2) ∨ ... ∨ (xn∧yn) إلى نموذج عطف طبيعي ما يلي








 ;

نلاحظ أن الأول هو فصل لعدد n من عطف بين متغيرين، بينما يتكون الأخير من 2n عبارة من n متغير.

 التعقيد والنسخ المقيدة 

 الاستيفاء غير المقيد 

كانت مسألة الاستيفاء غير المقيد أول مسألة كثيرة حدود غير قطعية كاملة معروفة، كما أثبتها ستيفن كوك في جامعة تورنتو في عام 1971 وليونيد ليفين بشكل مستقل في الأكاديمية الوطنية للعلوم في عام 1973. (pdf) , translated into English by  حتى ذلك الوقت، لم يكن مفهوم المسألة كثيرة حدود غير القطعية الكاملة موجودًا حتى. يوضح الدليل كيف يمكن اختزال كل مسألة قرار من فئة تعقيد كثير الحدود غير القطعي إلى مسألة الاستيفاء غير المقيد منطقية لصيغ نموذج عطف طبيعي، والتي تسمى أحيانًا CNFSAT. تعد إحدى الخصائص المفيدة لاختزال كوك أنه يحافظ على عدد الإجابات المقبولة. مثلًا، يعد تحديد ما إذا كان رسم بياني معين يحتوي على 3 ألوان مسألة أخرى كثيرة حدود غير قطعية، إذا احتوى كان الرسم البياني على 17 تلوينًا صالحًا، فإن صيغة مسألة الاستيفاء غير المقيد الناتجة عن اختزال كوك-ليفين ستشمل 17 تعيين مرضي.

يشير اكتمال مسألة كثيرة الحدود غير القطعية إلى وقت تشغيل أسوأ الحالات فقط. يمكن حل العديد من الحالات التي تحدث في التطبيقات العملية بسرعة أكبر. انظر خوارزميات حل مسائل الاستيفاء غير المقيد أدناه.

تعد مسألة الاستيفاء غير المقيد أمرًا بسيطًا إذا اقتصرت الصيغ على صيغ نموذج الفصل الطبيعي، أي إذا كانت فصل لعبارات عطف الأحرف. تكون هذه الصيغة مرضية فعلًا إذا وفقط إذا كانت إحدى عبارات العطف على الأقل مرضية، وتكون عبارة العطف مرضية إذا وفقط إذا لم تحتوي على كل من x ونفي x معًا. يمكن التحقق من ذلك في زمن خطي. بالإضافة إلى ذلك، إن اقتصرت على نموذج فصل طبيعي تمامًا، بحيث يظهر كل متغير مرة واحدة بالضبط في كل عطف، يمكن التحقق منها في وقت ثابت (يمثل كل عطف تعيين مرضي واحد). ولكن يمكن أن يستغرق الأمر وقتًا ومساحة أسيتين لتحويل مسألة استيفاء عامة إلى نموذج فصل طبيعي؛ لتبديل «∧» إلى «∨» في مثال النشر الأسي أعلاه لنماذج العطف الطبيعية.

 مراجع 

تصنيف:أتمتة التصميم الإلكتروني
تصنيف:جبر منطقي
تصنيف:طرق شكلية
تصنيف:مسائل كثيرة حدود غير قطعية كاملة
تصنيف:مسائل استيفاء
تصنيف:منطق في علم الحاسوب