كيف تعمل خوارزمية تارجان لـ 2-SAT

Question

تعتمد خوارزمية Tarjan لـ 2-SAT على الحقيقة:

تكون صيغة 2-CNF مرضية فقط إذا لم يكن هناك متغير ينتمي إلى نفس المكون المرتبط بقوة مثل نفيه.

لكنني لا أجد أي سبب للاتجاه من اليمين إلى اليسار.فكيف يمكن لعدم وجود مثل هذا المتغير أن يضمن رضا CNF؟

حاولت اتباع خطوات الخوارزمية، وعلقت هنا:

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

أليس من الممكن أن يكون المتغير قد تم تعيينه بشكل خاطئ بالفعل؟عندما نستمر في تعيين TRUE من الخلف، ونقوم بتعيين FALSE في المنتصف، ولكن سيتم تخصيص TRUE للمتغير التالي.في هذه الحالة، فواصل الجدوى.

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

• أعتقد أن سبب إمكانية هذه المهمة يتعلق بحالة الانحراف المتماثل للرسم البياني، حيث أن (x -> ~x -> y -> ~y) لا تحتوي أبدًا على تعيينات حقيقية.

Answer 1

تكون صيغة 2-CNF مرضية فقط إذا لم يكن هناك متغير ينتمي إلى نفس المكون المرتبط بقوة مثل نفيه.

لكنني لا أجد أي سبب للاتجاه من اليمين إلى اليسار.فكيف يمكن لعدم وجود مثل هذا المتغير أن يضمن رضا CNF؟

فكر في تخصيص متغير لبعض مثيلات 2-SAT غير المرضية.وهذا يعني أن بندًا واحدًا أو أكثر يجب أن يظل غير مستوفٍ مهما كانت المهمة.يمكنك تغيير إعداد متغير واحد أو أكثر لتلبية هذه البنود، ولكن هذا يترك حتماً بعض الجمل أو البنود الجديدة غير مرضية لأن المثيل غير مرضٍ.إن فشل التغيير في تلبية المثيل يعني أن قيمة بعض المتغيرات الأخرى يجب أن تتغير.تكرر الإجراء مرارًا وتكرارًا، مع تغيير المتغيرات الأخرى حسب ما يتطلبه الأمر ضمنيًا، ولكنك لا تنجح أبدًا في تلبية جميع البنود.في النهاية، نظرًا لأن عدد المتغيرات محدود، فإن الفشل يعني أنك تقوم بتغيير قيمة المتغير الذي قمت بزيارته بالفعل...وهذا هو ضمنا التعميم الخاص بك من $x$ ل $\بار{س}$ ارجع الى $x$.بدون التضمين الدائري، ستصل في النهاية إلى نهاية سلسلة التضمين وسيكون لديك مهمة مُرضية.الطريقة الوحيدة لعدم الوصول إلى نهاية السلسلة هي أن تكون السلسلة دائرية بين المتغير ونفيه.