Payamvdn/NorthPersian_fa_wiki huggingface dataset:
ب آنها ابتلا به اسکوربوت بود. جان وودال، جراح نظامی انگلیسی از کمپانی بریتانیایی هند شرقی، مصرف مرکبات (اثر ضد اسکوربوتیک) را از قرن هفدهم توصیه کرده بود، اما استفاده از آنها فراگیر نشد. لیند اولین کارآزمایی بالینی سیستماتیک را در سال ۱۷۴۷ انجام داد. او یک مکمل غذایی اسیدی را پس از دو ماه حضور در دریا، زمانی که افراد کشتی به بیماری اسکوربوت مبتلا شده بودند، در آزمون خود گنجاند. او دوازده ملوان اسکوربوتیک را به شش گروه دو نفره تقسیم کرد. همه آنها رژیم غذایی مشابهی دریافت کردند، اما علاوه بر این، به گروه یک روزانه یک لیتر شراب سیب، به گروه دو بیست و پنج قطره اکسیر ویتریول (اسید سولفوریک)، به گروه سه شش قاشق سرکه، به گروه چهار نصف پیمانه آب دریا داده شد. گروه پنج دو عدد پرتقال و یک لیمو (ابهام زدایی) و گروه آخر یک رب تند (spicy paste) به اضافه یک دریافت کردند. درمان گروه پنج پس از ۶ روز که میوه آنها تمام شد متوقف شد که در آن زمان، یکی از ملوانان آماده انجام وظیفه شده بود و دیگری نیز تقریباً بهبود یافته بود. علاوه بر گروه پنج، گروه یک نیز اثراتی از درمان را نشان داد. پس از سال ۱۷۵۰، کارآزمایی های بالینی شکل مدرن
به خود گرفت. دکتر جان هیگارث انگلیسی اهمیت گروه کنترل را برای شناسایی صحیح اثر دارونما در مطالعه مشهور خود در مورد یک ابزار درمانی بی اثر به نام تراکتورهای پرکینز نشان داد. کار بیشتر در این راستا توسط پزشک برجسته آقای ویلیام گال در دهه ۱۸۶۰ انجام شد. فردریک اکبر محمد (متوفی ۱۸۸۴)، که در بیمارستان گایز در لندن کار می کرد، مشارکت قابل توجهی در فرایند کارآزمایی های بالینی داشت، بدین ترتیب که «او نفریت مزمن همراه با پرفشارخونی ثانویه را از آنچه اکنون پرفشارخونی اولیه (اساسی) می نامیم مجزا کرد. او همچنین سابقه تحقیقات جمعی را برای انجمن پزشکی بریتانیا راه اندازی کرد؛ این سازمان داده هایی را از پزشکانی که خارج از محیط بیمارستان طبابت می کردند جمع آوری کرد و پیشگام کارآزمایی های بالینی مشترک مدرن بود.» کارآزمایی های مدرن رونالد فیشر در حالی که برای کار می کرد، "اصول طراحی تجربی (Principles of experimental design)" را در دهه ۱۹۲۰ به عنوان روشی دقیق برای طراحی مناسب آزمایش ها توسعه داد. از جمله ایده های اصلی او، اهمیت تصادفی سازی - تخصیص تصادفی افراد به گروه های مختلف جهت انجام آزمایش؛ تکرار - برای کاهش عدم قطعیت، اند
ازه گیری ها باید تکرار شوند و آزمایش ها چند بار انجام شوند تا منابع اختلاف و واریاسیون شناسایی شوند؛ بلوک بندی- تنظیم واحدهای آزمایش در گروه هایی (بلوک ها) که مشابه یکدیگرند، و در نتیجه کاهش منابع اختلاف و واریاسیون نامرتبط؛ استفاده از آزمایش های عاملی - در ارزیابی اثرات و برهم کنش احتمالی چندین عامل مستقل مؤثر است. شورای تحقیقات پزشکی بریتانیا اهمیت کارآزمایی های بالینی را از دهه ۱۹۳۰ به رسمیت شناخت. این شورا "کمیته کارآزمایی های درمانی" را برای مشاوره و کمک به تنظیم کارآزمایی های بالینی کنترل شده بر روی محصولات جدیدی که به نظر می رسد بر اساس دلایل تجربی در درمان بیماری ارزش دارند، ایجاد کرد. اولین کارآزمایی درمانی تصادفی شده در واحد تحقیقات سل MRC توسط سر جفری مارشال (۱۹۸۲–۱۸۸۷) انجام شد. این کارآزمایی که بین سال های ۱۹۴۶ و ۱۹۴۷ انجام شد، با هدف آزمایش اثربخشی ماده شیمیایی استرپتومایسین در درمان سل ریوی انجام شد. کارآزمایی دوسوکور و کنترل شده با دارونما کنترل شده بود. روش کارآزمایی های بالینی بعداً توسط آستین برادفورد هیل، که در کارآزمایی های استرپتومایسین شرکت داشت، بیشتر توسعه یافت. از دهه ۱۹۲۰، هیل آمار
را در پزشکی اعمال کرد و در سخنرانی های ریاضیدان های مشهور از جمله کارل پیرسون شرکت کرد. او به دنبال انجام یک مطالعه مهم با همکاری ریچارد دال در خصوص ارتباط بین سیگار کشیدن و سرطان ریه، به شهرت رسید. آنها یک مطالعه مورد-شاهدی را در سال ۱۹۵۰ انجام دادند که بیماران مبتلا به سرطان ریه را با یک گروه کنترل همسان مقایسه کردند که آغاز یک مطالعه هم گروهی (کهورت) آینده نگر طولانی مدت با موضوع گسترده تر ارتباط بین سیگار کشیدن و سلامت بود که عادت سیگار کشیدن و سلامت بیش از ۳۰٬۰۰۰ پزشک را در یک دوره چند ساله بررسی می کرد. گواهی وی برای انتخاب در انجمن سلطنتی او را چنین توصیف کرده است: «... راهبر در توسعه روش های آزمایشی دقیق در پزشکی که اکنون در سطح ملی و بین المللی در ارزیابی ترکیبات جدید درمانی و پیشگیرانه استفاده می شود.» روز جهانی کارآزمایی های بالینی هر سال در بیستم ماه مه جشن گرفته می شود تا یادبود روزی باشد که جیمز لیند اولین کارآزمایی بالینی تصادفی شده را در سال ۱۷۴۷ آغاز کرد. در اغلب موارد ساختگی است و موضوع نقد قرار گرفته است. انواع. کارآزمایی های بالینی بر اساس هدف پژوهشی پژوهشگران طبقه بندی می شوند. کارآزمایی
بر اساس هدفشان طبقه بندی می شوند. پس از اعطای تاییدیه برای انجام پژوهش های انسانی به حامی کارآزمایی، سازمان غذا و داروی ایالات متحده (FDA) نتایج کارآزمایی را بر اساس انواع زیر سازماندهی و نظارت می کند: کارآزمایی های بالینی معمولاً در چهار مرحله انجام می شوند که در هر مرحله از تعداد موضوعات و افراد مختلف استفاده می شود و هدف های متفاوتی برای ایجاد تمرکز بر شناسایی یک اثر را خاص دارد. مراحل. کارآزمایی بالینی که شامل داروهای جدید می باشد، معمولاً به پنج مرحله طبقه بندی می شوند. هر مرحله از فرایند تایید دارو یک کارآزمایی بالینی جداگانه در نظر گرفته می شود. فرایند توسعه دارو معمولاً طی سال های متمادی از طریق فازهای یک تا چهار ادامه می یابد که اغلب یک دهه یا بیشتر را در بر می گیرد. اگر دارو مراحل یک، دو و سه را با موفقیت پشت سر بگذارد، معمولاً توسط مرجع نظارتی ملی برای استفاده در جمعیت عمومی تأیید می شود. کارآزمایی فاز چهار پس از عرضه دارو، آزمون تشخیصی و یا دستگاه جدید تأیید شده انجام می شود و ارزیابی خطرها، مزایا و یا بهترین کاربردها را ارایه می دهد. طراحی کارآزمایی. کارآزمایی بالینی تصادفی سازی شده. کارآزمایی با
لینی تصادفی سازی شده (Randomized Clinical Trial): مطالعه ای که در آن شرکت کنندگان به طور تصادفی در گروه های مجزایی قرار می گیرند تا محققان درمان های مختلف را با هم مقایسه نمایند. محققان و شرکت کنندگان به دلخواه نمی توانند گروه ها را انتخاب کنند. به طور تصادفی قرار دادن شرکت کنندگان در گروه های مختلف به این معنی می باشد که گروه ها شبیه هم خواهند بود و اینکه درمان هایی را که در مورد شرکت کنندگان صورت می گیرد می توان به طور بی طرفانه مقایسه نمود. در هنگام انجام کارآزمایی بالینی، مشخص نیست کدام درمان از همه بهتر می باشد. کارآزمایی بالینی تصادفی سازی نشده. کارآزمایی بالینی تصادفی سازی نشده (Nonrandomized Clinical Trial): آزمایشی بالینی که در آن شرکت کنندگان به طور تصادفی در گروه های مختلف درمان قرار نمی گیرند. ممکن است خود شرکت کنندگان تصمیم بگیرند در کدام گروه شرکت کنند یا امکان دارد محقق آن ها را در گروه های مختلف قرار دهد. کارآزمایی بالینی شاهددار. آزمایش بالینی شاهددار (Controlled Clinical Trial) :آزمایشی بالینی که شامل گروه مقایسه (شاهد) است. افراد این گروه از درمانی دیگر برخوردار می شوند، یا آن ها را درمان ن
می کنند و به آن ها دارو نما (پلاسبو) داده می شود. ملاحظات اخلاقی. یک کمیته مستقل از پزشکان، متخصصان آمار بر روند تصویب کارآزمایی های بالینی نظارت می کنند. این کمیته باید اطمینان حاصل کند که خطرات کارآزمایی بالینی موردنظر اندک است و منافع بالقوه آن ارزشمند است. در ایران همهٔ کارآزمایی های بالینی در "پایگاه ثبت کار آزمایی های بالینی" ثبت می شوند. مفاهیم. دارونما یک قرص، مایع، یا پودر بی اثر است که هیچ ارزش درمانی ندارد. در کارآزمایی های بالینی، درمان های تجربی اغلب با دارونماها مورد مقایسه قرار می گیرند تا اثربخشی درمان تجربی مورد ارزیابی قرار گیرد. در برخی از کارآزمایی ها افرادی که در گروه کنترل (شاهد) قرار دارند، به جای دارو یا درمان تجربی فعال، دارونما دریافت می کنند. کنترل (یا شاهد)، استانداردی است که به وسیلهٔ آن مشاهدات تجربی مورد ارزیابی قرار می گیرند. در بسیاری از کارآزمایی های بالینی، گروهی از بیماران دارو یا درمان تجربی را دریافت می کنند (case group)، در حالی که افراد گروه کنترل (control group)، دارو یا درمان استاندارد رایج برای آن بیماری را دریافت نمی کنند یا اینکه از دارونما استفاده می کنند. منابع.
یانوش دوم یا یانوش ژیگموند ساپویائی ( زادهٔ ۱۸ ژوئیه ۱۵۴۰– مرگ ۱۴ مارس ۱۵۷۱) پادشاه مجارستان و اولین پرنس ترانسیلوانی بود. او پسر یانوش یکم بود که در خردسالی بعد از درگذشت پدر به پادشاهی رسید؛ ولی ابتدا ادارهٔ امور بر عهدهٔ مادرش بود. او مورد حمایت سلطان سلیمان عثمانی قرار گرفت. حکمرانی. ساپویائی در دهه ۱۵۶۰ ضد هابسبورک که متعلق به کلیسای کاتولیک بود، مجموعه ای از مباحث الهیاتی همسو با اصلاحات را آغاز کرد و خود از کاتولیک به لوتریانیسم و بعد به کالوینیسم گروید. او با تصویب فرمانی مبنی بر نکته «ایمان هدیه خداوند»، محدودیت های مذهبی را فراتر از استانداردهای اروپایی در اواخر قرن شانزدهم لغو کرد. ساپویائی سرانجام به عنوان پادشاه منتخب مجارستان در کنار گذاشته شد و در جایگاه پرنس ترانسیلوانی و فرمانروای بخش هایی از پادشاهی مجارستان حکومت کرد. پس از درگذشت او بدون وارث ایشتوان باتوری معتقد به کلیسای کاتولیک جانشین او شد.
صدق پذیری یا ارضاپذیری در دانش رایانه پرسمانی است که می پرسد آیا می توان ارزش متغیرهای فرمولی دودویی را به گونه ای یافت که فرمول درست باشد؟ بنابراین اگر چنین ارزش دهی پیدا شود، گوییم پرسمان "صدق پذیر" است. وگرنه، بی گمان این فرمول همواره نادرست است و گوییم که فرمول "صدق ناپذیر" است. برای نمونه، فرمول formula_1 صدق پذیر است چون اگر ارزش های formula_2 و formula_3 درست باشند، فرمول همواره درست است. پرسمان صدق پذیری نخستین پرسمانی است که ان پی کامل بودنش نشان داده شده است. کوک و لوین نشان دادند الگوریتمی شناخته شده ای نیست که در زمانی کوتاه پرسمان صدق پذیری را حل کند. محدودهٔ وسیعی از بقیهٔ مسائل تصمیم گیری و بهینه سازی طبیعی می توانند به موارد مسئلهٔ صدق پذیری تبدیل شوند. یک رده از الگوریتم ها به نام حل کننده های SAT به طور کارآمد می توانند زیرمجموعه ای به اندازهٔ کافی بزرگ از موارد SAT را حل کنند تا در حوزه های مختلف عملی از جمله طراحی مدار و قضیهٔ اثبات اتوماتیک مفید باشند. وسیعتر کردن قابلیت های الگوریتم های حل کنندهٔ SAT یک حوزهٔ در حال پیشرفت است. هرچند هیچ کدام از روش های کنونی نمی توانند "همه ی" موارد مسئ
لهٔ صدق پذیری را به طور کارآمد حل کنند. تعریف ها، واژگان و کاربردها. در نظریه پیچیدگی محاسباتی مسئلهٔ صدق پذیری یک مسئلهٔ تصمیم است که نمونهٔ آن یک عبارت بولی می باشد که فقط با AND، OR، NOT، متغیرها و پرانتز نوشته شده است. سؤال این است که: آیا می توان به متغیرها مقادیر "درست" و "نادرست" داد تا عبارت موردنظر همواره درست باشد؟ یک فرمول از منطق گزاره ای صدق پذیر است اگر به متغیرهای آن بتوان مقادیر منطقی داد تا فرمول همواره درست باشد. مسئلهٔ صدق پذیری دودویی یک ان پی کامل است. مسئلهٔ صدق پذیری گزاره ای (PSAT)، که مشخص می کند آیا یک فرمول گزاره ای صدق پذیر هست یا نه، مهم ترین مسئله در حوزه های مختلف علوم رایانه است؛ نظیر علوم نظری رایانه، الگوریتم ها، هوش مصنوعی، طراحی پردازنده، اتوماسیون طراحی الکترونیکی و تایید. یک متغیر یا خود آن متغیر یا نقیضش است. به طور مثال x۱ یک متغیر مثبت و (not(x۲ یک متغیر منفی است. یک عبارت فصل منطقی از متغیرهاست. به طور مثال (x۱ V not(x۲ یک عبارت است. در بعضی حالت های مسئله صدق پذیری دودویی، نیاز است که فرمول عطف منطقی چند عبارت باشد. حالتی که صدق پذیری یک فرمول به شکل عطف معمولی را بر
رسی می کنیم که هر عبارت حداکثر دارای سه متغیر باشد، ان پی کامل است؛ این مسئله "۳SAT" یا "۳CNFSAT" یا "۳-صدق پذیری" نامیده می شود. حالتی که فرمول موردبررسی دارای عبارت هایی با حداکثر دو متغیر باشد، ان ال کامل است؛ این مسئله "۲SAT" نامیده می شود. حالتی که فرمول موردبررسی دارای عبارت های هورن (که حداکثر یک متغیر مثبت دارند.) باشد، پی کامل است؛ این مسئله صدق پذیری هورن نامیده می شود. قضیه کوک لوین عنوان می کند که مسئله دودویی صدق پذیری یک ان پی کامل است، در واقع این اولین مسئله ایست که اثبات شده ان پی کامل است. پیچیدگی و نسخه های محدود. ان پی کامل. همانطور که استفن کوک در سال ۱۹۷۱ اثبات کرد، مسئلهٔ SAT اولین مسئلهٔ ان پی کامل شناخته شد. (اثبات را در قضیه کوک لوین ببینید.) تا آن زمان مفهومی به نام ان پی کامل وجود نداشت. این مسئله ان پی کامل باقی می ماند هرچند که همهٔ عبارات به صورت عطفی معمولی با سه متغیر در هر عبارت (۳-CNF) باشند؛ یعنی عبارت به شکل زیر است: در اینجا هر x یک "متغیر" است و هر متغیر می تواند چندبار در عبارت تکرار شوند. یک ویژگی مهم اختصار کوک آن است که تعداد جواب های درست را نگه می دارد. به طور مثال
اگر یک گراف 17 رنگ آمیزی سه گانه معتبر داشته باشد، قاعدهٔ SAT دارای 17 واگذاری ارضاپذیر است. ان پی کامل فقط به زمان اجرا در بدترین حالت ارجاع می دهد. بسیاری از مواردی که در کاربردهای عملی اتفاق می افتند می توانند خیلی سریعتر حل شوند. مسئلهٔ SAT آسان تر است اگر فرمول ها به صورت فصلی معمولی باشند، یعنی بین عبارات OR و در هر عبارت بین متغیرها AND قرار گرفته باشد. این فرمول ها صدق پذیر هستند اگر و تنها اگر حداقل یکی از عبارات آن صدق پذیر باشند، و یک عبارت صدق پذیر است اگر و تنها اگر به ازای هر متغیر x هم خودش و هم NOT آن را دربرنداشته باشد. این موضوع می تواند در زمان چندجمله ای بررسی شود. 2-صدق پذیری. همچنین مسئلهٔ SAT آسان تر است اگر تعداد متغیرهای یک عبارت به 2 محدود شده باشد، که در این حالت مسئله 2SAT نامیده می شود. این مسئله نیز می تواند در زمان چندجمله ای حل شود و در واقع برای ردهٔ ان ال کامل است. به طور مشابه اگر تعداد متغیرهای هر عبارت را به 2 محدود کرده و اعمال AND را به XOR تغییر دهیم، نتیجه یک "2-صدق پذیری XOR" است که یک مسئلهٔ کامل برای SL = L می باشد. یکی از مهم ترین محدودیت های SAT، مسئلهٔ HORNSAT م
ی باشد که فرمول، یک عطف از چند عبارت هورن باشد. این مسئله با الگوریتم ارضاپذیری هورن با زمان چندجمله ای قابل حل است، و در اصل پی-کامل می باشد. می تواند به صورت نسخه ای از ردهٔ پی برای مسئلهٔ صدق پذیری دودویی دیده شود. در صورتی که رده های پیچیدگی پی و ان پی یکسان نباشند، برخلاف SAT هیچ کدام از این محدودیت ها ان پی کامل نیستند. این فرضیه که پی و ان پی یکسان نیستند هنوز اثبات نشده است. 3-صدق پذیری. 3-صدق پذیری یک حالت خاص از k-SAT یا به طور ساده شده SAT است که هر عبارت دقیقاً k = 3 متغیر را شامل می شود. این یکی از 21 مسئله ان پی-کامل کارپ است. در اینجا یک مثال می زنیم: (¬ نشان دهندهٔ نقیض است.) E دارای دو عبارت (که با پرانتز مشخص شده اند)، چهار متغیر ("x"1, "x"2, "x"3, "x"4) و k = 3 (سه متغیر در هر عبارت) می باشد. برای آنکه این مثال از مسئلهٔ تصمیم گیری را حل کنیم باید مشخص کنیم که آیا یک جدول درستی برای متغیرها وجود دارد به طوری که کل عبارت همواره درست باشد یا خیر. در این مثال با "درست" قرار دادن همه متغیرها، می توان E را همواره درست در نظر گرفت. واگذاری های متنوعی می توان انجام داد. اگر هیج واگذاری ای امکان پذ
یر نبود، جواب "خیر" خواهد بود. 3-SAT ان پی کامل است و به عنوان یک نقطهٔ شروع برای اثبات آنکه بقیهٔ مسائل هم ان پی سخت هستند استفاده می شود. این عمل با محدودیت زمانی چندجمله ای قابل انجام است. 3-SAT می تواند به یک-در-سه 3-صدق پذیری محدود شود که در آن ما "دقیقاً" می پرسیم که آیا یکی از متغیرها در هر عبارت درست هست یا خیر، به جای اینکه "حداقل" یک متغیر را بررسی کنیم. این محدودیت نیز ان پی کامل باقی می ماند. بر اساس نظر شونینگ (1990) یک الگوریتم سادهٔ تصادفی وجود دارد که در زمان formula_5 اجرا می شود (n تعداد عبارات). این الگوریتم به احتمال قوی موفق می شود تا دربارهٔ 3-SAT درست تصمیم بگیرد. فرضیهٔ نمایی زمان آن است که هیچ الگوریتمی نمی تواند 3-SAT را در زمان formula_6 حل کند. صدق پذیری هورن. یک عبارت هورن است اگر حداکثر یک متغیر مثبت داشته باشد. این گونه عبارت ها مورد توجه هستند چون می توانند استلزام یک متغیر از مجموعه ای از متغیرها را بیان کنند. در واقع یک عبارت مانند formula_7 می تواند به شکل formula_8 بازنویسی شود، یعنی اگر formula_9 همه "درست" باشند، y هم باید "درست" باشد. مسئلهٔ تصمیم گیری در مورد صدق پذیری
عبارات هورن در پی (P) است. این مسئله نیز می تواند با یک مرحله از انتشار واحد حل شود که مدل کمینهٔ واحد از مجموعه ای از عبارات هورن ایجاد می کند. یک تعمیم از ردهٔ فرمول های هورن، فرمول با قابلیت اسم گذاری دوبارهٔ هورن است که یک مجموعه از فرمول ها می باشد که با فرمت هورن می تواند با چند متغیر به همراه نقیض مربوطهٔ آن ها جایگزین شود. بررسی وجود این جایگزینی می تواند در زمان خطی انجام بگیرد؛ پس صدق پذیری همچین فرمولی در پی (P) است، چون می تواند اول با این جایگزینی و سپس بررسی صدق پذیری فرمول هورن نتیجه شده حل شود. صدق پذیری XOR. یک حالت خاص دیگر مسائلی هستند که در آن ها هر عبارت فقط اعمال XOR را شامل می شود. چون عمل XOR معادل جمع در زمینهٔ گالویس از اندازهٔ 2 است، عبارات می توانند مانند یک دستگاه معادلات خطی دیده شوند و از روش های متناظر مانند حذف گاوسی می توان برای یافتن راه حل آن ها استفاده کرد. قضیهٔ دوگانگی شافر. محدودیت های بالا (CNF، 2CNF، 3CNF، هورن) فرمول موردبررسی را به عطفی بودن زیرفرمول محدود می کنند؛ هر محدودیت یک شکل خاص برای همهٔ زیرفرمول ها مشخص می کند: به طور مثال، فقط عبارات دودویی می توانند یک ز
یرفرمول در 2CNF باشند. قضیهٔ دوگانگی شافر عنوان می کند که برای هر محدودیتی بر اعمال بولی که می توانند این زیرفرمول ها را شکل دهند، مسئلهٔ صدق پذیری متناظر یک پی یا ان پی کامل است. عضویت در پی (P) برای صدق پذیری 2CNF و فرمول هورن، حالت های خاصی از این قضیه هستند. رفتار در زمان اجرا. همانطور که در بالا به طور خلاصه بیان شد، هرچند که مسئله، ان پی کامل است، مثال های عملی زیادی می توانند خیلی زود حل شوند. اکثر مسائل عملی در حقیقت "آسان" هستند، پس حل کنندهٔ SAT به آسانی می تواند یک راه حل بیابد یا اثبات کند که وجود ندارد؛ با وجود آنکه آن مورد هزاران متغیر و ده ها هزار محدودیت دارد. بقیهٔ مسائل کوچک زمان های اجرایی را ارائه می دهند که به صورت نمایی باشند و به مرور غیرعملی شده اند. متأسفانه هیچ راه قابل اطمینانی وجود ندارد که سختی مسئله را بدون امتحان آن بیان کند. پس تقریباً همهٔ حل کننده های SAT شامل زمان های اضافه می شوند، پس با آنکه هیچ راه حلی نیافته اند اما به پایان خواهند رسید. در نهایت حل کننده های SAT مختلفی موارد مختلف آسان یا سخت را پیدا خواهند کرد و بعضی از آن ها در اثبات صدق ناپذیری و دیگران در یافتن راه
حل برترند. همهٔ آن رفتارها در مسابقه های حل SAT دیده می شوند. قابلیت کاهش دادن خود. از یک الگوریتم که به درستی می گوید یک مثال از SAT قابل حل است یا نه، می توان برای یافتن واگذاری صدق پذیر استفاده کرد. در ابتدا سؤال از فرمول formula_10 پرسیده می شود. اگر جواب "خیر" باشد، فرمول صدق ناپذیر است. در غیر این صورت سؤال از formula_11 پرسیده می شود، یعنی اولین متغیر 0 در نظر گرفته می شود. اگر جواب "خیر" باشد، فرض می کنیم formula_12. به همین ترتیب مقادیر بقیهٔ متغیرها به دست می آیند. این ویژگی در تئوری های مختلفی از قضیهٔ پیچیدگی استفاده می شود: الگوریتم های حل کنندهٔ SAT. دو رده از الگوریتم های با کارایی بالا برای حل مسائل SAT وجود دارد: الگوریتم تضاد-راندهٔ شناختن عبارت، که می توان به عنوان نوعی دیگر از الگوریتم های DPLL به آن نگاه کرد، و همچنین الگوریتم های اتفاقی جستجوی محلی مانند WalkSAT. یک حل کنندهٔ مسئلهٔ صدق پذیری DPLL، یک روند جستجوی بازگشتی اصولی را به کار می گیرد تا فاصلهٔ واگذاری متغیرها برای یافتن واگذاری صدق پذیر را کشف کند. در اوایل دههٔ 60 میلادی، روند اصلی جستجو در دو مقاله مطرح شد (منابع زیر را ببین
ید) و حال به عنوان الگوریتم دیویس-پاتنام-لاگمن-لاولند (یا به اختصار DPLL یا DLL) مشهور است. از لحاظ تئوری کران پایین نمایی برای خانوادهٔ الگوریتم های DPLL اثبات شده است. حل کننده های SAT نوین (که در 10 سال گذشته ایجاد شدند) در دو نوع بیان می شوند: "تضاد-رانده" و "پیش بین". حل کننده های تضاد-رانده الگوریتم جستجوی DPLL اصلی را با تحلیل تضاد کارآمد، شناختن عبارت، بازگشت بدون ترتیب زمانی (الگوریتم پس پرش)، و همچنین انتشار واحد "دو-متغیر-تماشا"، انشعاب انطباقی و راه اندازی مجدد تصادفی، افزایش می دهند. نشان داده شده است که این "الحاقات" اصولی جستجو به صورت تجربی برای رسیدگی به موارد زیادی از SAT که در اتوماسیون طراحی الکترونیکی (EDA) به وجود می آیند ضروری هستند. حل کننده های پیش بین به خصوص کاهش ها (رفتن به ورای انتشار عبارت واحد) و کشف کننده ها را تشدید کردند و در کل در موارد پیچیده از حل کننده های تضاد-رانده قوی تر عمل می کنند. حل کننده های SAT نوین تأثیرات مهمی بر زمینه های تأیید نرم افزاری، حل کردن محدودیت های هوش مصنوعی و تحقیق در عملیات دارند. حل کننده های قوی به آسانی به صورت نرم افزار آزاد و متن باز در دستر
س هستند. به طور خاص نرم افزار تضاد-راندهٔ MiniSAT که در مسابقهٔ SAT در سال 2005 نسبتاً موفق بود، فقط دارای حدود 600 خط برنامه است. یک مثال از حل کننده های پیش بین march_dl است که در مسابقهٔ SAT در سال 2007 برنده شد. انواع خاصی از موارد بزرگ تصادفی صدق پذیر از SAT با انتشار نظرسنجی (SP) قابل حل هستند. به خصوص در طراحی پردازنده و برنامه های تایید، صدق پذیری و دیگر خواص منطقی از فرمول گزاره ای داده شده بعضی اوقات بر پایهٔ نمایشی از فرمول در نمودار تصمیم گیری دودویی (BDD) تصمیم گیری می شوند. پیوند به بیرون. اطلاعات بیشتر در مورد SAT: برنامه های SAT: حل کننده های SAT: کنفرانس بین المللی دربارهٔ قضیه و برنامه های آزمایش صدق پذیری: انتشارات: برنامه های محک: حل کردن SAT در حالت کلی: ارزیابی حل کننده های SAT: "این مقاله شامل موادی از یک ستون در ACM SIGDA e-newsletter توسط Prof. Karem Sakallah می باشد."
فردیناند چهارم (آلمانی:Ferdinand IV، مجاری:IV. Ferdinánd)(زادهٔ ۸ سپتامبر ۱۶۳۳- مرگ ۹ ژوئیهٔ ۱۶۵۴) پادشاه رومن ها، پادشاه مجارستان و بوهم بود. او پسر فردیناند سوم، امپراتور مقدس روم از همسر نخستش ماریا آنا بود. نیای مادری او فلیپه سوم، پادشاه اسپانیا بود. او همچنین برادر بزرگتر لئوپولد یکم، امپراتور مقدس روم بود. او در ۱۶۴۶ به پادشاهی بوهم و سال پس از آن به پادشاهی مجارستان رسید. در ۱۶۵۳ میلادی به عنوان پادشاه رومن ها رسید تا زمینه برای رسیدنش به مقام امپراتور مقدس روم فراهم شود، ولی بیماری آبله او را زودتر از پدر از پای درآورد. در نتیجه تاج امپراتور مقدس روم برادر کوچکتر او لئوپولد گردید. مرگ او در وین رخ داد. منابع. Wikipedia contributors, "Ferdinand IV, King of the Romans," Wikipedia, The Free Encyclopedia, http://en.wikipedia.org/w/index.php?title=Ferdinand_IV,_King_of_the_Romans&amp;oldid=451996464 (accessed December 8, 2011).
شراره درشتی (زاده ۲۱ اردیبهشت۱۳۵۴) بازیگر تئاتر، سینما و تلویزیون ایرانی است. زندگی شخصی. وی همسر، رضا ژیان بود. او پس از درگذشت همسرش به سوئیس مهاجرت کرد و از صحنهٔ هنری ایران فاصله گرفت. درشتی در خرداد ۱۳۹۸ در پستی در صفحهٔ اینستاگرامش خبر داد که به علت ابتلا به سرطان در بیمارستان بستری شده است.
جستجو سه تایی در علوم کامپیوتر رویه ی جستجو ترنری مهارتی برای پیدا کردن مقدار بیشینه یا کمینه در توابع أکید است. در این رویه مشخص می کنیم که مقدار بیشینه یا کمینه تابع نمی تواند در یک سوم ابتدا یا انتهای دامنه ی تابع وجود داشته باشد. سپس همین شیوه را بر روی دو سوم باقی مانده به کار می بریم. جستجو سه تایی نمونه ای از روش الگوریتم تقسیم و حل است(الگوریتم جستجو را ببینید.)Ternary search تابع. فرض کنید ما به دنبال بیشینه formula_1 هستیم و می دانیم این مقدار بین formula_2 و formula_3 قرار دارد. برای این که الگوریتم قابل اعمال باشند، یک مقدار formula_4 باید وجود داشته باشد به طوری که: الگوریتم. تابع اکید formula_1 را روی بازه formula_12 در نظر بگیرید. دو نقطه ی formula_13 و formula_14 را در این بازه انتخاب می کنیم. بنابراین formula_15در این صورت سه حالت وجود دارد : این فرایند تا زمانی ادامه پیدا می کند که بازه حاصل از مقدار ثابت از پیش تعیین شده کوچکتر شود. انتخاب نقاط formula_13 و formula_14 : زمان اجرا. T(n) = T(2/3 * n) + c (Θ(log n رویه بازگشتی. def ternarySearch(f, left, right, absolutePrecision): #left and ri
ght are the current bounds; the maximum is between them if (right - left) &lt;absolutePrecision: return (left + right)/2 leftThird = (2*left + right)/3 rightThird = (left + 2*right)/3 if f(leftThird)&gt; f(rightThird): return ternarySearch(f, leftThird, right, absolutePrecision) else: return ternarySearch(f, left, rightThird, absolutePrecision) Ternary search درخت جستجوی سه تایی. درخت جستجوی سه تایی یکی از جالب ترین داده ساختارهادر زمینه دانش خوداست، زیرا این درخت ذخیره سازی بهینه را با سریع پیدا کردن ترکیب می کندو توانایی جستجوی پیشوندرا نیز دارد. قسمتی از نظریه. درخت جستجو سه تایی کمی پیچیده تر از درخت جستجو دوتایی است. علاوه بر درخت جستجوی دودویی، اشاره گر سومی در هر گره وجود دارد. زمانی که بر روی درخت حرکت می کنیم، این اشاره گرهنگامی که مقداری که مقایسه می شود؛ با مقدار گره برابر باشد، استفاده می گردد.در نتیجه این درخت سه اشاره گر چپ، راست، و برابر دارد. که در شکل زیر مشاهده می کنید. شکل زیر درخت جستجو سه تایی رشته های "as", "at", "cup", "cute", "he", "i" and "us" را نشان می دهد: c a u h t t e u s p e i s
پیاده سازی. پیاده سازی تابع search : def search(string) return false unless (string &amp;&amp; !string.empty? &amp;&amp; self.value) head, tail = string.partition if head &lt;self.value return @left.search(string) if @left elsif head == self.value return true if !tail &amp;&amp; self.ending? return @equal.search(tail) if @equal elsif head&gt; self.value return @right.search(string) if @right end end پیاده سازی کلاس string : def search(string)class String def partition [head, tail] end # First character. def head (self.length&gt;= 1) ? self[0].chr : nil end # Cut the first character from the string and return the tail. def tail (self.length&gt;= 2) ? self[1..-1] : nil end end پیاده سازی کلاس درخت جستجوی سه تایی : class Tst def initialize @left = @equal = @right = nil @ending = false end def insert(string) raise ArgumentError unless string.is_a?(String) head, tail = string.partition if self.value.nil? # self.value ? self.value = head # self.value ? end if head &lt;self.value @left = Tst.new unless @left @left.
insert(string) elsif head == self.value if tail @equal = Tst.new unless @equal @equal.insert(tail) else self.ending_here() end elsif head&gt; self.value @right = Tst.new unless @right @right.insert(string) end end def search(string) return false unless (string &amp;&amp; !string.empty? &amp;&amp; self.value) head, tail = string.partition if head &lt;self.value return @left.search(string) if @left elsif head == self.value return true if !tail &amp;&amp; self.ending? return @equal.search(tail) if @equal elsif head&gt; self.value return @right.search(string) if @right end end alias :«:insert alias :[] :search protected def value @value end def value=(value) raise ArgumentError unless acceptable?(value) @value = value end def acceptable?(value) value.is_a?(String) &amp;&amp; value.length == 1 end def ending_here @ending = true end def ending? @ending end end