مشكلة إرضاء المنطق البولياني

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

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

تُعدّ مسألة SAT أول مسألة ثبت أنها من فئة NP-complete ، وذلك وفقًا لنظرية كوك-ليفين . وهذا يعني أن جميع المسائل في فئة التعقيد NP ، التي تشمل طيفًا واسعًا من مسائل اتخاذ القرارات والتحسين الطبيعية، لا تتجاوز في صعوبتها مسألة SAT. لا توجد خوارزمية معروفة تحل كل مسألة من مسائل SAT بكفاءة (حيث تعني "بكفاءة" "بشكل حتمي في زمن متعدد الحدود "). ورغم الاعتقاد السائد بعدم وجود مثل هذه الخوارزمية، إلا أن هذا الاعتقاد لم يُثبت أو يُدحض رياضيًا. إن حسم مسألة وجود خوارزمية لمسألة SAT في زمن متعدد الحدود من شأنه أن يحسم مسألة P مقابل NP ، وهي إحدى أهم المسائل المفتوحة في نظرية الحوسبة. [ 1 ] [ 2 ]

ومع ذلك، فإن خوارزميات SAT الاستدلالية قادرة على حل حالات المشكلة التي تتضمن عشرات الآلاف من المتغيرات والصيغ التي تتكون من ملايين الرموز، [ 3 ] وهو ما يكفي للعديد من مشاكل SAT العملية التي تحدث في الذكاء الاصطناعي وتصميم الدوائر ، [ 4 ] وإثبات النظريات التلقائي .

التعريفات

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

الصيغة العادية للوصل

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

على سبيل المثال، x1 هو حرف موجب، و¬ x2 هو حرف سالب، و x1 ∨ ¬x2 جملة. الصيغة ( x1 ∨ ¬x2 ) ∧ ( ¬x1 ∨ x2 ∨ x3 ) ∧ ¬x1 هي صيغة العطف العادية؛ جملتاها الأولى والثالثة جملتان من نوع هورن، بينما جملتها الثانية ليست كذلك . الصيغة قابلة للتحقيق، باختيار x 1  =  FALSE، x 2  =  FALSE، و x 3 بشكل تعسفي، لأن (FALSE ∨ ¬FALSE) ∧ (¬FALSE ∨ FALSE ∨ x 3 ) ∧ ¬FALSE تُقيّم إلى (FALSE ∨ TRUE) ∧ (TRUE ∨ FALSE ∨ x 3 ) ∧ TRUE، وبالتالي إلى TRUE ∧ TRUE ∧ TRUE (أي إلى TRUE). في المقابل، فإن صيغة CNF a ∧ ¬ a ، المكونة من عبارتين من حرف واحد ، غير قابلة للتنفيذ ، لأنه بالنسبة لـ a = TRUE أو a = FALSE فإنها تُقيّم إلى TRUE ∧ ¬TRUE (أي FALSE) أو FALSE ∧ ¬FALSE (أي FALSE مرة أخرى)، على التوالي.

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

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

( x 1  ∨ x 2 ∨ … ∨ x n ) ∧     
( y 1  ∨ x 2 ∨ … ∨ x n ) ∧     
( x 1  ∨ y 2 ∨ … ∨ x n ) ∧     
( ذ 1  ∨ ذ 2 ∨ … ∨ س ن ) ∧ ... ∧     
( x 1  ∨ x 2 ∨ … ∨ yn ) ∧     
( ص 1  ∨ × 2 ∨ … ∨ ذ ن ) ∧     
( س 1  ∨ ذ 2 ∨ … ∨ ذ ن ) ∧     
( ذ 1  ∨ ذ 2 ∨ … ∨ ذ ن )      ;

بينما الأول عبارة عن فصل لـ n من الاقترانات لمتغيرين، فإن الأخير يتكون من 2 n من البنود لـ n من المتغيرات.

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

تعقيد

كانت مسألة SAT أول مسألة تُعرف بأنها مسألة NP-كاملة ، كما أثبت ذلك ستيفن كوك في جامعة تورنتو عام 1971 [ 10 ] ، وبشكل مستقل ليونيد ليفين في الأكاديمية الروسية للعلوم عام 1973 [ 11 ]. حتى ذلك الحين، لم يكن مفهوم مسألة NP-كاملة موجودًا أصلًا. يُبين البرهان كيف يمكن اختزال أي مسألة قرار في فئة التعقيد NP إلى مسألة SAT لصيغ CNF [ a ] ، والتي تُسمى أحيانًا CNFSAT . من الخصائص المفيدة لاختزال كوك أنه يحافظ على عدد الإجابات المقبولة. على سبيل المثال، يُعد تحديد ما إذا كان لرسم بياني مُعطى تلوين ثلاثي مسألة أخرى في NP؛ فإذا كان للرسم البياني 17 تلوينًا ثلاثيًا صحيحًا، فإن صيغة SAT الناتجة عن اختزال كوك-ليفين ستحتوي على 17 تعيينًا مُرضيًا.

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

3- الرضا

تم اختزال مسألة 3-SAT ( x ∨ x ∨ y ) ∧ ( ¬x ∨ ¬y ∨ ¬y ) ∧ (¬x ∨ y ∨ y ) إلى مسألة زمرة . تشكل الرؤوس الخضراء زمرة ثلاثية وتتوافق مع التعيين المُرضي x = FALSE، y = TRUE.

كما هو الحال في مسألة قابلية الإرضاء للصيغ العشوائية، فإن تحديد قابلية إرضاء صيغة في شكلها الطبيعي الاقتراني، حيث يقتصر كل بند على ثلاثة متغيرات حرفية على الأكثر، يُعدّ مسألة NP-كاملة أيضًا؛ وتُسمى هذه المسألة 3-SAT أو 3CNFSAT أو قابلية الإرضاء الثلاثية . ولتبسيط مسألة SAT غير المقيدة إلى 3-SAT، يتم تحويل كل بند l 1 ∨ ⋯ ∨ l n إلى اقتران مكون من n - 2 بندًا .

( l 1 ∨ l 2 ∨ x 2 ) ∧
(¬ x 2 ∨ l 3 ∨ x 3 ) ∧
(¬ x 3 ∨ l 4 ∨ x 4 ) ∧ ⋯ ∧
(¬ x n −3 ∨ l n −2 ∨ x n −2 ) ∧
(¬ x n −2 ∨ l n −1 ∨ l n )

حيث x² ، ... ، xₙ₋₂ متغيرات جديدة لا تظهر في أي مكان آخر. على الرغم من أن الصيغتين ليستا متكافئتين منطقيًا ، إلا أنهما قابلتان للترضية بالتساوي . الصيغة الناتجة عن تحويل جميع البنود لا يزيد طولها عن ثلاثة أضعاف طول الصيغة الأصلية؛ أي أن نمو الطول متعدد الحدود. [ 12 ]

تُعدّ مسألة 3-SAT إحدى مسائل كارب الـ 21 من فئة NP-complete ، وتُستخدم كنقطة انطلاق لإثبات أن مسائل أخرى هي أيضًا من فئة NP-hard . [ ب ] ويتم ذلك عن طريق اختزال مسألة 3-SAT إلى المسألة الأخرى في زمن متعدد الحدود . ومن الأمثلة على المسائل التي استُخدمت فيها هذه الطريقة مسألة الزمرة : فعند إعطاء صيغة CNF تتكون من c بنود، يتكون الرسم البياني المقابل من رأس لكل حرف، وحافة بين كل حرفين غير متناقضين من [ c ] بنود مختلفة؛ انظر الشكل. يحتوي الرسم البياني على زمرة من الرتبة c إذا وفقط إذا كانت الصيغة قابلة للإرضاء. [ 13 ]

توجد خوارزمية عشوائية بسيطة من ابتكار شونينغ (1999) تعمل في زمن (4/3) n حيث n هو عدد المتغيرات في اقتراح 3-SAT، وتنجح باحتمالية عالية في اتخاذ قرار صحيح بشأن 3-SAT. [ 14 ]

تؤكد فرضية الوقت الأسي أنه لا يمكن لأي خوارزمية حل 3-SAT (أو في الواقع k -SAT لأي k > 2 ) في وقت exp( o ( n )) (أي أسرع بشكل أساسي من الأسي في n ).

قدّم سيلمان وميتشل وليفيسك (1996) بيانات تجريبية حول صعوبة صيغ 3-SAT المولدة عشوائيًا، وذلك تبعًا لمعاملات حجمها. وقد قُيست الصعوبة بعدد الاستدعاءات المتكررة التي يُجريها خوارزمية DPLL . وحددوا منطقة انتقال طورية من الصيغ شبه المؤكدة القابلة للإرضاء إلى الصيغ شبه المؤكدة غير القابلة للإرضاء عند نسبة البنود إلى المتغيرات التي تبلغ حوالي 4.26. [ 15 ]

يمكن تعميم مسألة الإرضاء الثلاثي إلى مسألة الإرضاء من الرتبة k ( k -SAT ، أو k -CNF-SAT )، عند النظر في الصيغ المكتوبة بصيغة CNF والتي تحتوي كل فقرة فيها على k متغيرًا حرفيًا كحد أقصى. [ 16 ] ومع ذلك، بما أنه لأي قيمة k ≥ 3 ، فإن هذه المسألة لا يمكن أن تكون أسهل من مسألة الإرضاء الثلاثي ولا أصعب من مسألة الإرضاء الأحادي، وهاتان المسألتان الأخيرتان كاملتان من فئة NP، لذا يجب أن تكون مسألة إرضاء من الرتبة k .

يقصر بعض المؤلفين استخدام k -SAT على صيغ CNF التي تحتوي على k حرفًا بالضبط . ولا يؤدي هذا إلى فئة تعقيد مختلفة، إذ يمكن إضافة نسخ متكررة من نفس الحرف إلى كل بند يحتوي على أقل من k حرفًا. [ 17 ]

تمت دراسة قابلية الإرضاء وهندسة فضاء الحلول لمسائل k -SAT ذات البنود المولدة عشوائيًا إحصائيًا. وكدالة لنسبة البنود إلى المتغيرات (المعروفة أيضًا بالكثافة)، يُظهر النموذج تحولات طورية متنوعة فيما يتعلق بقابلية الإرضاء وهندسة فضاء الحلول. بالنسبة لقابلية الإرضاء، توجد عتبة حادة بحيث يكون هناك احتمال كبير لوجود حل إذا وفقط إذا بقيت الكثافة أقل من هذه العتبة. [ 18 ] ودون عتبة قابلية الإرضاء بكثير، يخضع فضاء الحلول أيضًا لتحول طوري هندسي، أي أنه ينقسم إلى عدد هائل من المجموعات المتباعدة جيدًا. يتزامن بدء هذا التحول الطوري مع العتبة الخوارزمية المعروفة، مما يشير إلى وجود صلة بين الهندسة وصعوبة الحل الخوارزمي. [ 19 ] [ 20 ]

حالات خاصة من 3SAT

الصيغة العادية للوصل

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

قمر صناعي خطي

تُسمى صيغة 3-SAT صيغة SAT خطية ( LSAT ) إذا كان كل بند (يُنظر إليه كمجموعة من المتغيرات) يتقاطع مع بند واحد على الأكثر، وإذا تقاطع بندان، فإنهما يشتركان في متغير واحد فقط. يمكن تمثيل صيغة LSAT كمجموعة من الفترات شبه المغلقة المنفصلة على خط مستقيم. يُعد تحديد ما إذا كانت صيغة LSAT قابلة للإرضاء مسألة NP-كاملة. [ 21 ]

2- الرضا

تُصبح مسألة SAT أسهل إذا اقتصر عدد المتغيرات في كل بند على اثنين على الأكثر، وفي هذه الحالة تُسمى المسألة 2-SAT . يمكن حل هذه المسألة في وقت متعدد الحدود، وهي في الواقع مسألة كاملة لفئة التعقيد NL . إذا تم استبدال جميع عمليات OR في المتغيرات بعمليات XOR ، فإن النتيجة تُسمى مسألة XOR 2-satisfiability ، وهي مسألة كاملة لفئة التعقيد SL = L.

مدى إرضاء القرن

تُسمى مشكلة تحديد إمكانية إرضاء اقتران معين من عبارات هورن بمسألة إرضاء هورن ، أو اختصارًا HORN-SAT . ويمكن حلها في وقت متعدد الحدود بخطوة واحدة من خوارزمية نشر الوحدة ، التي تُنتج النموذج الأدنى الوحيد لمجموعة عبارات هورن (بالنسبة لمجموعة المتغيرات المُخصصة للقيمة TRUE). تُعد مسألة إرضاء هورن مسألة كاملة من فئة P ، ويمكن اعتبارها نسخة P من مسألة إرضاء الصيغ المنطقية. كما يمكن تحديد صحة صيغ هورن الكمية في وقت متعدد الحدود. [ 22 ]

تُعدّ عبارات هورن ذات أهمية لأنها قادرة على التعبير عن استلزام متغير واحد من مجموعة من المتغيرات الأخرى. في الواقع، يمكن إعادة كتابة إحدى هذه العبارات، وهي ¬ x 1 ∨ ... ∨ ¬ x n ∨ y، على النحو التالي: x 1 ∧ ... ∧ x n → y ؛ أي، إذا كانت x 1 ، ...، x n جميعها صحيحة، فإن y يجب أن تكون صحيحة أيضًا.

يُعدّ تعميم فئة صيغ هورن هو صيغ هورن القابلة لإعادة التسمية، وهي مجموعة الصيغ التي يمكن تحويلها إلى صيغة هورن باستبدال بعض المتغيرات بنفيها. على سبيل المثال، الصيغة ( x1 ∨ ¬x2 ) ∧ ( ¬x1 ∨ x2 ∨ x3 ) ∧ ¬x1 ليست صيغة هورن ، ولكن يمكن إعادة تسميتها إلى الصيغة ( x1 ∨ ¬x2 ) ∧ ( ¬x1 ∨ x2 ∨ ¬y3 ) ∧ ¬x1 بإدخال y3 كنفي لـ x3 . على النقيض من ذلك، لا يؤدي أي تغيير في تسمية ( x1 ∨ ¬x2 ∨ ¬x3) ∧ (¬x1 ∨ x2 ∨ x3) ∧ ¬x1 إلى صيغة هورن . يمكن التحقق من وجود مثل هذا الاستبدال في زمن خطي ؛ لذا، فإن قابلية إرضاء هذه الصيغ تقع ضمن P ، حيث يمكن حلها بإجراء هذا الاستبدال أولًا ثم التحقق من قابلية إرضاء صيغة هورن الناتجة .

ليست مشاكل اختبار 3SAT

الصيغة الطبيعية المنفصلة

تُعدّ مسألة SAT بسيطة إذا اقتصرت الصيغ على تلك المكتوبة بالصيغة الانفصالية العادية ، أي أنها عبارة عن فصل بين اقترانات بين متغيرات. وتكون هذه الصيغة قابلة للإرضاء إذا وفقط إذا كان أحد اقتراناتها على الأقل قابلاً للإرضاء، ويكون الاقتران قابلاً للإرضاء إذا وفقط إذا لم يحتوِ على كلٍّ من x و NOT x لمتغير ما x . ويمكن التحقق من ذلك في زمن خطي. علاوة على ذلك، إذا اقتصرت الصيغ على الصيغة الانفصالية العادية الكاملة ، حيث يظهر كل متغير مرة واحدة فقط في كل اقتران، فيمكن التحقق منها في زمن ثابت (يمثل كل اقتران تعيينًا مُرضيًا واحدًا). ​​ولكن قد يستغرق تحويل مسألة SAT عامة إلى الصيغة الانفصالية العادية وقتًا ومساحةً أُسّيين؛ وللحصول على مثال، استبدل الرمزين "∧" و "∨" في مثال التضخم الأُسّي أعلاه بالصيغ الاقترانية العادية.

الرضا التام -1 3

يُعدّ نوعٌ آخر من مسائل NP-complete لمسألة إرضاء ثلاثة متغيرات هو مسألة إرضاء ثلاثة متغيرات من نوع واحد من ثلاثة (المعروفة أيضًا باسم 1-in-3-SAT و 3-SAT-1 بالضبط ). في هذه المسألة، عند إعطاء صيغة اقترانية عادية بثلاثة متغيرات لكل جملة، يكمن المطلوب في تحديد ما إذا كان هناك تعيينٌ منطقي للمتغيرات بحيث تحتوي كل جملة على متغير صحيح واحد فقط (وبالتالي متغيرين خاطئين فقط).

مستوى الرضا 3 غير متساوٍ

هناك صيغة أخرى تُعرف بمسألة عدم تساوي جميع المتغيرات الثلاثة ( NAE3SAT ). في هذه المسألة، عند إعطاء صيغة اقترانية عادية بثلاثة متغيرات حرفية لكل جملة، يكمن المطلوب في تحديد ما إذا كان هناك تعيين للمتغيرات بحيث لا يكون للمتغيرات الثلاثة في أي جملة نفس القيمة المنطقية. وتُصنف هذه المسألة ضمن مسائل NP-complete، حتى في حال عدم السماح برموز النفي، وذلك وفقًا لنظرية شيفر الثنائية. [ 23 ]

قابلية إرضاء XOR

ثمة حالة خاصة أخرى تتمثل في فئة المسائل التي تحتوي كل جملة فيها على عامل XOR (أي XOR الحصري ) بدلاً من عامل OR (العادي). وتندرج هذه المسألة ضمن فئة P ، حيث يمكن اعتبار صيغة XOR-SAT نظام معادلات خطية بتردد 2، ويمكن حلها في زمن مكعب باستخدام طريقة الحذف الغاوسي . [ 24 ]

نظرية شيفر الثنائية

القيود المذكورة أعلاه (CNF، 2CNF، 3CNF، Horn، XOR-SAT) تقيد الصيغ المعتبرة لتكون اقترانات من الصيغ الفرعية؛ كل قيد يحدد شكلاً محدداً لجميع الصيغ الفرعية: على سبيل المثال، لا يمكن أن تكون العبارات الثنائية إلا صيغاً فرعية في 2CNF.

تنص نظرية شيفر الثنائية على أنه لأي قيد على الدوال البولية التي يمكن استخدامها لتكوين هذه الصيغ الفرعية، فإن مسألة الإرضاء المقابلة تقع ضمن فئة P أو NP-كاملة. وتُعد عضوية صيغ 2CNF وHorn وXOR-SAT في فئة P حالات خاصة من هذه النظرية. [ 23 ]

يلخص الجدول التالي بعض المتغيرات الشائعة لاختبار SAT.

اسمشفرةمشكلة في اختبار 3SAT؟قيودمتطلباتفصل
3- الرضا3SATنعمتحتوي كل جملة على 3 متغيرات حرفية.يجب أن يكون أحد العبارات الحرفية على الأقل صحيحاً.NP-c
2- الرضا2SATنعمتحتوي كل جملة على حرفين.يجب أن يكون أحد العبارات الحرفية على الأقل صحيحاً.NL-c
بالضبط -1 3-SAT1-in-3-SATلاتحتوي كل جملة على 3 متغيرات حرفية.يجب أن يكون أحد العبارات الحرفية صحيحًا.NP-c
نتيجة واحدة إيجابية بالضبط في اختبار 3-SAT1-in-3-SAT+لاتحتوي كل جملة على 3 متغيرات حرفية إيجابية.يجب أن يكون أحد العبارات الحرفية صحيحًا.NP-c
مستوى الرضا 3 غير متساوٍNAE3SATلاتحتوي كل جملة على 3 متغيرات حرفية.يجب أن يكون أحد المتغيرات الحرفية أو اثنان صحيحين.NP-c
نتائج اختبار 3-SAT الإيجابية غير متساويةNAE3SAT+لاتحتوي كل جملة على 3 متغيرات حرفية إيجابية.يجب أن يكون أحد المتغيرات الحرفية أو اثنان صحيحين.NP-c
قمر صناعي مستويPL-SATنعمالرسم البياني للوقوع (الرسم البياني للمتغيرات الشرطية) يكون مستوياً .يجب أن يكون أحد العبارات الحرفية على الأقل صحيحاً.NP-c
قمر صناعي خطيLSATنعمتحتوي كل جملة على 3 متغيرات حرفية، وتتقاطع مع جملة أخرى واحدة على الأكثر، ويكون التقاطع متغيرًا حرفيًا واحدًا بالضبط.يجب أن يكون أحد العبارات الحرفية على الأقل صحيحاً.NP-c
مدى إرضاء القرنHORN-SATنعمعبارات هورن (بحد أقصى حرف إيجابي واحد).يجب أن يكون أحد العبارات الحرفية على الأقل صحيحاً.جهاز كمبيوتر
قابلية الإرضاء XorXOR-SATلاتحتوي كل فقرة على عمليات XOR بدلاً من OR.يجب أن تكون عملية XOR لجميع القيم الحرفية صحيحة.P

امتدادات اختبار SAT

أحد التوسعات التي اكتسبت شعبية كبيرة منذ عام 2003 هو قابلية الإرضاء المعيارية للنظريات ( SMT ) التي يمكنها إثراء صيغ CNF بالقيود الخطية والمصفوفات والقيود المختلفة تمامًا والدوال غير المفسرة ، [ 25 ] وما إلى ذلك. عادة ما تظل هذه التوسعات NP-كاملة، ولكن تتوفر الآن حلول فعالة للغاية يمكنها التعامل مع العديد من هذه الأنواع من القيود.

تصبح مسألة الإرضاء أكثر تعقيدًا إذا سُمح باستخدام كلٍّ من مُحدِّدات الكمية "لكل" ( ∀ ) و"يوجد" ( ∃ ) لربط المتغيرات المنطقية. مثال على ذلك: ∀ x ∀ y ∃ z ( x ∨ y ∨ z ) ∧ (¬ x ∨ ¬ y ∨ ¬ z ) ؛ وهي صحيحة، لأنه لكل قيم x و y ، يمكن إيجاد قيمة مناسبة لـ z ، أي z = TRUE إذا كانت كل من x و y خاطئة، و z = FALSE فيما عدا ذلك. تستخدم مسألة الإرضاء (ضمنًا) مُحدِّدات الكمية ∃ فقط. أما إذا سُمح باستخدام مُحدِّدات الكمية ∀ فقط، فستظهر ما يُسمى بمسألة التكرار ، وهي مسألة كاملة من فئة NP . إذا سُمح بأي عدد من كلا المُكمِّمين، تُسمى المسألة مسألة الصيغة البولية الكمية ( QBF )، والتي يمكن إثبات أنها مسألة كاملة في فئة PSPACE . ويُعتقد على نطاق واسع أن مسائل PSPACE الكاملة أصعب بكثير من أي مسألة في فئة NP، على الرغم من أن هذا لم يُثبت بعد.

يسأل اختبار SAT العادي عما إذا كان هناك على الأقل تعيين واحد للمتغيرات يجعل الصيغة صحيحة. وتتناول العديد من الصيغ المختلفة عدد هذه التعيينات:

  • يسأل MAJ-SAT عما إذا كان نصف جميع التعيينات على الأقل يجعل الصيغة صحيحة. ومن المعروف أنها كاملة بالنسبة لـ PP ، وهي فئة احتمالية. والمثير للدهشة أنه تم إثبات أن MAJ-kSAT تنتمي إلى P لكل عدد صحيح محدود k. [ 26 ]
  • #SAT ، وهي مشكلة حساب عدد تعيينات المتغيرات التي تحقق صيغة معينة، هي مشكلة عد وليست مشكلة قرار، وهي #P-كاملة .
  • تُعرف مسألة UNIQUE SAT [ 27 ] بأنها مسألة تحديد ما إذا كانت الصيغة تحتوي على تعيين واحد فقط. وهي كاملة بالنسبة لفئة التعقيد US [ 28 ]، التي تصف المسائل القابلة للحل بواسطة آلة تورينغ ذات زمن متعدد الحدود غير حتمي، والتي تقبل الصيغة عندما يكون هناك مسار قبول غير حتمي واحد فقط ، وترفضها في غير ذلك.
  • يُطلق اسم UNAMBIGUOUS-SAT على مسألة الإرضاء عندما يُضمن أن يكون للصيغة المدخلة قيمة واحدة مُرضية على الأكثر. تُعرف هذه المسألة أيضًا باسم USAT . [ 29 ] يُسمح لخوارزمية حل UNAMBIGUOUS-SAT بإظهار أي سلوك، بما في ذلك التكرار اللانهائي، على صيغة لها عدة قيم مُرضية. على الرغم من أن هذه المسألة تبدو أسهل، فقد أثبت فاليانت وفازيراني [ 30 ] أنه إذا وُجدت خوارزمية عملية (أي خوارزمية عشوائية متعددة الحدود ) لحلها، فإنه يُمكن حل جميع مسائل NP بسهولة مماثلة.
  • مسألة MAX-SAT ، أو مسألة الإرضاء الأقصى ، هي تعميم من نوع FNP لمسألة SAT. تُطرح هذه المسألة مسألة إيجاد أكبر عدد من البنود التي يمكن تحقيقها بأي عملية إسناد. تتميز هذه المسألة بخوارزميات تقريبية فعّالة ، إلا أنها تُصنف ضمن مسائل NP-hard لحلها بدقة. والأسوأ من ذلك، أنها تُصنف ضمن مسائل APX -complete، مما يعني أنه لا يوجد مخطط تقريبي ذو زمن متعدد الحدود (PTAS) لهذه المسألة إلا إذا كانت P=NP.
  • تُعرف مسألة WMSAT بأنها إيجاد تعيين ذي وزن أدنى يحقق صيغة منطقية رتيبة (أي صيغة بدون نفي). تُعطى أوزان المتغيرات المنطقية في مدخلات المسألة. وزن التعيين هو مجموع أوزان المتغيرات الصحيحة. هذه المسألة مصنفة ضمن مسائل NP-كاملة (انظر النظرية 1 من [ 31 ] ).

وتشمل التعميمات الأخرى إمكانية الإرضاء لمنطق الرتبة الأولى والثانية ، ومشاكل إرضاء القيود ، والبرمجة العددية 0-1 .

إيجاد مهمة مُرضية

على الرغم من أن مسألة SAT هي مسألة قرار ، إلا أن مسألة البحث عن تعيين مُرضٍ تُختزل إلى مسألة SAT. أي أن كل خوارزمية تُجيب بشكل صحيح عما إذا كانت حالة معينة من SAT قابلة للحل، يُمكن استخدامها لإيجاد تعيين مُرضٍ. أولًا، يُطرح السؤال على الصيغة المُعطاة Φ. إذا كانت الإجابة "لا"، فإن الصيغة غير قابلة للحل. وإلا، يُطرح السؤال على الصيغة المُطبقة جزئيًا Φ { x 1 = TRUE } ، أي Φ مع استبدال المتغير الأول x 1 بالقيمة TRUE، وتبسيطها وفقًا لذلك. إذا كانت الإجابة "نعم"، فإن x 1 = TRUE، وإلا فإن x 1 = FALSE. يُمكن إيجاد قيم المتغيرات الأخرى لاحقًا بنفس الطريقة. إجمالًا، يلزم تشغيل الخوارزمية n + 1 مرة، حيث n هو عدد المتغيرات المختلفة في Φ.

تُستخدم هذه الخاصية في العديد من النظريات في نظرية التعقيد:

خوارزميات لحل اختبار SAT

التعقيد الأسي لحل اختبار SAT مقابل عدد المتغيرات، وعدد البنود، وطول الصيغة

نظرًا لأن مسألة SAT مصنفة ضمن فئة NP-complete، فإن الخوارزميات المعروفة لحلها تقتصر على تلك ذات التعقيد الأسي في أسوأ الحالات. مع ذلك، فقد طُوّرت خوارزميات فعّالة وقابلة للتوسع لحل SAT خلال العقد الأول من الألفية الثانية، مما ساهم في تحقيق تقدم كبير في القدرة على حل مسائل تتضمن عشرات الآلاف من المتغيرات وملايين القيود (أي البنود) تلقائيًا. [ 3 ] تشمل أمثلة هذه المسائل في أتمتة تصميم الإلكترونيات (EDA) التحقق الرسمي من التكافؤ ، والتحقق من النماذج ، والتحقق الرسمي من المعالجات الدقيقة ذات البنية الأنبوبية ، [ 25 ] والتوليد التلقائي لأنماط الاختبار ، وتوجيه الدوائر المتكاملة القابلة للبرمجة (FPGAs) ، [ 32 ] ومسائل التخطيط والجدولة ، وغيرها. كما يُعتبر محرك حل SAT عنصرًا أساسيًا في مجموعة أدوات أتمتة تصميم الإلكترونيات .

تشمل التقنيات الرئيسية المستخدمة في خوارزميات حل مشكلة SAT الحديثة خوارزمية ديفيس-بوتنام-لوغمان-لوفلاند (DPLL)، وخوارزمية تعلم البنود القائمة على التعارض (CDCL)، وخوارزميات البحث المحلي العشوائي مثل WalkSAT . تتضمن جميع خوارزميات حل مشكلة SAT تقريبًا خاصية انتهاء المهلة، لذا ستتوقف في وقت معقول حتى لو لم تتمكن من إيجاد حل. تختلف خوارزميات حل مشكلة SAT في سهولة أو صعوبة حل بعض الحالات، فبعضها يتفوق في إثبات عدم إمكانية الحل، والبعض الآخر في إيجاد الحلول. وقد بُذلت محاولات حديثة لتعلم إمكانية حل مشكلة ما باستخدام تقنيات التعلم العميق . [ 33 ]

يتم تطوير برامج حل مسائل SAT ومقارنتها في مسابقات حل مسائل SAT. [ 34 ] كما أن لبرامج حل مسائل SAT الحديثة تأثيراً كبيراً على مجالات التحقق من البرمجيات، وحل القيود في الذكاء الاصطناعي، وبحوث العمليات ، وغيرها.

تم تقديم خوارزميات نظرية ذات ضمانات أفضل لوقت التشغيل في أسوأ الحالات خلال العقود الماضية، بما في ذلكيا*(1.0638ل){\displaystyle O^{*}(1.0638^{L})}خوارزمية لمجموعات الجمل ذات الطول (إجمالي عدد الأحرف)ل{\displaystyle L}، [ 35 ] [ 36 ] ويا*(1.2226م){\displaystyle O^{*}(1.2226^{م})}خوارزمية لمجموعات منم{\displaystyle m}البنود، [ 37 ] [ 38 ] ويا*(1.32793ن){\displaystyle O^{*}(1.32793^{n})}خوارزمية لـ 3-SAT معن{\displaystyle n}المتغيرات. [ 39 ] هنا، الرمز "يا*(.){\displaystyle O^{*}(.)}" تعني "حتى عامل متعدد الحدود"، أييا*(و(ن))=يا(و(ن)نيا(1)){\displaystyle O^{*}(f(n))=O(f(n)n^{O(1)})}تظهر ضمانات وقت التشغيل السابقة في الرسم التخطيطي.

انظر أيضاً

ملحوظات

  1. ↑ مشكلة SAT للصيغ العشوائية هي NP-كاملة أيضًا، لأنه من السهل إثبات أنها في NP، ولا يمكن أن تكون أسهل من SAT لصيغ CNF.
  2. ↑ أي أنها على الأقل بنفس صعوبة أي مشكلة أخرى في فئة NP. تُعتبر مشكلة القرار كاملة من فئة NP إذا وفقط إذا كانت تنتمي إلى فئة NP وكانت صعبة من فئة NP.
  3. ↑ أي بحيث لا يكون أحد المتغيرين نفيًا للآخر

مراجع

  1. ↑ فورتناو، ل. (2009). "وضع مشكلة P مقابل NP" (ملف PDF) . اتصالات ACM . 52 (9): 78-86 . doi : 10.1145/1562164.1562186 . S2CID 5969255 . 
  2. ↑ فورتناو، ل. (2021). "خمسون عامًا من P مقابل NP وإمكانية المستحيل" (ملف PDF) . وقائع مؤتمر ACM (مؤتمر 2017) .
  3. 1 2 أوهريمينكو، أولغا؛ ستوكي، بيتر جيه؛ كوديش، مايكل (2007)، "الانتشار = توليد العبارات الكسولة"، مبادئ وممارسة البرمجة المقيدة - CP 2007 ، سلسلة محاضرات في علوم الحاسوب، المجلد 4741، الصفحات 544-558 ، CiteSeerX 10.1.1.70.5471 ، doi : 10.1007/978-3-540-74970-7_39 ، ISBN    978-3-540-74969-1تستطيع برامج حل مشكلة SAT الحديثة في كثير من الأحيان التعامل مع المشكلات التي تحتوي على ملايين القيود ومئات الآلاف من المتغيرات..
  4. ↑ هونغ، تيد؛ لي، يانجينغ؛ بارك، سونغ-بوم؛ موي، ديانا؛ لين، ديفيد؛ كاليق، زياد عبد؛ حكيم، نجيب؛ نعيمي، هيليا؛ غاردنر، دونالد س.؛ ميترا، سوبهاشيش (نوفمبر 2010). "QED: اختبارات الكشف السريع عن الأخطاء للتحقق الفعال بعد تصنيع السيليكون". المؤتمر الدولي للاختبارات IEEE لعام 2010. الصفحات 1-10 . doi : 10.1109/TEST.2010.5699215 . ISBN  978-1-4244-7206-2. S2CID 7909084 . 
  5. ↑ كارب، ريتشارد م. (1972). "قابلية الاختزال بين المسائل التوافقية" (ملف PDF) . في: ريموند إي. ميلر؛ جيمس دبليو. ثاتشر (محرران). تعقيد الحسابات الحاسوبية . نيويورك: بلينوم. ص 85-103 . ISBN  0-306-30707-3أُرشف من النسخة الأصلية (PDF) بتاريخ 29-06-2011 . تم الاطلاع عليه بتاريخ 07-05-2020 .هنا: صفحة 86
  6. ↑ أهو، ألفريد ف.؛ هوبكروفت، جون إي.؛ أولمان، جيفري د. (1974). تصميم وتحليل خوارزميات الحاسوب . أديسون-ويسلي. ص 403. ISBN  0-201-00029-6.
  7. ↑ ماساتشي، فابيو؛ مارارو، لورا (1 فبراير 2000). "التحليل المنطقي للشفرات كمسألة SAT". مجلة الاستدلال الآلي . 24 (1): 165-203 . doi : 10.1023/A:1006326723002 . S2CID 3114247 . 
  8. ↑ ميرونوف، إيليا؛ تشانغ، لينتاو (2006). "تطبيقات خوارزميات حل SAT على تحليل تشفير دوال التجزئة" . في: بيير، أرمين؛ غوميز، كارلا ب. (محرران). نظرية وتطبيقات اختبار قابلية الإرضاء - SAT 2006. سلسلة محاضرات في علوم الحاسوب. المجلد 4121. سبرينغر. الصفحات 102-115 . doi : 10.1007/11814948_13 . ISBN   978-3-540-37207-3.
  9. ↑ فيزل، ي.؛ فايسنباخر، ج.؛ مالك، س. (2015). "حلول قابلية الإرضاء المنطقية وتطبيقاتها في التحقق من النماذج". وقائع معهد مهندسي الكهرباء والإلكترونيات . 103 (11): 2021-2035 . doi : 10.1109/JPROC.2015.2455034 . S2CID 10190144 . 
  10. ↑ كوك، ستيفن أ. (1971). "تعقيد إجراءات إثبات النظريات" (ملف PDF) . وقائع الندوة السنوية الثالثة لجمعية ACM حول نظرية الحوسبة - STOC '71 . الصفحات 151-158 . CiteSeerX 10.1.1.406.395 . doi : 10.1145/800157.805047 . S2CID 7573663. مؤرشف (ملف PDF) من الأصل بتاريخ 2022-10-09.   
  11. ^ ليفين ، ليونيد (1973). "مشاكل البحث الشامل (بالروسية: Унивенсальные задачи пебора, Universal'nye perebornye zadachi)". مشاكل نقل المعلومات (بالروسية: Проблемы Педачи Информа́ции، مشكلة Peredachi Informatsii) . 9 (3): 115- 116.(ملف PDF) (باللغة الروسية) ، ترجمة تراختنبروت، بكالوريوس (1984). "دراسة استقصائية للمناهج الروسية في خوارزميات البحث الشامل ( بيريبور )". حوليات تاريخ الحوسبة . 6 (4): 384-400 . رمز Bibcode : 1984IAHC....6d.384T . doi : 10.1109/MAHC.1984.10036 . S2CID 950581 . 
  12. ↑ أهو، هوبكروفت وأولمان (1974) ، النظرية 10.4.
  13. ↑ أهو، هوبكروفت وأولمان (1974) ، النظرية 10.5.
  14. ↑ شونينغ، أوفه (أكتوبر 1999). "خوارزمية احتمالية لمسائل k-SAT ومسائل إرضاء القيود" (ملف PDF) . الندوة السنوية الأربعون حول أسس علوم الحاسوب (رقم التصنيف 99CB37039) . الصفحات 410-414 . doi : 10.1109/SFFCS.1999.814612 . ISBN  0-7695-0409-4. S2CID 123177576 . مؤرشف (PDF) من الأصل بتاريخ 2022-10-09. 
  15. ↑ سيلمان، بارت؛ ميتشل، ديفيد؛ ليفيسك، هيكتور (1996). "توليد مسائل الإرضاء الصعبة". الذكاء الاصطناعي . 81 ( 1-2 ): 17-29 . CiteSeerX 10.1.1.37.7362 . doi : 10.1016/0004-3702(95)00045-3 . 
  16. ^ وزيراني، فيجاي ف. (2001). خوارزميات التقريب . برلين: سبرينغر-فيرلاغ. ص. 343. ردمك  3-540-65367-8MR 1851303 .​ 
  17. ↑ باباديميتريو، كريستوس هـ. (1994). التعقيد الحسابي . ريدينغ، ماساتشوستس: شركة أديسون-ويسلي للنشر. ص 183. ISBN  0-201-53082-1MR 1251285​​ 
  18. ↑ دينغ، جيان؛ سلاي، آلان؛ صن، نايكي (2022). "إثبات تخمين قابلية الإرضاء لقيم k الكبيرة " . حوليات الرياضيات . السلسلة الثانية. 196 (1): 1-388 . doi : 10.4007/annals.2022.196.1.1 .
  19. ↑ كرزاكالا، فلورنت؛ مونتاناري، أندريا؛ ريتشي-تيرسينغي، فيديريكو؛ سيميرجيان، غيلهيم؛ زديبوروفا، لينكا (19-06-2007). "حالات جيبس ​​ومجموعة حلول مسائل إرضاء القيود العشوائية". وقائع الأكاديمية الوطنية للعلوم . 104 (25): 10318-10323 . doi : 10.1073/pnas.0703685104 .
  20. ↑ أخليوبتاس، ديميتريس؛ كوجا-أوغلان، أمين (2008). "العوائق الخوارزمية الناتجة عن التحولات الطورية". المؤتمر السنوي التاسع والأربعون لجمعية مهندسي الكهرباء والإلكترونيات حول أسس علوم الحاسوب، FOCS 2008، فيلادلفيا، بنسلفانيا، الولايات المتحدة الأمريكية، 25-28 أكتوبر 2008. جمعية مهندسي الكهرباء والإلكترونيات. الصفحات 793-802 . arXiv : 0803.2122 . doi : 10.1109/FOCS.2008.11 . 
  21. ↑ أركين، إستر م.؛ بانيك، أريترا؛ كارمي، باز؛ سيتوفسكي، غوي؛ كاتز، ماثيو ج.؛ ميتشل، جوزيف س.ب.؛ سيماكوف، مارينا (11-12-2018). "اختيار وتغطية النقاط الملونة" . الرياضيات التطبيقية المنفصلة . 250 : 75-86 . doi : 10.1016/j.dam.2018.05.011 . ISSN 0166-218X . 
  22. ↑ بونينغ، إتش كيه؛ كاربينسكي، ماريك؛ فلوغل، أ. (1995). "حل الصيغ المنطقية الكمية" . المعلومات والحوسبة . 117 (1). إلسيفير: 12-18 . doi : 10.1006/inco.1995.1025 .
  23. 1 2 شيفر، توماس ج. (1978). "تعقيد مسائل الإرضاء" (ملف PDF) . وقائع الندوة السنوية العاشرة لجمعية ACM حول نظرية الحوسبة . سان دييغو، كاليفورنيا. الصفحات 216-226 . CiteSeerX 10.1.1.393.8951 . doi : 10.1145/800133.804350 .  
  24. ↑ مور، كريستوفر ؛ ميرتنز، ستيفان (2011)، طبيعة الحوسبة ، مطبعة جامعة أكسفورد، ص 366، ISBN  9780199233212.
  25. 1 2 R. E. Bryant, SM German, and MN Velev, Microprocessor Verification Using Efficient Decision Procedures for a Logic of Equality with Uninterpreted Functions , in Analytic Tableaux and Related Methods, pp. 1–13, 1999.
  26. ↑ أكمل، شيان؛ ويليامز، رايان (2022). مسألة إرضاء الأغلبية الثلاثية (والمسائل ذات الصلة) في وقت متعدد الحدود . الصفحات 1033-1043 . arXiv : 2107.02748 . doi : 10.1109/FOCS52979.2021.00103 . ISBN  978-1-6654-2055-6.
  27. ↑ بلاس، أندرياس؛ غوريفيتش، يوري (1982-10-01). "حول مسألة الإرضاء الفريد" . المعلومات والتحكم . 55 (1): 80-88 . doi : 10.1016/S0019-9958(82)90439-9 . hdl : 2027.42/23842 . ISSN 0019-9958 . 
  28. ↑ "حديقة حيوانات التعقيد: يو - حديقة حيوانات التعقيد" . complexzoo.uwaterloo.ca . مؤرشف من الأصل بتاريخ 2019-07-09 . تم الاطلاع عليه بتاريخ 2019-12-05 .
  29. ↑ كوزين، ديكستر سي. (2006). "المحاضرة التكميلية F: إمكانية الإرضاء الفريدة" . نظرية الحوسبة . نصوص في علوم الحاسوب. سبرينغر. ص 180. ISBN  9781846282973.
  30. ↑ فاليانت، ل.؛ فازيراني، ف. (1986). "NP سهل مثل اكتشاف الحلول الفريدة" (ملف PDF) . علوم الحاسوب النظرية . 47 : 85-93 . doi : 10.1016/0304-3975(86)90135-0 .
  31. ↑ بولداس، أهتو؛ لينين، ألكسندر؛ ويليمسون، يان؛ شارنامورد، أنطون (2017). "شهادات عدم الجدوى البسيطة لأشجار الهجوم". في: أوبانا، ساتوشي؛ تشيدا، كوجي (محرران). التطورات في أمن المعلومات والحاسوب . سلسلة محاضرات في علوم الحاسوب. المجلد 10418. دار نشر سبرينغر الدولية. الصفحات 39-55 . doi : 10.1007/978-3-319-64200-0_3 . ISBN   9783319642000.
  32. ↑ جي-جون نام؛ ساكالا، ك.أ؛ روتنبار، ر.أ (2002). "نهج جديد للتوجيه التفصيلي لـ FPGA عبر قابلية الإرضاء المنطقية القائمة على البحث" (ملف PDF) . معاملات IEEE في التصميم بمساعدة الحاسوب للدوائر والأنظمة المتكاملة . 21 (6): 674. رمز Bibcode : 2002ITCAD..21..674N . doi : 10.1109/TCAD.2002.1004311 . مؤرشف من الأصل (ملف PDF) بتاريخ 15-03-2016 . تم الاسترجاع بتاريخ 04-09-2015 .
  33. ↑ سيلسام، دانيال؛ لام، ماثيو؛ بونز، بينيديكت؛ ليانغ، بيرسي ؛ دي مورا، ليوناردو؛ ديل، ديفيد ل. (11 مارس 2019). "تعلم خوارزمية حل SAT من خلال الإشراف أحادي البت". arXiv : 1802.03685 [ cs.AI ].
  34. ↑ "صفحة الويب الخاصة بمسابقات SAT الدولية" . تم الاطلاع عليها بتاريخ 15-11-2007 .
  35. ↑ جونكيانغ بنغ ومينغيو شياو (أغسطس 2022). تحسينات إضافية لـ SAT من حيث طول الصيغة (تقرير فني). arXiv : 2105.06131 .
  36. ↑ جونكيانغ بنغ ومينغيو شياو (أكتوبر 2023). "تحسينات إضافية لـ SAT من حيث طول الصيغة". المعلومات والحوسبة . 294 105085: رقم المقالة 105085. doi : 10.1016/j.ic.2023.105085 .
  37. ↑ هوايروي تشو ومينغيو شياو وتشي تشانغ (يوليو 2020). حد أعلى مُحسَّن لـ SAT (تقرير فني). arxiv. arXiv : 2007.03829 .
  38. ↑ هوايروي تشو ومينغيو شياو وتشي تشانغ (أكتوبر 2021). "حد أعلى مُحسَّن لمسألة SAT". علوم الحاسوب النظرية . 887 : 51-62 . doi : 10.1016/j.tcs.2021.06.045 .
  39. ↑ إس. ليو (يوليو 2018). آي. تشاتزيجياناكيس، سي. كاكلامانيس، دي. ماركس، ودي. سانيلا (محررون). سلسلة، تعميم رمز التغطية، وخوارزمية حتمية لـ k -SAT . وقائع المؤتمر الدولي لعلوم الحاسوب والبرمجة (ICALP). المجلد 107. شلوس داغشتول. الصفحات 88:1-13. doi : 10.4230/LIPIcs.ICALP.2018.88 .  

مصادر

  • يتضمن هذا المقال مواد من https://web.archive.org/web/20070708233347/http://www.sigda.org/newsletter/2006/eNews_061201.html بقلم البروفيسور كارم أ. ساكالا .

للمزيد من القراءة

(بحسب تاريخ النشر)