عباس پالاش
عباس پالاش
خواندن ۱۲ دقیقه·۴ سال پیش

احتمال حل حدس کلاتز با SAT

حدس کلاتز Collatz

یکی از مسایل ساده و سرسخت ریاضی حدس کلاتز است. توضیح حدس کلاتز بسیار ساده است ولی اثبات درستی یا رد درستی آن نزدیک به ۱ قرن است که ریاضیدانان را به چالش کشانده است.
یک عدد طبیعی را انتخاب کنید،
اگر عدد زوج بود آن را تقسیم بر ۲ می‌کنیم
اگر عدد فرد بود آن را ۳ برابر کرده با ۱ جمع می‌کنیم

حدس کلاتز می‌گوید هر عدد طبیعی انتخاب کنید نهایتا به ۱ می‌رسید، در واقع در حلقه تکراری ۱ و ۴و ۲و ۱ گیر خواهید کرد.
مثلا عدد ۶ را در نظر بگیرید.
سری کلاتز آن می‌شود
۶، ۳، ۱۰، ۵، ۱۶، ۸، ۴، ۲، ۱

عدد ۴۳۷

۴۳۷، ۱۳۱۲، ۶۵۶، ۳۲۸، ۱۶۴، ۸۲، ۴۱، ۱۲۴، ۶۲، ۳۱، ۹۴، ۴۷، ۱۴۲، 71، 214، ۱۰۷، ۳۲۲، 161، ۴۸۴، 242، 121، 364، ۱۸۲، ۹۱، ۲۷۴، ۱۳۷، 412، 206، 103، 310، 155، 466، 233، 700، 350، 175، 526، 263، 790، 395، 1186، 593، 1780، 890، 445، 1336، 668، 334، 167، 502، 251، 754، 377، 1132، 566، 283، 850، 425، 1276، 638، 319، 958، 479، 1438، 719، 2158، 1079، 3238، 1619، 4858، 2429، 7288، 3644، 1822، 911، 2734، 1367، 4102، 2051، 6154، 3077، 9232، 4616، 2308، 1154، 577، 1732، 866، 433، 1300، 650، 325، 976، 488، 244، 122، 61، 184، 92، 46، 23، 70، 35، 106، 53، 160، 80، 40، 20، 10، 5، 16، 8، 4، 2، 1

بالاخره!

مثال‌هایی از سری کلاتز برای اعداد ۱۱، ۱۳، ۳۲۰ و ۶۴۰
مثال‌هایی از سری کلاتز برای اعداد ۱۱، ۱۳، ۳۲۰ و ۶۴۰

از سایت زیر می‌توانید استفاده کنید تا برای هر عدد سری کلاتز آن را حساب کند.

https://www.dcode.fr/collatz-conjecture

همچنین می‌توانید پارامترهای تقسیم و ضرب و جمع برای اعداد زوج و فرد را تغییر دهید و نتیجه را بررسی کنید که آیا سری‌های حاصل مانند حدس کلاتز همگرایی دارند یا خیر.

در طی این سال‌ها تلاش‌های زیادی برای اثبات حدس کلاتز شده است که به ثمر نرسیده است اما یکی از جالب‌ترین تلاش‌های اخیر، تلاش برای حل معمای حدس کلاتز با استفاده از روش SAT بوده که هنوز در حال انجام است ولی امید بسیاری هست تا به نتیجه برسد.

واژه SAT از satisfiability می‌آید و دلیل اینکه چرا با اینکه مخفف و سرواژه نیست با حروف بزرگ نوشته می‌شود را بعدتر توضیح خواهیم داد. اما مفهوم satisfiability یا صدق‌پذیری یا Boolean satisfiability problem یا مساله صدق‌پذیر دودویی یا بولی چیست؟

به زبان ساده SAT از جنس مسایل تصمیم‌گیری در علوم کامپیوتری است. مساله تصمیم‌گیری به این معناست که پاسخ سوال و مساله، بله یا خیر باشد. مسایل تصمیم‌گیری اغلب با مجموعه‌ای از ورودی‌ها مشخص می‌شود که به ازای آن‌ها پاسخ مساله، بله است. رسم است که مجموعه جواب را با حروف بزرگ نام‌گذاری می‌کنند. سنتی که از زمان کتاب مهم و تاثیرگذار مایکل گری و دیوید جانسون به نام Computers and Intractability: A Guide to the Theory of NP-Completeness باقی مانده است.

فرض کنید مساله ما این باشد که آیا اعداد طبیعی وجود دارند که بجز خود و ۱ بر اعداد طبیعی دیگری بخش‌پذیر نباشند؟ جواب بله است و مجموعه پاسخ مساله که مجموعه اعداد اول است بصورت PRIMES نوشته می‌شود.

فرض کنید مسئول برگزاری انتخاباتی شده‌اید. فرض کنید n نامزد انتخابی داریم و رای دهندگان می‌توانند از ۰ (هیچکس) تا n (همه) را انتخاب کنند. هر رای دهنده فهرستی را تحویل می‌دهد که شامل نامزدهایی‌ست که دوست دارد انتخاب شوند و نامزدهایی که دوست ندارد انتخاب شود. مثلا فهرست رای‌دهنده می‌توانند «الف، ب، نه ج» باشد یعنی رای دهنده دوست دارد الف و ب رای بیاورند ولی ج رای نیاورد. می‌گوییم رای‌دهنده خوشحال و راضی خواهد بود اگر یکی از خواسته‌هایش برآورده شود. مثلا اگر الف یا ب انتخاب شود راضی خواهد شد و اگر ج رای نیاورد هم راضی خواهد شد. در این مثال اگر مثلا هیچکس رای نیاورد هم رای‌دهنده راضی خواهد شد چون شرط رای نیاوردن ج برآورده شده است. اگر رای دهنده‌ای مثلا رای خالی یا سفید بدهد یعنی هر کس رای بیاورد او راضی نخواهد بود. در واقع بین بخش‌های رای، رابطه «یا منطقی» برقرار است که با علامت «V» نشان داده می‌شود.

رای‌ها را تحویل شما که برگزارکننده انتخابات هستید داده‌اند. حالا مساله‌ای که باید حل کنید این است که آیا امکان راضی کردن همه رای‌دهندگان وجود دارد؟ اگر بله، چه مجموعه‌ای از نامزدها رای بیاورند همه رای‌دهندگان راضی خواهند شد؟ فرض کنید ۳ نامزد داریم A، ‌B و C. تعداد رای‌دهندگان ۴ نفر است.
هر رای را در خطی جدا می‌نویسیم و علامت نقیض یعنی رای نیاوردن نامزد خاص. مثلا رای‌ها به این صورت هستند

A B ~C

B C

~B

~A C

۳ نامزد داریم و از بین ۸ حالت ممکن تنها یک حالت است که همه را راضی خواهد کرد

جواب این است: نامزدهای A و C انتخاب شوند و B انتخاب نشود.

حالا مساله را تعمیم بدهیم. در عوض نامزدها به آن‌ها می‌گوییم متغیرها. هر متغیر می‌تواند مقدار صحیح یا نادرست داشته باشد. مساله یافتن مقداری از متغیرهاست که بتواند همه شرط‌ها را تامین کند. برای مثال بالا مقدار

A=true , B = false و C = true

باعث می‌شود همه گزاره‌های مساله راضی و برآورده شوند. راضی یعنی حداقل یک بخش از آن صحیح شود.

حالا تعریف SAT به زبان ساده یعنی، اگر گزاره‌های یک مساله را به ما بدهند، آیا مجموعه مقداری برای متغیرها وجود دارد که باعث شود همه گزاره‌ها راضی شوند یا صادق باشند؟

اثبات مسایل ریاضی با استفاده از کامپیوتر

مسایلی از جنس SAT مسایل دشوار و بزرگ اما با محاسبه محدود هستند. یعنی ممکن است توان پردازش بسیار زیادی نیاز داشته باشند اما بالاخره محدود هستند و بی‌نهایت نیستند. برای اینکه تصوری از بزرگی پردازش داشته باشید باید بدانید متن اثبات کامپیوتری مساله معروف افراز ۳تایی‌های فیثاغورثی به روش SAT برابر ۲۰۰ ترابایت است.

مساله ۳تایی‌های فیثاغورثی چیست؟

با رابطه فیثاغورثی در مثلث قائم‌الزاویه آشنا هستیم. مجموع مربع ۲ ضلع برابر با مربع وتر است. اعداد صحیحی هم وجود دارند که رابطه فیثاغورثی a^2 + b^2 = c^2 بین آنها برقرار است مانند ۳ و ۴و ۵

یعنی ۳ به توان ۲ بعلاوه ۴ به توان ۲ برابر است با ۵ به توان ۲

یا ۵، ۱۲ و ۱۳

صورت مساله تقسیم یا افراز ۳تایی‌های فیثاغورثی مساله‌ای است که در دهه ۸۰ قرن بیستم توسط ریاضیدانی به نام رونالد گراهام مطرح شد و وی جایزه‌ای صد دلاری برای حل آن تعیین کرد.

آیا می‌توان مجموعه اعداد طبیعی را طوری به ۲ دسته تقسیم یا افراز کرد که هیچ دسته‌ای شامل ۳‌تایی‌های فیثاغورثی نباشد؟ یعنی در هیچ دسته نتوان ۳ عدد پیدا کرد که رابطه فیثاغورث a^2 + b^2 = c^2 بین آنها برقرار باشد.

این مساله به رنگ کردن هم معروف است. فرض کنید که اعداد طبیعی را به ۲ دسته تقسیم کنیم و به اعداد دسته اول رنگ آبی و دسته دوم رنگ سرخ بدهیم. آیا همه ۳تایی‌های فیثاغورثی حتما ۲ رنگ آبی و سرخ را خواهند داشت؟ آیا می‌توان طوری تقسیم کرد که ۳تایی‌های فیثاغورثی هرگز هم‌رنگ نباشند؟

بیایید تلاش کنیم این کار را انجام دهیم. اولین ۳تایی‌های فیثاغورثی ۳ و ۴و ۵ هستند. ۳ را در دسته اول قرار می‌دهیم و ۴ و ۵ را در دسته دوم.

دسته اول ۳

دسته دوم ۴ و ۵

یکی از ۳تایی‌های فیثاغورثی ۵ و ۱۲ و ۱۳ است. نمی‌توانیم ۱۲ و ۱۳ را در همان دسته‌ای قرار دهیم که ۴ و ۵ هستند چون ۱۲ و ۱۳ و ۵ سه‌تایی فیثاغورثی هستند.

پس باید یا هر دو را در دسته اول یعنی کنار ۳ بگذاریم یا حداقل یکی از آن‌ها را در دسته اول بگذاریم

دسته اول ۳ و ۱۲

دسته دوم ۴ و ۵ و ۱۳

۳تایی فیثاغورثی بعدی ۱۲، ۳۵ و ۳۷ است. ۳۵ و ۳۷ را نمی‌توانیم کنار ۱۲ یعنی در دسته اول قرار دهیم. پس مثلا باید ۳۵ را در یک دسته و ۳۷ را در دسته دیگر بگذاریم

دسته اول ۳ و ۱۲ و ۳۵

دسته دوم ۴ و ۵ و ۱۳و ۳۷

۳تایی فیثاغورثی بعدی ۱۳ و ۸۴ و ۸۵ است. ۸۴ و ۸۵ را نمی‌توانیم کنار ۱۳ یعنی دسته دوم قرار دهیم و ...

هر چه بیشتر جلو می‌رویم کار سخت‌تر می‌شود.

تا قبل از اثبات اخیر برای مجموعه اعداد ۱ تا ۷۶۶۴ توانسته بودیم دسته‌بندی یا افراز مناسب را پیدا کنیم. یعنی اعداد ۱ تا ۷۶۶۴ بدون اینکه ۳تایی فیثاغورثی هم‌رنگ داشته باشند قابل افراز و دسته‌بندی هستند.

ابرکامپیوتر دانشگاه تگزارش با ۲۷۰ ترابایت رم و ۱۴ پتابایت هارد و ۵۲۲۰۸۰ هسته محاسباتی
ابرکامپیوتر دانشگاه تگزارش با ۲۷۰ ترابایت رم و ۱۴ پتابایت هارد و ۵۲۲۰۸۰ هسته محاسباتی


با کمک ابرکامپیوتر ۶۰ میلیون دلاری دانشگاه تگزاس که ۲۷۰ ترابایت رم و ۱۴ پتابایت هارد و ۵۲۲۰۸۰ هسته محاسباتی داشت اثبات شد که برای عدد ۷۸۲۴ هم می‌توان افراز کرد اما برای ۷۸۲۵ امکان چنین دسته‌بندی وجود ندارد. گفتیم که جواب SAT معمولا بله یا خیر است که جواب در این مساله خیر بود اما اثبات آن ۲۰۰ ترابایت فضا نیاز دارد. یعنی اثبات اینکه در همه حالت‌های افراز و دسته‌بندی ممکن،‌ باز هم حداقل یک ۳تایی فیثاغورثی قرار خواهد گرفت.

طراحی حل‌کنندهSAT برای حدس کلاتز

بسیاری از مسایل ریاضی از جنس SAT یا تصمیم‌گیری نیستند. مثلا مساله کلاتز به نظر نمی‌رسد ربطی به SAT داشته باشد. اما نکته‌ای که وجود دارد این است که می‌توان بعضی از مسایل را به مساله دیگری تبدیل کرد.
در سال ۲۰۱۸ دو دانشمند علوم کامپیوتر به نام‌های Heule و Aaronson توانستند از بنیاد ملی علوم آمریکا بودجه لازم را برای اعمال و یافتن حل کننده SAT برای حدس کلاتز را دریافت کنند. موفقیت‌های قبلی Heule در اثبات ۲۰۰ ترابایتی افراز ۳تایی‌های فیثاغورثی در ۲۰۱۶ و عدد Schur ۵ در سال ۲۰۱۷ و حدس کلر در بعد هفت با کمک SAT این بار او را به سراغ حدس کلاتز کشانده است و او سعی دارد با چکش SAT حدس بدقلق و دردسرساز کلاتز را بشکند.

ابتدا باید حدس کلاتز به مساله هم‌ارز دیگری تبدیل می‌شد.

آرنسون صورت‌بندی دیگری از حدس کلاتز بر مبنای سیستم بازنویسی یا rewriting system ارایه کرد که برای استفاده در کامپیوتر بسیار مناسب‌تر از شکل اصلی حدس کلاتز است. بازنویسی یا rewriting به زبان ساده یعنی شما مجموعه‌ای از علایم دارید مثلا حروف A, B, C که از آن‌ها برای ساخت رشته‌های مانند ACACBACB استفاده می‌کنید. قواعدی هم برای تبدیل این رشته‌ها دارید. مثلا یک قاعده دارید که هر جا AC دید آن را به BC تبدیل و تعویض کند. یا مثلا قاعده دومی دارید که هر جا BC دید آن را به AAA تبدیل و تعویض کند. تعداد قواعد در اختیار ماست و هر تعدادی می‌تواند باشد. سوالی که در بازنویسی یا rewriting مطرح‌ است این است که آیا یک نظام یا سیستم بازنویسی همیشه به پایان می‌رسد؟ منظور از پایان این است که آیا رشته ابتدایی بعد از اعمال قوانین تعریف شده به حالت و رشته‌ای تبدیل می‌شود که دیگر هیچ قاعده‌ای برای تبدیل و تغییر آن نداشته باشیم؟

مثال بالا یعنی ACACBACB را در نظر بگیرید. قواعد ما ۱) تبدیل AC‌ به BC و ۲) تبدیل BC به AAA است.

پس رشته ACACBACB با استفاده از قاعده اول تبدیل می‌شود به BCBCBBCB

رشته BCBCBBCB با قاعده دوم تبدیل می‌شود به AAAAAABAAAB

رشته AAAAAABAAAB دیگر قابل تبدیل نیست و ما هیچ قاعده‌ای برای تبدیل آن نداریم پس رشته اولیه به پایان می‌رسد و تبدیل بیشتری ممکن نیست.

آرنسون حدس کلاتز را به ۷ علامت و ۱۱ قاعده مشابه‌سازی کرد. حالا اگر هیول بتواند ثابت کند که این سیستم همیشه به پایان می‌رسد و تمام می‌شود، حدس کلاتز اثبات خواهد شد.

برای تبدیل حدس کلاتز به مساله SAT یک قدم دیگر هم باید برداشته شود. برای اثبات پایان پذیر بودن سیستم بازنویسی، از ماتریس‌ها استفاده می‌شود . آرانسون و هیول باید به هر علامت و نشانه یک ماتریس نسبت بدهند و قواعد تبدیل علایم به ضرب ماتریس‌ها بدل می‌شوند. این هفت ماتریس نماینده ۷ نشانه و علامت سیستم بازنویسی هستند و باید شرایط خاصی را برآورده کنند که نشان دهنده سازگاری ۱۱ قاعده با یکدیگر باشد.

اگر این ۷ ماتریس پیدا شوند، اثبات می‌شود نظام بازنویسی پایان‌پذیر است و اثبات پایان‌پذیری یعنی اثبات حدس کلاتز.

حالا مساله «آیا ماتریسی وجود دارد که این شرایط را برآورده کند؟» یک مساله SAT است.

جستجو از ماتریس‌های ۲ در ۲ آغاز شد و سپس ۳ در ۳ و بعد از پیدا نشدن ابعاد ماتریس‌ها افزایش پیدا کرد. حدس هیول این است که اگر در ماتریس‌های ۱۲ در ۱۲ به جواب نرسد، مرتبه‌های بالاتر از توان پردازشی موجود بالاتر می‌رود و مساله ناتمام می‌ماند. حالا مساله هیول و آرانسون یافتن راه‌حل‌های جستجوی بهینه است که اگر نیاز به ابعاد بزرگتر بود با همین توان پردازشی موجود بتوان آن را یافت.

جستجو هنوز ادامه دارد.

منابع

https://www.quantamagazine.org/can-computers-solve-the-collatz-conjecture-20200826/

https://sahandsaba.com/understanding-sat-by-implementing-a-simple-sat-solver-in-python.html

کولاتزSATsatisfiabilityCollatzREWRITE SYSTEMS
داد جاروبی به دستم آن نگار / گفت کز دریا برانگیزان غبار
شاید از این پست‌ها خوشتان بیاید