مسألة قابلية الإرضاء المنطقية

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

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

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

تعريفات ومصطلحات أساسية عدل

تبنى الصيغة المنطقية الافتراضية، وتسمى أيضًا تعبيرًا منطقيًا، من المتغيرات، وعمليات AND (وَ، العطف يُشار إليها أيضًا بـ∧)، و OR( أو، الفصل، ∨)، NOT (ليس، النفي، ¬)، والأقواس. يقال أن الصيغة مرضية إذا كان ممكنًا جعلها صحيحة عن طريق تعيين القيم المنطقية المناسبة (مثل TRUE، FALSE) لمتغيراتها. تعطى مسالة الإرضاء المنطقية بمعادلة للتحقق ما إذا كانت مرضية. تعتبر مسألة القرار هذه ذات أهمية مركزية في العديد من مجالات علوم الحاسوب بما فيها علوم الحاسوب النظرية، ونظرية التعقيد،^[3]^[4] والخوارزميات، والتشفير^[5]^[6] والذكاء الاصطناعي.^[7]

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

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

يمكن تحويل كل صيغة منطقية افتراضية إلى نموذج عطف طبيعي مكافئ، باستخدام قوانين الجبر المنطقي، والذي قد يكون، رغم ذلك، أطول بكثير، يعطي مثلًا تحويل الصيغة(x₁∧y₁) ∨ (x₂∧y₂) ∨ ... ∨ (x_n∧y_n) إلى نموذج عطف طبيعي ما يلي

(x 1 \lor x 2 \lor \dots \lor x n) \land

(y 1 \lor x 2 \lor \dots \lor x n) \land

(x 1 \lor y 2 \lor \dots \lor x n) \land

(y 1 \lor y 2 \lor \dots \lor x n) \land ... \land

(x 1 \lor x 2 \lor \dots \lor y n) \land

(y 1 \lor x 2 \lor \dots \lor y n) \land

(x 1 \lor y 2 \lor \dots \lor y n) \land

(y 1 \lor y 2 \lor \dots \lor y n)

;

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

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

قابلية الإرضاء غير المقيدة عدل

كانت مسألة قابلية الإرضاء أول مسألة كثيرة حدود غير قطعية كاملة معروفة، كما أثبتها ستيفن كوك في جامعة تورنتو في عام 1971^[8] وليونيد ليفين بشكل مستقل في الأكاديمية الوطنية للعلوم في عام 1973.^[9] حتى ذلك الوقت، لم يكن مفهوم المسألة كثيرة حدود غير القطعية الكاملة موجودًا حتى. يوضح الدليل كيف يمكن اختزال كل مسألة قرار من فئة تعقيد كثير الحدود غير القطعي إلى مسألة قابلية إرضاء منطقية لصيغ نموذج عطف طبيعي، والتي تسمى أحيانًا CNFSAT. تعد إحدى الخصائص المفيدة لاختزال كوك أنه يحافظ على عدد الإجابات المقبولة. مثلًا، يعد تحديد ما إذا كان رسم بياني معين يحتوي على 3 ألوان مسألة أخرى كثيرة حدود غير قطعية، إذا احتوى كان الرسم البياني على 17 تلوينًا صالحًا، فإن صيغة مسألة قابلية الإرضاء الناتجة عن اختزال كوك-ليفين ستشمل 17 تعيين مرضي.

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

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

مراجع عدل

^ Ohrimenko، Olga؛ Stuckey، Peter J.؛ Codish، Michael (2007)، "Propagation = Lazy Clause Generation"، Principles and Practice of Constraint Programming – CP 2007، Lecture Notes in Computer Science، ج. 4741، ص. 544–558، CiteSeerX:10.1.1.70.5471، DOI:10.1007/978-3-540-74970-7_39، modern SAT solvers can often handle problems with millions of constraints and hundreds of thousands of variables.
^ Hong، Ted؛ Li، Yanjing؛ Park، Sung-Boem؛ Mui، Diana؛ Lin، David؛ Kaleq، Ziyad Abdel؛ Hakim، Nagib؛ Naeimi، Helia؛ Gardner، Donald S.؛ Mitra، Subhasish (نوفمبر 2010). "QED: Quick Error Detection tests for effective post-silicon validation". 2010 IEEE International Test Conference: 1–10. DOI:10.1109/TEST.2010.5699215. ISBN:978-1-4244-7206-2. S2CID:7909084.
^ Karp، Richard M. (1972). "Reducibility Among Combinatorial Problems" (PDF). في Raymond E. Miller؛ James W. Thatcher (المحررون). Complexity of Computer Computations. New York: Plenum. ص. 85–103. ISBN:0-306-30707-3. مؤرشف من الأصل (PDF) في 2011-06-29. اطلع عليه بتاريخ 2020-05-07. Here: p.86
^ Alfred V. Aho and John E. Hopcroft and Jeffrey D. Ullman (1974). The Design and Analysis of Computer Algorithms. Reading/MA: Addison-Wesley. ISBN:0-201-00029-6. Here: p.403
^ Massacci, Fabio; Marraro, Laura (1 Feb 2000). "Logical Cryptanalysis as a SAT Problem". Journal of Automated Reasoning (بالإنجليزية). 24 (1): 165–203. DOI:10.1023/A:1006326723002. ISSN:1573-0670. Archived from the original on 2020-03-01.
^ Mironov, Ilya; Zhang, Lintao (2006). Biere, Armin; Gomes, Carla P. (eds.). "Applications of SAT Solvers to Cryptanalysis of Hash Functions". Theory and Applications of Satisfiability Testing - SAT 2006. Lecture Notes in Computer Science (بالإنجليزية). Berlin, Heidelberg: Springer. 4121: 102–115. DOI:10.1007/11814948_13. ISBN:978-3-540-37207-3. Archived from the original on 2021-03-21.
^ Vizel، Y.؛ Weissenbacher، G.؛ Malik، S. (2015). "Boolean Satisfiability Solvers and Their Applications in Model Checking". Proceedings of the IEEE. ج. 103 ع. 11: 2021–2035. DOI:10.1109/JPROC.2015.2455034. S2CID:10190144.
^ Cook، Stephen A. (1971). "The Complexity of Theorem-Proving Procedures" (PDF). Proceedings of the 3rd Annual ACM Symposium on Theory of Computing: 151–158. CiteSeerX:10.1.1.406.395. DOI:10.1145/800157.805047. S2CID:7573663. مؤرشف من الأصل (PDF) في 2021-05-07.
^ Levin، Leonid (1973). "Universal search problems (Russian: Универсальные задачи перебора, Universal'nye perebornye zadachi)". Problems of Information Transmission (Russian: Проблемы передачи информа́ции, Problemy Peredachi Informatsii). ج. 9 ع. 3: 115–116. (pdf) باللغة الروسية, translated into English by Trakhtenbrot، B. A. (1984). "A survey of Russian approaches to perebor (brute-force searches) algorithms". Annals of the History of Computing. ج. 6 ع. 4: 384–400. DOI:10.1109/MAHC.1984.10036. S2CID:950581.

مسألة قابلية الإرضاء المنطقية في المشاريع الشقيقة:

صور وملفات صوتية من كومنز.

بوابة منطق

[Codish.Ohrimenko.Stuckey.2007-1] Ohrimenko، Olga؛ Stuckey، Peter J.؛ Codish، Michael (2007)، "Propagation = Lazy Clause Generation"، Principles and Practice of Constraint Programming – CP 2007، Lecture Notes in Computer Science، ج. 4741، ص. 544–558، CiteSeerX:10.1.1.70.5471، DOI:10.1007/978-3-540-74970-7_39، modern SAT solvers can often handle problems with millions of constraints and hundreds of thousands of variables.

[2] Hong، Ted؛ Li، Yanjing؛ Park، Sung-Boem؛ Mui، Diana؛ Lin، David؛ Kaleq، Ziyad Abdel؛ Hakim، Nagib؛ Naeimi، Helia؛ Gardner، Donald S.؛ Mitra، Subhasish (نوفمبر 2010). "QED: Quick Error Detection tests for effective post-silicon validation". 2010 IEEE International Test Conference: 1–10. DOI:10.1109/TEST.2010.5699215. ISBN:978-1-4244-7206-2. S2CID:7909084.

[3] Karp، Richard M. (1972). "Reducibility Among Combinatorial Problems" (PDF). في Raymond E. Miller؛ James W. Thatcher (المحررون). Complexity of Computer Computations. New York: Plenum. ص. 85–103. ISBN:0-306-30707-3. مؤرشف من الأصل (PDF) في 2011-06-29. اطلع عليه بتاريخ 2020-05-07. Here: p.86

[4] Alfred V. Aho and John E. Hopcroft and Jeffrey D. Ullman (1974). The Design and Analysis of Computer Algorithms. Reading/MA: Addison-Wesley. ISBN:0-201-00029-6. Here: p.403

[5] Massacci, Fabio; Marraro, Laura (1 Feb 2000). "Logical Cryptanalysis as a SAT Problem". Journal of Automated Reasoning (بالإنجليزية). 24 (1): 165–203. DOI:10.1023/A:1006326723002. ISSN:1573-0670. Archived from the original on 2020-03-01.

[6] Mironov, Ilya; Zhang, Lintao (2006). Biere, Armin; Gomes, Carla P. (eds.). "Applications of SAT Solvers to Cryptanalysis of Hash Functions". Theory and Applications of Satisfiability Testing - SAT 2006. Lecture Notes in Computer Science (بالإنجليزية). Berlin, Heidelberg: Springer. 4121: 102–115. DOI:10.1007/11814948_13. ISBN:978-3-540-37207-3. Archived from the original on 2021-03-21.

[7] Vizel، Y.؛ Weissenbacher، G.؛ Malik، S. (2015). "Boolean Satisfiability Solvers and Their Applications in Model Checking". Proceedings of the IEEE. ج. 103 ع. 11: 2021–2035. DOI:10.1109/JPROC.2015.2455034. S2CID:10190144.

[8] Cook، Stephen A. (1971). "The Complexity of Theorem-Proving Procedures" (PDF). Proceedings of the 3rd Annual ACM Symposium on Theory of Computing: 151–158. CiteSeerX:10.1.1.406.395. DOI:10.1145/800157.805047. S2CID:7573663. مؤرشف من الأصل (PDF) في 2021-05-07.

[9] Levin، Leonid (1973). "Universal search problems (Russian: Универсальные задачи перебора, Universal'nye perebornye zadachi)". Problems of Information Transmission (Russian: Проблемы передачи информа́ции, Problemy Peredachi Informatsii). ج. 9 ع. 3: 115–116. (pdf) باللغة الروسية, translated into English by Trakhtenbrot، B. A. (1984). "A survey of Russian approaches to perebor (brute-force searches) algorithms". Annals of the History of Computing. ج. 6 ع. 4: 384–400. DOI:10.1109/MAHC.1984.10036. S2CID:950581.

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]