قابلية الإرضاء الثنائية

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

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

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

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

تمثيلات المسألة[عدل]

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

${\begin{aligned}&(x_{0}\lor x_{2})\land (x_{0}\lor \lnot x_{3})\land (x_{1}\lor \lnot x_{3})\land (x_{1}\lor \lnot x_{4})\land {}\\&(x_{2}\lor \lnot x_{4})\land {}(x_{0}\lor \lnot x_{5})\land (x_{1}\lor \lnot x_{5})\land (x_{2}\lor \lnot x_{5})\land {}\\&(x_{3}\lor x_{6})\land (x_{4}\lor x_{6})\land (x_{5}\lor x_{6}).\end{aligned}}$

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

تُعرف الصيغ في هذا النموذج بـ2-سي إن إف. يرمز الرقم «2» في هذا الاسم إلى عدد المحارف لكل عبارة، ويرمز «سي إن إف» إلى صيغة العطف الطبيعي، وهو نوع من التعبير المنطقي في صيغة عطف الفصل.^[1] وتسمى أيضًا صيغ كورم، تكريمًا لأعمال عالم الرياضيات في جامعة كاليفورنيا في ديفيس ميلفن ر. كروم، الذي كانت ورقته البحثية عام 1967 إحدى أقدم الأعمال المتعلقة بمسألة قابلية الإرضاء الثنائية.^[2]

تعد كل عبارة في صيغة العطف الطبيعي الثنائية مكافئ منطقي لاقتضاء من متغير واحد أو نفي متغير إلى الآخر. يمكن مثلًا كتابة الفقرة الثانية في المثال بأي من الطرق الثلاثة المكافئة:

$(x_{0}\lor \lnot x_{3})\;\equiv \;(\lnot x_{0}\Rightarrow \lnot x_{3})\;\equiv \;(x_{3}\Rightarrow x_{0}).$

يمكن أيضًا كتابة مثيل قابلية الإرضاء الثنائية في صيغة اقتضاء طبيعي، بسبب هذا التكافؤ بين أنواع العمليات المختلفة هذه، بحيث نستبدل كل عبارة أو في صيغة العطف الطبيعي بالمقتضين المساويين.^[3]

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

مخطط اقتضاء لمثيل قابلية الإرضاء الثنائية الموضح في هذا القسم.^[4]

الخوارزميات[عدل]

تُعرف عدة خوارزميات لحل مسألة قابلية الإرضاء الثنائية. تستغرق أكثر الخوارزميات كفاءة وقتًا خطيًا.^[2]^[4]^[5]

القرار والإغلاق المتعدِ[عدل]

وصف كروم (1967) إجراء اتخاذ القرار الزمني متعدد الحدود التالي لحل مثيلات قابلية الإرضاء الثنائية.^[2]

لنفترض أن مثيل قابلية إرضاء ثنائية يحتوي على عبارتين يستخدم كلاهما المتغير x نفسه، لكن ينفى x في إحدى العبارتين. بالتالي يمكن الجمع بين الجملتين لإنتاج جملة ثالثة، تحتوي المحرفيين الآخرين من العبارتين؛ ترضى العبارة الثالثة حكمًا عند إرضاء أول عبارتين. مثلًا، إذا دمجنا العبارتين (a ∨ b) و(b ∨¬c¬) تنتج بهذه الطريقة عبارة (a ∨ ¬c). بالنسبة لصيغة الاقتضاء لنموذج العطف الطبيعي الثنائي، تعادل هذه القاعدة إيجاد اقتضائين a ⇒ b¬ وb ⇒ ¬c واستدلال اقتضاء ثالث بالتعدِ a ⇒ ¬ c¬.^[2]

المراجع[عدل]

^ Prestwich، Steven (2009)، "2. CNF Encodings"، في Biere، Armin؛ Heule، Marijn؛ van Maaren، Hans؛ Walsh، Toby (المحررون)، Handbook of Satisfiability، Frontiers in Artificial Intelligence and Applications، IOS Press، ج. 185، ص. 75–98، DOI:10.3233/978-1-58603-929-5-75، ISBN:978-1-58603-929-5.
^ ^ا ^ب ^ج ^د Krom، Melven R. (1967)، "The Decision Problem for a Class of First-Order Formulas in Which all Disjunctions are Binary"، Zeitschrift für Mathematische Logik und Grundlagen der Mathematik، ج. 13، ص. 15–20، DOI:10.1002/malq.19670130104.
^ Russell، Stuart Jonathan؛ Norvig، Peter (2010)، Artificial Intelligence: A Modern Approach، Prentice Hall series in artificial intelligence، Prentice Hall، ص. 282، ISBN:978-0-13-604259-4.
^ ^ا ^ب Aspvall، Bengt؛ Plass، Michael F.؛ Tarjan، Robert E. (1979)، "A linear-time algorithm for testing the truth of certain quantified boolean formulas" (PDF)، Information Processing Letters، ج. 8، ص. 121–123، DOI:10.1016/0020-0190(79)90002-4، مؤرشف من الأصل (PDF) في 2021-05-06.
^ Even، S.؛ Itai، A.؛ Shamir، A. (1976)، "On the complexity of time table and multi-commodity flow problems"، SIAM Journal on Computing، ج. 5، ص. 691–703، DOI:10.1137/0205048.

بوابة علم الحاسوب

[cnf-1] Prestwich، Steven (2009)، "2. CNF Encodings"، في Biere، Armin؛ Heule، Marijn؛ van Maaren، Hans؛ Walsh، Toby (المحررون)، Handbook of Satisfiability، Frontiers in Artificial Intelligence and Applications، IOS Press، ج. 185، ص. 75–98، DOI:10.3233/978-1-58603-929-5-75، ISBN:978-1-58603-929-5.

[Krom1967-2] ا ^ب ^ج ^د Krom، Melven R. (1967)، "The Decision Problem for a Class of First-Order Formulas in Which all Disjunctions are Binary"، Zeitschrift für Mathematische Logik und Grundlagen der Mathematik، ج. 13، ص. 15–20، DOI:10.1002/malq.19670130104.

[3] Russell، Stuart Jonathan؛ Norvig، Peter (2010)، Artificial Intelligence: A Modern Approach، Prentice Hall series in artificial intelligence، Prentice Hall، ص. 282، ISBN:978-0-13-604259-4.

[APT79-4] ا ^ب Aspvall، Bengt؛ Plass، Michael F.؛ Tarjan، Robert E. (1979)، "A linear-time algorithm for testing the truth of certain quantified boolean formulas" (PDF)، Information Processing Letters، ج. 8، ص. 121–123، DOI:10.1016/0020-0190(79)90002-4، مؤرشف من الأصل (PDF) في 2021-05-06.

[EIS76-5] Even، S.؛ Itai، A.؛ Shamir، A. (1976)، "On the complexity of time table and multi-commodity flow problems"، SIAM Journal on Computing، ج. 5، ص. 691–703، DOI:10.1137/0205048.

[1]

[2]

[3]

[4]

[5]