يمكن أن تعمل تقنية حل SAT القوية مع فرضية Collatz سيئة السمعة. ومع ذلك ، فإن فرص ذلك ليست عالية جدًا.
في السنوات القليلة الماضية ، استخدمت Mariin Hijul تقنية إثبات محوسبة تسمى SAT solver (SAT للرضا) للتغلب على قائمة رائعة من المشاكل الرياضية. ثلاثة توائم فيثاغورس في عام 2016 ، رقم 5 لشور في عام 2017 ، ومؤخرًا فرضية كيلر في البعد السابع ، والتي كتبنا عنها منذ وقت ليس ببعيد في مقال " ساعد البحث على الكمبيوتر في التعامل مع مشكلة رياضية عمرها 90 عامًا ".
الآن ، ومع ذلك ، فإن Hijul ، عالم الكمبيوتر في جامعة كارنيجي ميلون ، قد وضع نصب عينيه هدفًا أكثر طموحًا: تخمين Collatz ، الذي يعتبره الكثيرون أصعب مشكلة مفتوحة في الرياضيات (ويمكن القول إنها أبسط صياغة). علماء رياضيات آخرون ، تعلموا مني أن خيول كان يقوم بمثل هذه المحاولة ، كانوا متشككين في ذلك.
قال توماس هالز من جامعة بيتسبرغ ، وهو خبير بارز في أدلة الكمبيوتر: "لا أرى كيف يمكنك حل هذه المشكلة تمامًا باستخدام أداة حل SAT" . تساعد هذه التقنية علماء الرياضيات بشكل أساسي في حل المشكلات - التي يحتوي بعضها على عدد لا حصر له من الخيارات - عن طريق تحويلها إلى مسائل منفصلة ومحدودة.
ومع ذلك ، كان هالس ، مثل الآخرين ، حذرًا من التقليل من شأن خيول. "إنه جيد جدًا في إيجاد طرق ذكية لصياغة المشكلات في لغة SAT. إنه جيد جدًا في ذلك ".
سكوت آرونسونمن جامعة تكساس في أوستن ، بالعمل مع Hijul على تخمين Collatz ، أضاف: "Marin هو رجل بمطرقة ، وهذا هو ، SAT حلالا ، وربما يكون أكثر من يستحق هذه المطرقة في العالم بأسره. ويحاول تطبيقه على كل شيء تقريبًا ". لكن الوقت فقط سيحدد ما إذا كان بإمكانه تحويل فرضية Collatz إلى مسمار.
يتطلب حل SAT إعادة صياغة المشكلات بلغة مفهومة بالكمبيوتر تستخدم المنطق الافتراضي ، ثم توصيل أجهزة الكمبيوتر لتحديد ما إذا كانت هناك طريقة لجعل هذه العبارات صحيحة. هذا مثال بسيط.
لنفترض أنك أحد الوالدين يحاول ترتيب رعاية الطفل. قد تعمل إحدى مربياتك طوال الأسبوع ما عدا الثلاثاء والخميس. الآخر بصرف النظر عن الثلاثاء والجمعة. الثالث - ما عدا الخميس والجمعة. يجب أن تجلس مع طفلك أيام الثلاثاء والخميس والجمعة. هل يمكن تحقيق ذلك؟
إحدى طرق اختبار ذلك هي تحويل قيود المربية إلى صيغة وإدخالها إلى محلل SAT. سيبحث البرنامج عن طريقة لتوزيع الأيام بين المربيات بحيث تصبح الصيغة صحيحة أو "راضية" - أي حتى تحصل على الأيام الثلاثة التي تحتاجها. إذا نجحت ، فستكون هذه الطريقة موجودة.
لسوء الحظ ، ليس من الواضح على الفور كيفية إعادة صياغة العديد من أهم الأسئلة الرياضية في لغة SAT. لكن في بعض الأحيان يمكن إعادة صياغتها كأسئلة رضا بطرق غير متوقعة.
قال آرونسون: "من الصعب التكهن بالوقت الذي سيتم فيه تقليص المهمة إلى حساب ضخم ولكنه محدود".
تخمين Collatz هو أحد أسئلة الرياضيات التي لا تبدو في البداية كمسألة مربية على الإطلاق. تقترح ما يلي: خذ أي رقم (عدد صحيح ، غير صفري). إذا كان الأمر فرديًا ، اضربه في 3 وأضف 1. إذا كان عددًا زوجيًا ، اقسمه على 2. نتيجة لذلك ، تحصل على رقم جديد. طبق نفس القواعد عليه واستمر. تتوقع الفرضية أنه بغض النظر عن رقم البداية ، ينتهي بك الأمر بالرقم 1 ، ثم تتعثر في حلقة: 1 ، 4 ، 2 ، 1.
وعلى الرغم من حقيقة أن هذه الفرضية قد تم العمل بها لما يقرب من 100 عام ، إلا أن علماء الرياضيات لم يقتربوا من إثباتها.
لكن هذا لم يمنع خيول. في عام 2018 ، تلقت هي وأرونسون - أثناء كونهما زميلتين في الجامعة - منحة من مؤسسة العلوم الوطنية لتطبيق SAT solver على تخمين Collatz.
خذ أي رقم. إذا كان الأمر فرديًا ، اضربه في 3 وأضف 1. إذا كان عددًا زوجيًا ، اقسمه على 2. نتيجة لذلك ، تحصل على رقم جديد. طبق نفس القواعد عليه واستمر. هل يمكنك العثور على رقم لا يؤدي إلى 1؟ يمكنك تجربتها بنفسك .
بادئ ذي بدء ، توصل آرونسون ، عالم الكمبيوتر ، إلى صياغة بديلة لفرضية Collatz ، أو ما يسمى بـ. "نظام قواعد الاستبدال" الذي سهّل على أجهزة الكمبيوتر العمل معها.
في نظام قواعد الاستبدال ، أنت تستخدم مجموعة من الأحرف ، مثل الأحرف A و B و C. يمكنك استخدامها لتكوين تسلسلات: ACACBACB. لديك أيضًا قواعد لتحويل هذه التسلسلات. قد تقول إحدى القواعد أنه عندما تقابل AC ، فإنك تستبدلها بـ BC. يمكن للآخرين استبدال الطائرة بـ AAA. يمكنك تحديد أي عدد من القواعد التي تحدد أي تحويلات.
يحتاج علماء الكمبيوتر عمومًا إلى معرفة ما إذا كانت JV معينة تنتهي دائمًا. أي ، بغض النظر عن السطر الذي نبدأ به وبأي ترتيب لتطبيق القواعد ، هل صحيح أن الخط سيتحول في النهاية إلى حالة لا يمكن فيها تطبيق أي قواعد؟
أتى آرونسون بـ SP مع سبعة رموز و 11 قاعدة ، على غرار فرضية Collatz. إذا تمكنوا من إثبات أن شركته المشتركة تنتهي دائمًا ، فسيثبتون بذلك صحة الفرضية.
لتحويل تخمين Collatz إلى مشكلة SAT-solver ، كان على Aaronson و Hiyul اتخاذ خطوة أخرى تتضمن مصفوفات أو مصفوفات من الأرقام. لقد احتاجوا إلى تخصيص مصفوفة فريدة لكل رمز في نقاط SP الخاصة بهم. هذا النهج - طريقة شائعة للبحث عن دليل على أن SP قد أنهى العمل - سيسمح لهم بالتفكير حول تحويلات الأرقام من خلال ضرب المصفوفة. كان على سبع مصفوفات تشير إلى سبعة رموز مع SP تلبية مجموعة كاملة من القيود ، مما يعكس تطابق 11 قاعدة مع بعضها البعض.
قال: "أولاً ، تحاول العثور على مصفوفات تفي بهذه القيود"إيمري يولشو ، طالب دكتوراه في جامعة كارنيجي ميلون ، يعمل على حل هذه المشكلة مع Hijul. "إذا نجحت ، فأنت تثبت أن التنفيذ يتوقف" ، وبالتالي فإن فرضية Collatz صحيحة.
يمكن لمحلل SAT الإجابة على سؤال وجود مصفوفات تفي بهذه القيود. قام Aaronson و Hijul أولاً بتشغيل SAT solver على مصفوفات 2x2 صغيرة. لم يجدوا خيارات العمل. ثم جربوا مصفوفات 3x3. ومرة أخرى دون جدوى. استمروا في زيادة حجم المصفوفات على أمل أن يجدوا المصفوفات التي يحتاجونها.
ومع ذلك ، لا يمكن أن يتطور هذا النهج إلى ما لا نهاية ، حيث إن تعقيد البحث عن المصفوفات المناسبة ينمو بشكل كبير مع حجمها. يقترح حجول أن أجهزة الكمبيوتر الحديثة لا تستطيع ببساطة التعامل مع مصفوفات أكبر من 12 × 12.
قال "عندما تصبح المصفوفات معقدة للغاية ، لا يمكنك حل المشكلة".
لا يزال Hijul يعمل على تحسين البحث ، في محاولة لجعله أكثر كفاءة بحيث يمكن لمحلل SAT التحقق من المصفوفات الأكبر والأكبر. تعمل هي وزملاؤها على مقال يلخص اكتشافاتهم الحالية ، لكنهم على وشك النفاد من الأفكار وربما يتعين عليهم الاستسلام قريبًا - على الأقل لفترة من الوقت.
بعد كل شيء ، فإن جاذبية أداة حل SAT هي أنه إذا كان بإمكانك فقط معرفة كيفية التحقق من حالة أخرى ، والاتصال بمربية أخرى ، وتوسيع نطاق البحث حتى لفترة قصيرة ، فمن المحتمل أن تجد ما كنت تبحث عنه. في هذا المعنى ، قد لا تكون الميزة الرئيسية لخيول هي تجربته مع حلول SAT ، ولكن حبه للسعي لتحقيق النتائج.
قال "أنا مجرد متفائل". "غالبًا ما أشعر أنني محظوظ ، لذلك أحاول فقط أن أرى المدى الذي يمكنني الوصول إليه."