CRYPTOMINISAT5(1) User Commands CRYPTOMINISAT5(1)

cryptominisat5 - صفحه راهنمای cryptominisat5 نسخه 5.14.7

cryptominisat [--help] [--version] [--verb VAR] [--maxtime VAR] [--maxconfl VAR] [--random VAR] [--threads VAR] [--mult VAR] [--nextm VAR] [--memoutmult VAR] [--maxsol VAR] [--polar VAR] [--scc VAR] [--restart VAR] [--rstfirst VAR] [--gluehist VAR] [--lwrbndblkrest VAR] [--locgmult VAR] [--ratiogluegeom VAR] [--blockingglue VAR] [--gluecut0 VAR] [--gluecut1 VAR] [--adjustglue VAR] [--everylev1 VAR] [--everylev2 VAR] [--lev1usewithin VAR] [--branchstr VAR] [--nobansol] [--debuglib VAR] [--breakid VAR] [--breakideveryn VAR] [--breakidmaxlits VAR] [--breakidmaxcls VAR] [--breakidmaxvars VAR] [--breakidtime VAR] [--breakidcls VAR] [--breakidmatrix VAR] [--sls VAR] [--slstype VAR] [--slsmaxmem VAR] [--slseveryn VAR] [--yalsatmems VAR] [--walksatruns VAR] [--slsgetphase VAR] [--slsccnraspire VAR] [--slstobump VAR] [--slstobumpmaxpervar VAR] [--slsbumptype VAR] [--transred VAR] [--intree VAR] [--intreemaxm VAR] [--otfhyper VAR] [--schedsimp VAR] [--presimp VAR] [--allpresimp VAR] [--nonstop VAR] [--maxnumsimppersolve VAR] [--schedule VAR] [--preschedule VAR] [--occsimp VAR] [--confbtwsimp VAR] [--confbtwsimpinc VAR] [--tern VAR] [--terntimelim VAR] [--ternkeep VAR] [--terncreate VAR] [--ternbincreate VAR] [--occredmax VAR] [--occredmaxmb VAR] [--occirredmaxmb VAR] [--strengthen VAR] [--weakentimelim VAR] [--substimelim VAR] [--substimelimbinratio VAR] [--substimelimlongratio VAR] [--strstimelim VAR] [--sublonggothrough VAR] [--bva VAR] [--bvaeveryn VAR] [--bvalim VAR] [--bva2lit VAR] [--bvato VAR] [--varelim VAR] [--varelimto VAR] [--varelimover VAR] [--emptyelim VAR] [--varelimmaxmb VAR] [--eratio VAR] [--varelimcheckres VAR] [--xor VAR] [--maxxorsize VAR] [--xorfindtout VAR] [--maxxormat VAR] [--gates VAR] [--printgatedot VAR] [--gatefindto VAR] [--recur VAR] [--moreminim VAR] [--moremoreminim VAR] [--moremorealways VAR] [--decbased VAR] [--updateglueonanalysis VAR] [--maxgluehistltlimited VAR] [--diffdeclevelchrono VAR] [--verbstat VAR] [--verbrestart VAR] [--verballrestarts VAR] [--printsol VAR] [--restartprint VAR] [--distill VAR] [--distillbin VAR] [--distillmaxm VAR] [--distillincconf VAR] [--distillminconf VAR] [--distilltier0ratio VAR] [--distilltier1ratio VAR] [--distillirredalsoremratio VAR] [--distillirrednoremratio VAR] [--distillshuffleeveryn VAR] [--distillsort VAR] [--renumber VAR] [--mustconsolidate VAR] [--savemem VAR] [--mustrenumber VAR] [--fullwatchconseveryn VAR] [--strmaxt VAR] [--implicitmanip VAR] [--implsubsto VAR] [--implstrto VAR] [--cardfind VAR] [--sync VAR] [--clearinter VAR] [--zero-exit-status] [--printtimes VAR] [--maxsccdepth VAR] [--sampling VAR] [--assump VAR] [--maxmatrixrows VAR] [--maxmatrixcols VAR] [--autodisablegauss VAR] [--minmatrixrows VAR] [--maxnummatrices VAR] [--gaussusefulcutoff VAR] [--dumpresult VAR] files

فایل ورودی و خروجی FRAT [تعداد آرگومان‌ها: ۰ یا بیشتر]

نمایش پیام راهنما و خروج
چاپ اطلاعات نسخه
[0-10] میزان پرگویی (verbosity) حل‌کننده. مقدار ۰ = فقط راه‌حل [nargs=0..1] [پیش‌فرض: 1]
توقف حل پس از این مقدار زمان (ثانیه)
توقف حل پس از این تعداد تعارض (conflict)
[0..] بذر تصادفی (random seed) [nargs=0..1] [پیش‌فرض: 0]
تعداد رشته‌ها (threads) [nargs=0..1] [پیش‌فرض: 1]
ضریب زمان برای تمامی آستانه‌های ساده‌سازی [nargs=0..1] [پیش‌فرض: 3]
ضریب سراسری برای زمان اجرای پردازش در حین حل (inprocessing) بعدی [nargs=0..1] [پیش‌فرض: 1]
ضریب بررسی‌های اتمام حافظه روی توابع inprocessing. مواردی مانند پیوند بندها (clause-link-in) را محدود می‌کند. زمانی که حافظه محدودی دارید اما هم‌چنان مایل به انجام مقداری inprocessing هستید مفید است [nargs=0..1] [پیش‌فرض: 1]
جست‌وجو برای تعداد مشخصی راه‌حل. با تشکر از Jannis Harder برای ایده ممنوع‌سازی مبتنی بر تصمیم (decision-based banning) [nargs=0..1] [پیش‌فرض: 1]
{true,false,rnd,auto,stable} انتخاب حالت قطبیت (polarity). مقدار 'true' -> هنگام انشعاب، فقط قطبیت مثبت را انتخاب می‌کند. 'false' -> هنگام انشعاب، فقط قطبیت منفی را انتخاب می‌کند. 'auto' -> آخرین قطبیت استفاده‌شده را انتخاب می‌کند (که با عنوان 'caching' نیز شناخته می‌شود) [nargs=0..1] [پیش‌فرض: "auto"]
یافتن لیترال‌های معادل از طریق SCC (مؤلفه‌های قویاً همبند) و جایگزینی آن‌ها [nargs=0..1] [پیش‌فرض: 1]
{geom, glue, luby} راهبرد راه‌اندازی مجدد (restart) برای دنبال کردن. [nargs=0..1] [پیش‌فرض: "auto"]
اندازه پایه راه‌اندازی مجدد [nargs=0..1] [پیش‌فرض: 100]
اندازه پنجره متحرک برای تاریخچه کوتاه‌مدت glue بندهای زائد. هرچه بالاتر باشد، حداقل تعداد تعارض‌ها بین راه‌اندازی‌های مجدد بیشتر است [nargs=0..1] [پیش‌فرض: 50]
حد پایین برای راه‌اندازی مجدد مسدودکننده -- پیش از این تعداد تعارض مسدود نکن [nargs=0..1] [پیش‌فرض: 10000]
ضریب مورد استفاده برای تعیین این‌که آیا باید در طول راه‌اندازی مجدد مبتنی بر glue، راه‌اندازی مجدد انجام گیرد یا خیر [nargs=0..1] [پیش‌فرض: 0.8]
نسبت راه‌اندازی‌های مجدد glue به هندسی (geometric) -- مقدار بیشتر یعنی استفاده بیشتر از glue [nargs=0..1] [پیش‌فرض: 5]
انجام راه‌اندازی مجدد مسدودکننده برای مقادیر glue [nargs=0..1] [پیش‌فرض: 1]
مقدار glue برای برش سطح ۰ ('نگه‌داری') [nargs=0..1] [پیش‌فرض: 3]
مقدار glue برای برش سطح ۱ ('فرصت دوباره') [nargs=0..1] [پیش‌فرض: 6]
اگر بیش از این درصد از بندها دارای glue پایین (سطح ۰) باشند، حد آستانه glue را ۱ واحد کاهش بده -- یک‌بار و هرگز دوباره تکرار نشود [nargs=0..1] [پیش‌فرض: 0.7]
کاهش بندهای سطح ۱ (lev1) در هر N گام [nargs=0..1] [پیش‌فرض: 10000]
کاهش بندهای سطح ۲ (lev2) در هر N گام [nargs=0..1] [پیش‌فرض: 15000]
بند فراگرفته‌شده باید در این بازه زمانی در سطح ۱ استفاده شود، در غیر این صورت به سطح ۲ منتقل می‌شود [nargs=0..1] [پیش‌فرض: 70000]
رشته راهبرد انشعاب که حین حل بین راهبردهای مختلف جابه‌جا می‌شود؛ مانند 'vsids1+vsids2' [nargs=0..1] [پیش‌فرض: "vmtf+vsids"]
عدم ممنوع‌سازی راه‌حل پس از یافتن آن
تجزیه یادداشت‌های (comments) ویژه برای اجرای solve/simplify حین تجزیه CNF
اجرای BreakID برای شکستن تقارن‌ها. [nargs=0..1] [پیش‌فرض: false]
اجرای BreakID در هر N تکرارِ ساده‌سازی [nargs=0..1] [پیش‌فرض: 5]
حداکثر تعداد لیترال‌ها به هزار. در صورت فراتر رفتن، BreakID اجرا نخواهد شد [nargs=0..1] [پیش‌فرض: 3500]
حداکثر تعداد بندها به هزار. در صورت فراتر رفتن، BreakID اجرا نخواهد شد [nargs=0..1] [پیش‌فرض: 600]
حداکثر تعداد متغیرها به هزار. در صورت فراتر رفتن، BreakID اجرا نخواهد شد [nargs=0..1] [پیش‌فرض: 300]
حداکثر تعداد گام‌های برداشته‌شده حین یافتن خودریختی (automorphism). [nargs=0..1] [پیش‌فرض: 2000]
حداکثر تعداد بندهای شکننده به ازای هر جایگشت. [nargs=0..1] [پیش‌فرض: 50]
تشخیص تعویض‌پذیری سطر ماتریس [nargs=0..1] [پیش‌فرض: true]
اجرای SLS در طول ساده‌سازی [nargs=0..1] [پیش‌فرض: 1]
کدام SLS اجرا شود. مقادیر مجاز: walksat، yalsat، ccnr، ccnr_yalsat [nargs=0..1] [پیش‌فرض: "ccnr"]
حداکثر حافظه به مگابایت برای حل‌کننده SLS. اگر مصرف حافظه بیشتر از این مقدار باشد، حل‌کننده SLS را اجرا نمی‌کند. [nargs=0..1] [پیش‌فرض: 500]
اجرای حل‌کننده SLS فقط در هر N مرحله ساده‌سازی [nargs=0..1] [پیش‌فرض: 2]
اجرای Yalsat با مهلت زمانی این مقدار میلیون دسترسی به حافظه (mems*million). زمان اجرای yalsat را محدود می‌کند [nargs=0..1] [پیش‌فرض: 10]
حداکثر 'اجراها' (runs) برای WalkSAT. زمان اجرای WalkSAT را محدود می‌کند [nargs=0..1] [پیش‌فرض: 50]
دریافت فاز از حل‌کننده SLS و تنظیم آن به‌عنوان فاز جدید برای CDCL [nargs=0..1] [پیش‌فرض: 1]
فعال/غیرفعال کردن آرزومندی (aspiration) برای CCNR [nargs=0..1] [پیش‌فرض: 1]
تعداد متغیرها جهت ارتقای فعالیت (bump) در CCNR [nargs=0..1] [پیش‌فرض: 100]
حداکثر دفعات ارتقای فعالیت یک متغیر مجزا در CCNR [nargs=0..1] [پیش‌فرض: 100]
نحوه محاسبه متغیری که باید فعالیتش ارتقا یابد (bump). مقدار ۱ = مبتنی بر بند، ۲ = مبتنی بر وارون‌سازی متغیر، ۳ = مبتنی بر امتیاز متغیر [nargs=0..1] [پیش‌فرض: 6]
حذف بندهای دوتایی بی‌فایده (کاهش متعدی یا transitive reduction) [nargs=0..1] [پیش‌فرض: 1]
انجام کاوش بر پایه درخت درونی (intree-based probing) [nargs=0..1] [پیش‌فرض: 1]
زمان بر حسب mega-bogoprops برای انجام کاوش درون‌درختی [nargs=0..1] [پیش‌فرض: 400]
انجام تفکیک فرادوتایی در حین کار (on-the-fly hyper-binary resolution) در طول کاوش [nargs=0..1] [پیش‌فرض: 1]
انجام دورهای ساده‌سازی. در صورت مقدار ۰، هیچ‌کدام انجام نمی‌شوند. [nargs=0..1] [پیش‌فرض: 1]
انجام ساده‌سازی در همان ابتدای کار [nargs=0..1] [پیش‌فرض: 0]
انجام ساده‌سازی در هر بار شروع -- فقط در حالت کتابخانه‌ای کاربرد دارد [nargs=0..1] [پیش‌فرض: 0]
فرایند search() در کلاس SATSolver هرگز متوقف نشود [nargs=0..1] [پیش‌فرض: 0].TP --maxnumsimppersolve حداکثر تعداد ساده‌سازی‌ها برای اجرا به ازای هر فراخوانی solve(). پس از این، دیگر هیچ پردازش حین حلی انجام نخواهد شد. [nargs=0..1] [پیش‌فرض: 25]
زمان‌بندی ساده‌سازی در طول اجرا
زمان‌بندی ساده‌سازی هنگام راه‌اندازی
انجام بهینه‌سازی‌های مبتنی بر فهرست رخدادها (حذف متغیر، شمول، افزودن متغیر محدودشده و...) [nargs=0..1] [پیش‌فرض: 1]
شروع نخستین ساده‌سازی پس از این تعداد تعارض [nargs=0..1] [پیش‌فرض: 40000]
افزایش دورهای ساده‌سازی با این توان از N [nargs=0..1] [پیش‌فرض: 1.4]
انجام تفکیک سه‌تایی (Ternary resolution) [nargs=0..1] [پیش‌فرض: true]
مهلت زمانی بر حسب میلیون bogoprops برای تفکیک سه‌تایی مطابق با مقاله “Look-Ahead Versus Look-Back for Satisfiability Problems” [nargs=0..1] [پیش‌فرض: 100]
نگه‌داری بندهای تفکیک سه‌تایی تنها در صورتی که در این مضرب از “lev1usewithin” استفاده شوند [nargs=0..1] [پیش‌فرض: 5]
ایجاد بندهای تفکیک سه‌تایی در هر دور ساده‌سازی، فقط تا این مضرب (از بندهای پیوندیافته) [nargs=0..1] [پیش‌فرض: 0.3]
مجاز دانستن تفکیک سه‌تایی برای تولید بندهای دوتایی [nargs=0..1] [پیش‌فرض: 0]
عدم افزودن بندهای زائد بزرگ‌تر از این مقدار به فهرست رخدادها [nargs=0..1] [پیش‌فرض: 50]
جلوگیری از فراتر رفتن اندازه رخدادهای زائد از این مقدار مگابایت [nargs=0..1] [پیش‌فرض: 600]
جلوگیری از فراتر رفتن اندازه رخدادهای غیرزائد از این مقدار مگابایت [nargs=0..1] [پیش‌فرض: 2500]
انجام انقباض بند از طریق تفکیک خودشمول به عنوان بخشی از سامانه رخداد-شمول [nargs=0..1] [پیش‌فرض: 1]
مهلت زمانی بر حسب میلیون bogoprops برای تضعیف مورداستفاده [nargs=0..1] [پیش‌فرض: 300]
مهلت زمانی بر حسب میلیون bogoprops برای شمول بندهای طولانی با بندهای طولانی، پس از محاسبه رخدادها [nargs=0..1] [پیش‌فرض: 300]
نسبت محدودیت زمانی شمول برای صرف روی شمول و تقویت (sub&str) بندهای طولانی با بندهای دوتایی [nargs=0..1] [پیش‌فرض: 0.1]
نسبت محدودیت زمانی شمول برای صرف روی شمول بندهای طولانی با بندهای طولانی [nargs=0..1] [پیش‌فرض: 0.9]
مهلت زمانی بر حسب میلیون bogoprops برای تقویت بندهای طولانی با بندهای طولانی، پس از محاسبه رخدادها [nargs=0..1] [پیش‌فرض: 300]
تعداد دفعات پیمایش فرایند شمول [nargs=0..1] [پیش‌فرض: 1]
انجام افزودن متغیر محدودشده (BVA) [nargs=0..1] [پیش‌فرض: 0]
انجام BVA فقط به ازای هر N فراخوانی ساده‌سازی رخدادها [nargs=0..1] [پیش‌فرض: 7]
حداکثر تعداد متغیرهای افزوده شده توسط BVA در هر فراخوانی [nargs=0..1] [پیش‌فرض: 250000]
انجام BVA با ترفند اختلاف ۲ لفظی نیز فعال باشد. هشدار: این کار اثربخشی اختلاف ۱ لفظی را کاهش می‌دهد [nargs=0..1] [پیش‌فرض: 1]
محدودیت زمانی BVA بر حسب میلیون bogoprops [nargs=0..1] [پیش‌فرض: 50]
انجام حذف متغیر بر اساس روش Een و Biere [nargs=0..1] [پیش‌فرض: 1]
محدودیت زمانی حذف متغیر بر حسب میلیون bogoprops [nargs=0..1] [پیش‌فرض: 750]
انجام BVE تا زمانی که افزایش حاصل در تعداد بندها کمتر از X باشد. تنها توان‌های ۲ معنادار هستند؛ مانند ۲، ۴، ۸ و... [nargs=0..1] [پیش‌فرض: 16]
انجام حذف حاصل‌تفکیک‌های خالی با استفاده از ترفند بیت‌مپ [nargs=0..1] [پیش‌فرض: 1]
حداکثر حافظه اضافی بر حسب مگابایت برای استفاده در بندهای جدید هنگام varelim [nargs=0..1] [پیش‌فرض: 1000]
حذف حداکثر این نسبت از متغیرهای آزاد در هر دور از حذف متغیر [nargs=0..1] [پیش‌فرض: 1.6]
بررسی این که آیا حاصل‌تفکیک‌ها موارد دیگر را شمول می‌کنند یا خیر، و بررسی دقیق افزایش اندازه توسط BVE [nargs=0..1] [پیش‌فرض: 0]
کشف XORهای طولانی [nargs=0..1] [پیش‌فرض: 1]
حداکثر اندازه XOR برای یافتن [nargs=0..1] [پیش‌فرض: 7]
محدودیت زمانی برای یافتن XORها [nargs=0..1] [پیش‌فرض: 400]
حداکثر اندازه ماتریس (=تعداد عناصر) که باید برای پلکانی کردن آن تلاش شود [nargs=0..1] [پیش‌فرض: 400]
یافتن گیت‌ها. [nargs=0..1] [پیش‌فرض: 0]
چاپ منظم ساختار گیت در فایل “gatesX.dot” [nargs=0..1] [پیش‌فرض: 0]
حداکثر زمان بر حسب میلیون bogoprops برای یافتن گیت‌ها [nargs=0..1] [پیش‌فرض: 200]
انجام کمینه‌سازی بازگشتی [nargs=0..1] [پیش‌فرض: 1]
انجام کمینه‌سازی قوی هنگام تولید تعارض [nargs=0..1] [پیش‌فرض: 1]
انجام کمینه‌سازی باز هم قوی‌تر هنگام تولید تعارض [nargs=0..1] [پیش‌فرض: 2]
همواره بندها به صورت قوی کمینه‌سازی شوند [nargs=0..1] [پیش‌فرض: 0]
ایجاد بندهای تعارض مبتنی بر تصمیم هنگامی که بند UIP بیش از حد بزرگ باشد [nargs=0..1] [پیش‌فرض: 1]
به‌روزرسانی مقادیر glue هنگام تحلیل [nargs=0..1] [پیش‌فرض: 1]
حداکثر glue مورداستفاده در راهبرد بازراه‌اندازی مبتنی بر glue هنگام پر کردن تاریخچه glue. [nargs=0..1] [پیش‌فرض: 50]
اگر اختلاف در سطح تصمیم‌گیری بیش از این مقدار باشد، پسگرد زمانی به جای پسگرد غیرزمانی انجام می‌شود. مقدار -1 به معنای عدم فعال‌سازی همیشگی آن است (در این حالت، “--confltochrono -1” نادیده گرفته می‌شود). [nargs=0..1] [پیش‌فرض: 20]
تغییر میزان جزئیات آمار در پایان فرایند حل مسئله [0..3] [nargs=0..1] [پیش‌فرض: 2]
چاپ آمار دقیق‌تر، اما متفاوت [nargs=0..1] [پیش‌فرض: 0]
چاپ یک خط به ازای هر بازراه‌اندازی [nargs=0..1] [پیش‌فرض: 0]
چاپ تخصیص متغیرها در صورتی که پاسخ SAT باشد [nargs=0..1] [پیش‌فرض: 1]
چاپ خطوط وضعیت بازراه‌اندازی دست‌کم به ازای هر N تعارض [nargs=0..1] [پیش‌فرض: 8192]
اجرای منظم تقطیر بندها [nargs=0..1] [پیش‌فرض: 1]
اجرای منظم تقطیر بندهای دوتایی [nargs=0..1] [پیش‌فرض: 1]
حداکثر تعداد مگا-bogoprops (حدوداً معادل زمان) برای صرف روی حیات‌بخشی/تقطیر بندهای طولانی از طریق صف‌بندی و انتشار [nargs=0..1] [پیش‌فرض: 200]
ضریب تعداد فعلی تعارض‌ها در تقطیر بلادرنگ (OTF distill) [nargs=0..1] [پیش‌فرض: 0.1]
حداقل تعداد تعارض‌ها میان تقطیرهای بلادرنگ [nargs=0..1] [پیش‌فرض: 10000]
میزان تقطیر رده ۰ [nargs=0..1] [پیش‌فرض: 10]
میزان تقطیر رده ۱ [nargs=0..1] [پیش‌فرض: 0.03].TP --distillirredalsoremratio چه میزانی از irred در هنگام انجام حذف (removal) نیز تقطیر شود [nargs=0..1] [پیش‌فرض: 1.2]
چه میزانی از irred در صورت عدم انجام حذف تقطیر شود [nargs=0..1] [پیش‌فرض: 1]
بُر زدن تصادفی بندهای در شرف تقطیر هر N مورد یک‌بار [nargs=0..1] [پیش‌فرض: 3]
نوع مرتب‌سازی تقطیر [nargs=0..1] [پیش‌فرض: 1]
شماره‌گذاری مجدد متغیرها برای افزایش کارایی حافظه نهان (کش) پردازنده [nargs=0..1] [پیش‌فرض: 1]
تجمیع همیشگی، حتی اگر مفید نباشد. این گزینه فقط برای اشکال‌زدایی استفاده می‌شود [nargs=0..1] [پیش‌فرض: 0]
صرفه‌جویی در حافظه با آزادسازی فضای متغیرها پس از شماره‌گذاری مجدد. فقط در صورت فعال بودن شماره‌گذاری مجدد کار می‌کند. [nargs=0..1] [پیش‌فرض: 1]
در نظر گرفتن تمام راهبردهای 'renumber' به عنوان 'must-renumber' [nargs=0..1] [پیش‌فرض: 0]
تجمیع کامل فهرست‌های دیده‌بانی (watchlists) هر N تداخل یک‌بار. در طول دورهای ساده‌سازی زمان‌بندی می‌شود. [nargs=0..1] [پیش‌فرض: 4000000]
حداکثر MBP قابل مصرف برای تقطیر بندهای طولانی irred از طریق دیده‌بان‌ها [nargs=0..1] [پیش‌فرض: 20]
شمول (subsume) و تقویت بندهای ضمنی با یکدیگر [nargs=0..1] [پیش‌فرض: 1]
مهلت زمانی (به میلیون bogoprop) برای شمول ضمنی [nargs=0..1] [پیش‌فرض: 100]
مهلت زمانی (به میلیون bogoprop) برای تقویت ضمنی [nargs=0..1] [پیش‌فرض: 200]
یافتن محدودیت‌های عدد اصلی (cardinality constraints) [nargs=0..1] [پیش‌فرض: 0]
همگام‌سازی رشته‌ها (threads) هر N تداخل یک‌بار [nargs=0..1] [پیش‌فرض: 7000]
قطع رشته‌ها به صورت تمیز در تمام مدت [nargs=0..1] [پیش‌فرض: 0]
خروج با وضعیت صفر در صورتی که حل مسئله بدون مشکل به پایان رسیده باشد
چاپ زمان صرف‌شده برای هر اجرای ساده‌سازی. در صورت تنظیم روی 0، مقایسه لاگ‌ها آسان‌تر خواهد بود [nargs=0..1] [پیش‌فرض: 1]
حداکثر عمق جستجوی scc [nargs=0..1] [پیش‌فرض: 10000]
تنظیم متغیرهای نمونه‌برداری مانند '1,84,44'. همچنین از طریق CNF با استفاده از 'c p show 1 84 44 0' قابل تنظیم است
فایل فرضیات [nargs=0..1] [پیش‌فرض: ""]
تنظیم حداکثر تعداد ردیف‌ها برای ماتریس گاوسی. ماتریس‌های بیش از حد بزرگ باید به دلایل کارایی کنار گذاشته شوند [nargs=0..1] [پیش‌فرض: 2000]
تنظیم حداکثر تعداد ستون‌ها برای ماتریس گاوسی. ماتریس‌های بیش از حد بزرگ باید به دلایل کارایی کنار گذاشته شوند [nargs=0..1] [پیش‌فرض: 1000]
غیرفعال‌سازی خودکار گاوس هنگامی که کارایی نامطلوبی دارد [nargs=0..1] [پیش‌فرض: true]
تنظیم حداقل تعداد ردیف‌ها برای ماتریس گاوسی. معمولاً ماتریس‌های بیش از حد کوچک به دلایل کارایی کنار گذاشته می‌شوند [nargs=0..1] [پیش‌فرض: 3]
حداکثر تعداد ماتریس‌ها برای پردازش. [nargs=0..1] [پیش‌فرض: 5]
غیرفعال‌سازی گاوس در صورتی که نسبت سودمندی کمتر از این مقدار ثبت شود [nargs=0..1] [پیش‌فرض: 0.2]
نوشتن راه‌حل(ها) در این فایل.SH "همچنین ببینید (SEE ALSO)" مستندات کامل cryptominisat5 به‌صورت یک راهنمای Texinfo نگهداری می‌شود. اگر برنامه‌های info و cryptominisat5 به‌درستی روی سیستم شما نصب شده باشند، دستور
info cryptominisat5

باید دسترسی به راهنمای کامل را فراهم کند.

June 2026 cryptominisat5 5.14.7