.\" DO NOT MODIFY THIS FILE!  It was generated by help2man 1.49.3.
.TH CRYPTOMINISAT5 "1" "June 2026" "cryptominisat5 5.14.7" "User Commands"
.SH "نام (NAME)"
cryptominisat5 \- صفحه راهنمای cryptominisat5 نسخه 5.14.7
.SH "خلاصه دستور (SYNOPSIS)"
.B cryptominisat
[\fI\,--help\/\fR] [\fI\,--version\/\fR] [\fI\,--verb VAR\/\fR] [\fI\,--maxtime VAR\/\fR] [\fI\,--maxconfl VAR\/\fR] [\fI\,--random VAR\/\fR] [\fI\,--threads VAR\/\fR] [\fI\,--mult VAR\/\fR] [\fI\,--nextm VAR\/\fR] [\fI\,--memoutmult VAR\/\fR] [\fI\,--maxsol VAR\/\fR] [\fI\,--polar VAR\/\fR] [\fI\,--scc VAR\/\fR] [\fI\,--restart VAR\/\fR] [\fI\,--rstfirst VAR\/\fR] [\fI\,--gluehist VAR\/\fR] [\fI\,--lwrbndblkrest VAR\/\fR] [\fI\,--locgmult VAR\/\fR] [\fI\,--ratiogluegeom VAR\/\fR] [\fI\,--blockingglue VAR\/\fR] [\fI\,--gluecut0 VAR\/\fR] [\fI\,--gluecut1 VAR\/\fR] [\fI\,--adjustglue VAR\/\fR] [\fI\,--everylev1 VAR\/\fR] [\fI\,--everylev2 VAR\/\fR] [\fI\,--lev1usewithin VAR\/\fR] [\fI\,--branchstr VAR\/\fR] [\fI\,--nobansol\/\fR] [\fI\,--debuglib VAR\/\fR] [\fI\,--breakid VAR\/\fR] [\fI\,--breakideveryn VAR\/\fR] [\fI\,--breakidmaxlits VAR\/\fR] [\fI\,--breakidmaxcls VAR\/\fR] [\fI\,--breakidmaxvars VAR\/\fR] [\fI\,--breakidtime VAR\/\fR] [\fI\,--breakidcls VAR\/\fR] [\fI\,--breakidmatrix VAR\/\fR] [\fI\,--sls VAR\/\fR] [\fI\,--slstype VAR\/\fR] [\fI\,--slsmaxmem VAR\/\fR] [\fI\,--slseveryn VAR\/\fR] [\fI\,--yalsatmems VAR\/\fR] [\fI\,--walksatruns VAR\/\fR] [\fI\,--slsgetphase VAR\/\fR] [\fI\,--slsccnraspire VAR\/\fR] [\fI\,--slstobump VAR\/\fR] [\fI\,--slstobumpmaxpervar VAR\/\fR] [\fI\,--slsbumptype VAR\/\fR] [\fI\,--transred VAR\/\fR] [\fI\,--intree VAR\/\fR] [\fI\,--intreemaxm VAR\/\fR] [\fI\,--otfhyper VAR\/\fR] [\fI\,--schedsimp VAR\/\fR] [\fI\,--presimp VAR\/\fR] [\fI\,--allpresimp VAR\/\fR] [\fI\,--nonstop VAR\/\fR] [\fI\,--maxnumsimppersolve VAR\/\fR] [\fI\,--schedule VAR\/\fR] [\fI\,--preschedule VAR\/\fR] [\fI\,--occsimp VAR\/\fR] [\fI\,--confbtwsimp VAR\/\fR] [\fI\,--confbtwsimpinc VAR\/\fR] [\fI\,--tern VAR\/\fR] [\fI\,--terntimelim VAR\/\fR] [\fI\,--ternkeep VAR\/\fR] [\fI\,--terncreate VAR\/\fR] [\fI\,--ternbincreate VAR\/\fR] [\fI\,--occredmax VAR\/\fR] [\fI\,--occredmaxmb VAR\/\fR] [\fI\,--occirredmaxmb VAR\/\fR] [\fI\,--strengthen VAR\/\fR] [\fI\,--weakentimelim VAR\/\fR] [\fI\,--substimelim VAR\/\fR] [\fI\,--substimelimbinratio VAR\/\fR] [\fI\,--substimelimlongratio VAR\/\fR] [\fI\,--strstimelim VAR\/\fR] [\fI\,--sublonggothrough VAR\/\fR] [\fI\,--bva VAR\/\fR] [\fI\,--bvaeveryn VAR\/\fR] [\fI\,--bvalim VAR\/\fR] [\fI\,--bva2lit VAR\/\fR] [\fI\,--bvato VAR\/\fR] [\fI\,--varelim VAR\/\fR] [\fI\,--varelimto VAR\/\fR] [\fI\,--varelimover VAR\/\fR] [\fI\,--emptyelim VAR\/\fR] [\fI\,--varelimmaxmb VAR\/\fR] [\fI\,--eratio VAR\/\fR] [\fI\,--varelimcheckres VAR\/\fR] [\fI\,--xor VAR\/\fR] [\fI\,--maxxorsize VAR\/\fR] [\fI\,--xorfindtout VAR\/\fR] [\fI\,--maxxormat VAR\/\fR] [\fI\,--gates VAR\/\fR] [\fI\,--printgatedot VAR\/\fR] [\fI\,--gatefindto VAR\/\fR] [\fI\,--recur VAR\/\fR] [\fI\,--moreminim VAR\/\fR] [\fI\,--moremoreminim VAR\/\fR] [\fI\,--moremorealways VAR\/\fR] [\fI\,--decbased VAR\/\fR] [\fI\,--updateglueonanalysis VAR\/\fR] [\fI\,--maxgluehistltlimited VAR\/\fR] [\fI\,--diffdeclevelchrono VAR\/\fR] [\fI\,--verbstat VAR\/\fR] [\fI\,--verbrestart VAR\/\fR] [\fI\,--verballrestarts VAR\/\fR] [\fI\,--printsol VAR\/\fR] [\fI\,--restartprint VAR\/\fR] [\fI\,--distill VAR\/\fR] [\fI\,--distillbin VAR\/\fR] [\fI\,--distillmaxm VAR\/\fR] [\fI\,--distillincconf VAR\/\fR] [\fI\,--distillminconf VAR\/\fR] [\fI\,--distilltier0ratio VAR\/\fR] [\fI\,--distilltier1ratio VAR\/\fR] [\fI\,--distillirredalsoremratio VAR\/\fR] [\fI\,--distillirrednoremratio VAR\/\fR] [\fI\,--distillshuffleeveryn VAR\/\fR] [\fI\,--distillsort VAR\/\fR] [\fI\,--renumber VAR\/\fR] [\fI\,--mustconsolidate VAR\/\fR] [\fI\,--savemem VAR\/\fR] [\fI\,--mustrenumber VAR\/\fR] [\fI\,--fullwatchconseveryn VAR\/\fR] [\fI\,--strmaxt VAR\/\fR] [\fI\,--implicitmanip VAR\/\fR] [\fI\,--implsubsto VAR\/\fR] [\fI\,--implstrto VAR\/\fR] [\fI\,--cardfind VAR\/\fR] [\fI\,--sync VAR\/\fR] [\fI\,--clearinter VAR\/\fR] [\fI\,--zero-exit-status\/\fR] [\fI\,--printtimes VAR\/\fR] [\fI\,--maxsccdepth VAR\/\fR] [\fI\,--sampling VAR\/\fR] [\fI\,--assump VAR\/\fR] [\fI\,--maxmatrixrows VAR\/\fR] [\fI\,--maxmatrixcols VAR\/\fR] [\fI\,--autodisablegauss VAR\/\fR] [\fI\,--minmatrixrows VAR\/\fR] [\fI\,--maxnummatrices VAR\/\fR] [\fI\,--gaussusefulcutoff VAR\/\fR] [\fI\,--dumpresult VAR\/\fR] \fI\,files\/\fR
.SH "توضیحات (DESCRIPTION)"
.SS "آرگومان‌های موضعی (Positional arguments):"
.TP
files
فایل ورودی و خروجی FRAT [تعداد آرگومان‌ها: ۰ یا بیشتر]
.SS "گزینه‌های اختیاری (Optional arguments):"
.TP
\fB\-h\fR, \fB\-\-help\fR
نمایش پیام راهنما و خروج
.TP
\fB\-v\fR, \fB\-\-version\fR
چاپ اطلاعات نسخه
.TP
\fB\-\-verb\fR
[0\-10] میزان پرگویی (verbosity) حل‌کننده. مقدار ۰ = فقط راه‌حل [nargs=0..1] [پیش‌فرض: 1]
.TP
\fB\-\-maxtime\fR
توقف حل پس از این مقدار زمان (ثانیه)
.TP
\fB\-\-maxconfl\fR
توقف حل پس از این تعداد تعارض (conflict)
.TP
\fB\-r\fR, \fB\-\-random\fR
[0..] بذر تصادفی (random seed) [nargs=0..1] [پیش‌فرض: 0]
.TP
\fB\-t\fR, \fB\-\-threads\fR
تعداد رشته‌ها (threads) [nargs=0..1] [پیش‌فرض: 1]
.TP
\fB\-m\fR, \fB\-\-mult\fR
ضریب زمان برای تمامی آستانه‌های ساده‌سازی [nargs=0..1] [پیش‌فرض: 3]
.TP
\fB\-\-nextm\fR
ضریب سراسری برای زمان اجرای پردازش در حین حل (inprocessing) بعدی [nargs=0..1] [پیش‌فرض: 1]
.TP
\fB\-\-memoutmult\fR
ضریب بررسی‌های اتمام حافظه روی توابع inprocessing. مواردی مانند پیوند بندها (clause\-link\-in) را محدود می‌کند. زمانی که حافظه محدودی دارید اما هم‌چنان مایل به انجام مقداری inprocessing هستید مفید است [nargs=0..1] [پیش‌فرض: 1]
.TP
\fB\-\-maxsol\fR
جست‌وجو برای تعداد مشخصی راه‌حل. با تشکر از Jannis Harder برای ایده ممنوع‌سازی مبتنی بر تصمیم (decision\-based banning) [nargs=0..1] [پیش‌فرض: 1]
.TP
\fB\-\-polar\fR
{true,false,rnd,auto,stable} انتخاب حالت قطبیت (polarity). مقدار 'true' \-> هنگام انشعاب، فقط قطبیت مثبت را انتخاب می‌کند. 'false' \-> هنگام انشعاب، فقط قطبیت منفی را انتخاب می‌کند. 'auto' \-> آخرین قطبیت استفاده‌شده را انتخاب می‌کند (که با عنوان 'caching' نیز شناخته می‌شود) [nargs=0..1] [پیش‌فرض: "auto"]
.TP
\fB\-\-scc\fR
یافتن لیترال‌های معادل از طریق SCC (مؤلفه‌های قویاً همبند) و جایگزینی آن‌ها [nargs=0..1] [پیش‌فرض: 1]
.TP
\fB\-\-restart\fR
{geom, glue, luby} راهبرد راه‌اندازی مجدد (restart) برای دنبال کردن. [nargs=0..1] [پیش‌فرض: "auto"]
.TP
\fB\-\-rstfirst\fR
اندازه پایه راه‌اندازی مجدد [nargs=0..1] [پیش‌فرض: 100]
.TP
\fB\-\-gluehist\fR
اندازه پنجره متحرک برای تاریخچه کوتاه‌مدت glue بندهای زائد. هرچه بالاتر باشد، حداقل تعداد تعارض‌ها بین راه‌اندازی‌های مجدد بیشتر است [nargs=0..1] [پیش‌فرض: 50]
.TP
\fB\-\-lwrbndblkrest\fR
حد پایین برای راه‌اندازی مجدد مسدودکننده \fB\-\-\fR پیش از این تعداد تعارض مسدود نکن [nargs=0..1] [پیش‌فرض: 10000]
.TP
\fB\-\-locgmult\fR
ضریب مورد استفاده برای تعیین این‌که آیا باید در طول راه‌اندازی مجدد مبتنی بر glue، راه‌اندازی مجدد انجام گیرد یا خیر [nargs=0..1] [پیش‌فرض: 0.8]
.TP
\fB\-\-ratiogluegeom\fR
نسبت راه‌اندازی‌های مجدد glue به هندسی (geometric) \fB\-\-\fR مقدار بیشتر یعنی استفاده بیشتر از glue [nargs=0..1] [پیش‌فرض: 5]
.TP
\fB\-\-blockingglue\fR
انجام راه‌اندازی مجدد مسدودکننده برای مقادیر glue [nargs=0..1] [پیش‌فرض: 1]
.TP
\fB\-\-gluecut0\fR
مقدار glue برای برش سطح ۰ ('نگه‌داری') [nargs=0..1] [پیش‌فرض: 3]
.TP
\fB\-\-gluecut1\fR
مقدار glue برای برش سطح ۱ ('فرصت دوباره') [nargs=0..1] [پیش‌فرض: 6]
.TP
\fB\-\-adjustglue\fR
اگر بیش از این درصد از بندها دارای glue پایین (سطح ۰) باشند، حد آستانه glue را ۱ واحد کاهش بده \fB\-\-\fR یک‌بار و هرگز دوباره تکرار نشود [nargs=0..1] [پیش‌فرض: 0.7]
.TP
\fB\-\-everylev1\fR
کاهش بندهای سطح ۱ (lev1) در هر N گام [nargs=0..1] [پیش‌فرض: 10000]
.TP
\fB\-\-everylev2\fR
کاهش بندهای سطح ۲ (lev2) در هر N گام [nargs=0..1] [پیش‌فرض: 15000]
.TP
\fB\-\-lev1usewithin\fR
بند فراگرفته‌شده باید در این بازه زمانی در سطح ۱ استفاده شود، در غیر این صورت به سطح ۲ منتقل می‌شود [nargs=0..1] [پیش‌فرض: 70000]
.TP
\fB\-\-branchstr\fR
رشته راهبرد انشعاب که حین حل بین راهبردهای مختلف جابه‌جا می‌شود؛ مانند 'vsids1+vsids2' [nargs=0..1] [پیش‌فرض: "vmtf+vsids"]
.TP
\fB\-\-nobansol\fR
عدم ممنوع‌سازی راه‌حل پس از یافتن آن
.TP
\fB\-\-debuglib\fR
تجزیه یادداشت‌های (comments) ویژه برای اجرای solve/simplify حین تجزیه CNF
.TP
\fB\-\-breakid\fR
اجرای BreakID برای شکستن تقارن‌ها. [nargs=0..1] [پیش‌فرض: false]
.TP
\fB\-\-breakideveryn\fR
اجرای BreakID در هر N تکرارِ ساده‌سازی [nargs=0..1] [پیش‌فرض: 5]
.TP
\fB\-\-breakidmaxlits\fR
حداکثر تعداد لیترال‌ها به هزار. در صورت فراتر رفتن، BreakID اجرا نخواهد شد [nargs=0..1] [پیش‌فرض: 3500]
.TP
\fB\-\-breakidmaxcls\fR
حداکثر تعداد بندها به هزار. در صورت فراتر رفتن، BreakID اجرا نخواهد شد [nargs=0..1] [پیش‌فرض: 600]
.TP
\fB\-\-breakidmaxvars\fR
حداکثر تعداد متغیرها به هزار. در صورت فراتر رفتن، BreakID اجرا نخواهد شد [nargs=0..1] [پیش‌فرض: 300]
.TP
\fB\-\-breakidtime\fR
حداکثر تعداد گام‌های برداشته‌شده حین یافتن خودریختی (automorphism). [nargs=0..1] [پیش‌فرض: 2000]
.TP
\fB\-\-breakidcls\fR
حداکثر تعداد بندهای شکننده به ازای هر جایگشت. [nargs=0..1] [پیش‌فرض: 50]
.TP
\fB\-\-breakidmatrix\fR
تشخیص تعویض‌پذیری سطر ماتریس [nargs=0..1] [پیش‌فرض: true]
.TP
\fB\-\-sls\fR
اجرای SLS در طول ساده‌سازی [nargs=0..1] [پیش‌فرض: 1]
.TP
\fB\-\-slstype\fR
کدام SLS اجرا شود. مقادیر مجاز: walksat، yalsat، ccnr، ccnr_yalsat [nargs=0..1] [پیش‌فرض: "ccnr"]
.TP
\fB\-\-slsmaxmem\fR
حداکثر حافظه به مگابایت برای حل‌کننده SLS. اگر مصرف حافظه بیشتر از این مقدار باشد، حل‌کننده SLS را اجرا نمی‌کند. [nargs=0..1] [پیش‌فرض: 500]
.TP
\fB\-\-slseveryn\fR
اجرای حل‌کننده SLS فقط در هر N مرحله ساده‌سازی [nargs=0..1] [پیش‌فرض: 2]
.TP
\fB\-\-yalsatmems\fR
اجرای Yalsat با مهلت زمانی این مقدار میلیون دسترسی به حافظه (mems*million). زمان اجرای yalsat را محدود می‌کند [nargs=0..1] [پیش‌فرض: 10]
.TP
\fB\-\-walksatruns\fR
حداکثر 'اجراها' (runs) برای WalkSAT. زمان اجرای WalkSAT را محدود می‌کند [nargs=0..1] [پیش‌فرض: 50]
.TP
\fB\-\-slsgetphase\fR
دریافت فاز از حل‌کننده SLS و تنظیم آن به‌عنوان فاز جدید برای CDCL [nargs=0..1] [پیش‌فرض: 1]
.TP
\fB\-\-slsccnraspire\fR
فعال/غیرفعال کردن آرزومندی (aspiration) برای CCNR [nargs=0..1] [پیش‌فرض: 1]
.TP
\fB\-\-slstobump\fR
تعداد متغیرها جهت ارتقای فعالیت (bump) در CCNR [nargs=0..1] [پیش‌فرض: 100]
.TP
\fB\-\-slstobumpmaxpervar\fR
حداکثر دفعات ارتقای فعالیت یک متغیر مجزا در CCNR [nargs=0..1] [پیش‌فرض: 100]
.TP
\fB\-\-slsbumptype\fR
نحوه محاسبه متغیری که باید فعالیتش ارتقا یابد (bump). مقدار ۱ = مبتنی بر بند، ۲ = مبتنی بر وارون‌سازی متغیر، ۳ = مبتنی بر امتیاز متغیر [nargs=0..1] [پیش‌فرض: 6]
.TP
\fB\-\-transred\fR
حذف بندهای دوتایی بی‌فایده (کاهش متعدی یا transitive reduction) [nargs=0..1] [پیش‌فرض: 1]
.TP
\fB\-\-intree\fR
انجام کاوش بر پایه درخت درونی (intree\-based probing) [nargs=0..1] [پیش‌فرض: 1]
.TP
\fB\-\-intreemaxm\fR
زمان بر حسب mega\-bogoprops برای انجام کاوش درون‌درختی [nargs=0..1] [پیش‌فرض: 400]
.TP
\fB\-\-otfhyper\fR
انجام تفکیک فرادوتایی در حین کار (on-the-fly hyper-binary resolution) در طول کاوش [nargs=0..1] [پیش‌فرض: 1]
.TP
\fB\-\-schedsimp\fR
انجام دورهای ساده‌سازی. در صورت مقدار ۰، هیچ‌کدام انجام نمی‌شوند. [nargs=0..1] [پیش‌فرض: 1]
.TP
\fB\-\-presimp\fR
انجام ساده‌سازی در همان ابتدای کار [nargs=0..1] [پیش‌فرض: 0]
.TP
\fB\-\-allpresimp\fR
انجام ساده‌سازی در هر بار شروع \fB\-\-\fR فقط در حالت کتابخانه‌ای کاربرد دارد [nargs=0..1] [پیش‌فرض: 0]
.TP
\fB\-n\fR, \fB\-\-nonstop\fR
فرایند search() در کلاس SATSolver هرگز متوقف نشود [nargs=0..1] [پیش‌فرض: 0].TP
\fB\-\-maxnumsimppersolve\fR
حداکثر تعداد ساده‌سازی‌ها برای اجرا به ازای هر فراخوانی solve(). پس از این، دیگر هیچ پردازش حین حلی انجام نخواهد شد. [nargs=0..1] [پیش‌فرض: 25]
.TP
\fB\-\-schedule\fR
زمان‌بندی ساده‌سازی در طول اجرا
.TP
\fB\-\-preschedule\fR
زمان‌بندی ساده‌سازی هنگام راه‌اندازی
.TP
\fB\-\-occsimp\fR
انجام بهینه‌سازی‌های مبتنی بر فهرست رخدادها (حذف متغیر، شمول، افزودن متغیر محدودشده و...) [nargs=0..1] [پیش‌فرض: 1]
.TP
\fB\-\-confbtwsimp\fR
شروع نخستین ساده‌سازی پس از این تعداد تعارض [nargs=0..1] [پیش‌فرض: 40000]
.TP
\fB\-\-confbtwsimpinc\fR
افزایش دورهای ساده‌سازی با این توان از N [nargs=0..1] [پیش‌فرض: 1.4]
.TP
\fB\-\-tern\fR
انجام تفکیک سه‌تایی (Ternary resolution) [nargs=0..1] [پیش‌فرض: true]
.TP
\fB\-\-terntimelim\fR
مهلت زمانی بر حسب میلیون bogoprops برای تفکیک سه‌تایی مطابق با مقاله \(lqLook\-Ahead Versus Look\-Back for Satisfiability Problems\(rq [nargs=0..1] [پیش‌فرض: 100]
.TP
\fB\-\-ternkeep\fR
نگه‌داری بندهای تفکیک سه‌تایی تنها در صورتی که در این مضرب از \(lqlev1usewithin\(rq استفاده شوند [nargs=0..1] [پیش‌فرض: 5]
.TP
\fB\-\-terncreate\fR
ایجاد بندهای تفکیک سه‌تایی در هر دور ساده‌سازی، فقط تا این مضرب (از بندهای پیوندیافته) [nargs=0..1] [پیش‌فرض: 0.3]
.TP
\fB\-\-ternbincreate\fR
مجاز دانستن تفکیک سه‌تایی برای تولید بندهای دوتایی [nargs=0..1] [پیش‌فرض: 0]
.TP
\fB\-\-occredmax\fR
عدم افزودن بندهای زائد بزرگ‌تر از این مقدار به فهرست رخدادها [nargs=0..1] [پیش‌فرض: 50]
.TP
\fB\-\-occredmaxmb\fR
جلوگیری از فراتر رفتن اندازه رخدادهای زائد از این مقدار مگابایت [nargs=0..1] [پیش‌فرض: 600]
.TP
\fB\-\-occirredmaxmb\fR
جلوگیری از فراتر رفتن اندازه رخدادهای غیرزائد از این مقدار مگابایت [nargs=0..1] [پیش‌فرض: 2500]
.TP
\fB\-\-strengthen\fR
انجام انقباض بند از طریق تفکیک خودشمول به عنوان بخشی از سامانه رخداد-شمول [nargs=0..1] [پیش‌فرض: 1]
.TP
\fB\-\-weakentimelim\fR
مهلت زمانی بر حسب میلیون bogoprops برای تضعیف مورداستفاده [nargs=0..1] [پیش‌فرض: 300]
.TP
\fB\-\-substimelim\fR
مهلت زمانی بر حسب میلیون bogoprops برای شمول بندهای طولانی با بندهای طولانی، پس از محاسبه رخدادها [nargs=0..1] [پیش‌فرض: 300]
.TP
\fB\-\-substimelimbinratio\fR
نسبت محدودیت زمانی شمول برای صرف روی شمول و تقویت (sub&str) بندهای طولانی با بندهای دوتایی [nargs=0..1] [پیش‌فرض: 0.1]
.TP
\fB\-\-substimelimlongratio\fR
نسبت محدودیت زمانی شمول برای صرف روی شمول بندهای طولانی با بندهای طولانی [nargs=0..1] [پیش‌فرض: 0.9]
.TP
\fB\-\-strstimelim\fR
مهلت زمانی بر حسب میلیون bogoprops برای تقویت بندهای طولانی با بندهای طولانی، پس از محاسبه رخدادها [nargs=0..1] [پیش‌فرض: 300]
.TP
\fB\-\-sublonggothrough\fR
تعداد دفعات پیمایش فرایند شمول [nargs=0..1] [پیش‌فرض: 1]
.TP
\fB\-\-bva\fR
انجام افزودن متغیر محدودشده (BVA) [nargs=0..1] [پیش‌فرض: 0]
.TP
\fB\-\-bvaeveryn\fR
انجام BVA فقط به ازای هر N فراخوانی ساده‌سازی رخدادها [nargs=0..1] [پیش‌فرض: 7]
.TP
\fB\-\-bvalim\fR
حداکثر تعداد متغیرهای افزوده شده توسط BVA در هر فراخوانی [nargs=0..1] [پیش‌فرض: 250000]
.TP
\fB\-\-bva2lit\fR
انجام BVA با ترفند اختلاف ۲ لفظی نیز فعال باشد. هشدار: این کار اثربخشی اختلاف ۱ لفظی را کاهش می‌دهد [nargs=0..1] [پیش‌فرض: 1]
.TP
\fB\-\-bvato\fR
محدودیت زمانی BVA بر حسب میلیون bogoprops [nargs=0..1] [پیش‌فرض: 50]
.TP
\fB\-\-varelim\fR
انجام حذف متغیر بر اساس روش Een و Biere [nargs=0..1] [پیش‌فرض: 1]
.TP
\fB\-\-varelimto\fR
محدودیت زمانی حذف متغیر بر حسب میلیون bogoprops [nargs=0..1] [پیش‌فرض: 750]
.TP
\fB\-\-varelimover\fR
انجام BVE تا زمانی که افزایش حاصل در تعداد بندها کمتر از X باشد. تنها توان‌های ۲ معنادار هستند؛ مانند ۲، ۴، ۸ و... [nargs=0..1] [پیش‌فرض: 16]
.TP
\fB\-\-emptyelim\fR
انجام حذف حاصل‌تفکیک‌های خالی با استفاده از ترفند بیت‌مپ [nargs=0..1] [پیش‌فرض: 1]
.TP
\fB\-\-varelimmaxmb\fR
حداکثر حافظه اضافی بر حسب مگابایت برای استفاده در بندهای جدید هنگام varelim [nargs=0..1] [پیش‌فرض: 1000]
.TP
\fB\-\-eratio\fR
حذف حداکثر این نسبت از متغیرهای آزاد در هر دور از حذف متغیر [nargs=0..1] [پیش‌فرض: 1.6]
.TP
\fB\-\-varelimcheckres\fR
بررسی این که آیا حاصل‌تفکیک‌ها موارد دیگر را شمول می‌کنند یا خیر، و بررسی دقیق افزایش اندازه توسط BVE [nargs=0..1] [پیش‌فرض: 0]
.TP
\fB\-\-xor\fR
کشف XORهای طولانی [nargs=0..1] [پیش‌فرض: 1]
.TP
\fB\-\-maxxorsize\fR
حداکثر اندازه XOR برای یافتن [nargs=0..1] [پیش‌فرض: 7]
.TP
\fB\-\-xorfindtout\fR
محدودیت زمانی برای یافتن XORها [nargs=0..1] [پیش‌فرض: 400]
.TP
\fB\-\-maxxormat\fR
حداکثر اندازه ماتریس (=تعداد عناصر) که باید برای پلکانی کردن آن تلاش شود [nargs=0..1] [پیش‌فرض: 400]
.TP
\fB\-\-gates\fR
یافتن گیت‌ها. [nargs=0..1] [پیش‌فرض: 0]
.TP
\fB\-\-printgatedot\fR
چاپ منظم ساختار گیت در فایل \(lqgatesX.dot\(rq [nargs=0..1] [پیش‌فرض: 0]
.TP
\fB\-\-gatefindto\fR
حداکثر زمان بر حسب میلیون bogoprops برای یافتن گیت‌ها [nargs=0..1] [پیش‌فرض: 200]
.TP
\fB\-\-recur\fR
انجام کمینه‌سازی بازگشتی [nargs=0..1] [پیش‌فرض: 1]
.TP
\fB\-\-moreminim\fR
انجام کمینه‌سازی قوی هنگام تولید تعارض [nargs=0..1] [پیش‌فرض: 1]
.TP
\fB\-\-moremoreminim\fR
انجام کمینه‌سازی باز هم قوی‌تر هنگام تولید تعارض [nargs=0..1] [پیش‌فرض: 2]
.TP
\fB\-\-moremorealways\fR
همواره بندها به صورت قوی کمینه‌سازی شوند [nargs=0..1] [پیش‌فرض: 0]
.TP
\fB\-\-decbased\fR
ایجاد بندهای تعارض مبتنی بر تصمیم هنگامی که بند UIP بیش از حد بزرگ باشد [nargs=0..1] [پیش‌فرض: 1]
.TP
\fB\-\-updateglueonanalysis\fR
به‌روزرسانی مقادیر glue هنگام تحلیل [nargs=0..1] [پیش‌فرض: 1]
.TP
\fB\-\-maxgluehistltlimited\fR
حداکثر glue مورداستفاده در راهبرد بازراه‌اندازی مبتنی بر glue هنگام پر کردن تاریخچه glue. [nargs=0..1] [پیش‌فرض: 50]
.TP
\fB\-\-diffdeclevelchrono\fR
اگر اختلاف در سطح تصمیم‌گیری بیش از این مقدار باشد، پسگرد زمانی به جای پسگرد غیرزمانی انجام می‌شود. مقدار \fB\-1\fR به معنای عدم فعال‌سازی همیشگی آن است (در این حالت، \(lq\-\-confltochrono \fB\-1\fR\(rq نادیده گرفته می‌شود). [nargs=0..1] [پیش‌فرض: 20]
.TP
\fB\-\-verbstat\fR
تغییر میزان جزئیات آمار در پایان فرایند حل مسئله [0..3] [nargs=0..1] [پیش‌فرض: 2]
.TP
\fB\-\-verbrestart\fR
چاپ آمار دقیق‌تر، اما متفاوت [nargs=0..1] [پیش‌فرض: 0]
.TP
\fB\-\-verballrestarts\fR
چاپ یک خط به ازای هر بازراه‌اندازی [nargs=0..1] [پیش‌فرض: 0]
.TP
\fB\-s\fR, \fB\-\-printsol\fR
چاپ تخصیص متغیرها در صورتی که پاسخ SAT باشد [nargs=0..1] [پیش‌فرض: 1]
.TP
\fB\-\-restartprint\fR
چاپ خطوط وضعیت بازراه‌اندازی دست‌کم به ازای هر N تعارض [nargs=0..1] [پیش‌فرض: 8192]
.TP
\fB\-\-distill\fR
اجرای منظم تقطیر بندها [nargs=0..1] [پیش‌فرض: 1]
.TP
\fB\-\-distillbin\fR
اجرای منظم تقطیر بندهای دوتایی [nargs=0..1] [پیش‌فرض: 1]
.TP
\fB\-\-distillmaxm\fR
حداکثر تعداد مگا\-bogoprops (حدوداً معادل زمان) برای صرف روی حیات‌بخشی/تقطیر بندهای طولانی از طریق صف‌بندی و انتشار [nargs=0..1] [پیش‌فرض: 200]
.TP
\fB\-\-distillincconf\fR
ضریب تعداد فعلی تعارض‌ها در تقطیر بلادرنگ (OTF distill) [nargs=0..1] [پیش‌فرض: 0.1]
.TP
\fB\-\-distillminconf\fR
حداقل تعداد تعارض‌ها میان تقطیرهای بلادرنگ [nargs=0..1] [پیش‌فرض: 10000]
.TP
\fB\-\-distilltier0ratio\fR
میزان تقطیر رده ۰ [nargs=0..1] [پیش‌فرض: 10]
.TP
\fB\-\-distilltier1ratio\fR
میزان تقطیر رده ۱ [nargs=0..1] [پیش‌فرض: 0.03].TP
\fB\-\-distillirredalsoremratio\fR
چه میزانی از irred در هنگام انجام حذف (removal) نیز تقطیر شود [nargs=0..1] [پیش‌فرض: 1.2]
.TP
\fB\-\-distillirrednoremratio\fR
چه میزانی از irred در صورت عدم انجام حذف تقطیر شود [nargs=0..1] [پیش‌فرض: 1]
.TP
\fB\-\-distillshuffleeveryn\fR
بُر زدن تصادفی بندهای در شرف تقطیر هر N مورد یک‌بار [nargs=0..1] [پیش‌فرض: 3]
.TP
\fB\-\-distillsort\fR
نوع مرتب‌سازی تقطیر [nargs=0..1] [پیش‌فرض: 1]
.TP
\fB\-\-renumber\fR
شماره‌گذاری مجدد متغیرها برای افزایش کارایی حافظه نهان (کش) پردازنده [nargs=0..1] [پیش‌فرض: 1]
.TP
\fB\-\-mustconsolidate\fR
تجمیع همیشگی، حتی اگر مفید نباشد. این گزینه فقط برای اشکال‌زدایی استفاده می‌شود [nargs=0..1] [پیش‌فرض: 0]
.TP
\fB\-\-savemem\fR
صرفه‌جویی در حافظه با آزادسازی فضای متغیرها پس از شماره‌گذاری مجدد. فقط در صورت فعال بودن شماره‌گذاری مجدد کار می‌کند. [nargs=0..1] [پیش‌فرض: 1]
.TP
\fB\-\-mustrenumber\fR
در نظر گرفتن تمام راهبردهای 'renumber' به عنوان 'must\-renumber' [nargs=0..1] [پیش‌فرض: 0]
.TP
\fB\-\-fullwatchconseveryn\fR
تجمیع کامل فهرست‌های دیده‌بانی (watchlists) هر N تداخل یک‌بار. در طول دورهای ساده‌سازی زمان‌بندی می‌شود. [nargs=0..1] [پیش‌فرض: 4000000]
.TP
\fB\-\-strmaxt\fR
حداکثر MBP قابل مصرف برای تقطیر بندهای طولانی irred از طریق دیده‌بان‌ها [nargs=0..1] [پیش‌فرض: 20]
.TP
\fB\-\-implicitmanip\fR
شمول (subsume) و تقویت بندهای ضمنی با یکدیگر [nargs=0..1] [پیش‌فرض: 1]
.TP
\fB\-\-implsubsto\fR
مهلت زمانی (به میلیون bogoprop) برای شمول ضمنی [nargs=0..1] [پیش‌فرض: 100]
.TP
\fB\-\-implstrto\fR
مهلت زمانی (به میلیون bogoprop) برای تقویت ضمنی [nargs=0..1] [پیش‌فرض: 200]
.TP
\fB\-\-cardfind\fR
یافتن محدودیت‌های عدد اصلی (cardinality constraints) [nargs=0..1] [پیش‌فرض: 0]
.TP
\fB\-\-sync\fR
همگام‌سازی رشته‌ها (threads) هر N تداخل یک‌بار [nargs=0..1] [پیش‌فرض: 7000]
.TP
\fB\-\-clearinter\fR
قطع رشته‌ها به صورت تمیز در تمام مدت [nargs=0..1] [پیش‌فرض: 0]
.TP
\fB\-\-zero\-exit\-status\fR
خروج با وضعیت صفر در صورتی که حل مسئله بدون مشکل به پایان رسیده باشد
.TP
\fB\-\-printtimes\fR
چاپ زمان صرف‌شده برای هر اجرای ساده‌سازی. در صورت تنظیم روی 0، مقایسه لاگ‌ها آسان‌تر خواهد بود [nargs=0..1] [پیش‌فرض: 1]
.TP
\fB\-\-maxsccdepth\fR
حداکثر عمق جستجوی scc [nargs=0..1] [پیش‌فرض: 10000]
.TP
\fB\-\-sampling\fR
تنظیم متغیرهای نمونه‌برداری مانند '1,84,44'. همچنین از طریق CNF با استفاده از 'c p show 1 84 44 0' قابل تنظیم است
.TP
\fB\-\-assump\fR
فایل فرضیات [nargs=0..1] [پیش‌فرض: ""]
.TP
\fB\-\-maxmatrixrows\fR
تنظیم حداکثر تعداد ردیف‌ها برای ماتریس گاوسی. ماتریس‌های بیش از حد بزرگ باید به دلایل کارایی کنار گذاشته شوند [nargs=0..1] [پیش‌فرض: 2000]
.TP
\fB\-\-maxmatrixcols\fR
تنظیم حداکثر تعداد ستون‌ها برای ماتریس گاوسی. ماتریس‌های بیش از حد بزرگ باید به دلایل کارایی کنار گذاشته شوند [nargs=0..1] [پیش‌فرض: 1000]
.TP
\fB\-\-autodisablegauss\fR
غیرفعال‌سازی خودکار گاوس هنگامی که کارایی نامطلوبی دارد [nargs=0..1] [پیش‌فرض: true]
.TP
\fB\-\-minmatrixrows\fR
تنظیم حداقل تعداد ردیف‌ها برای ماتریس گاوسی. معمولاً ماتریس‌های بیش از حد کوچک به دلایل کارایی کنار گذاشته می‌شوند [nargs=0..1] [پیش‌فرض: 3]
.TP
\fB\-\-maxnummatrices\fR
حداکثر تعداد ماتریس‌ها برای پردازش. [nargs=0..1] [پیش‌فرض: 5]
.TP
\fB\-\-gaussusefulcutoff\fR
غیرفعال‌سازی گاوس در صورتی که نسبت سودمندی کمتر از این مقدار ثبت شود [nargs=0..1] [پیش‌فرض: 0.2]
.TP
\fB\-\-dumpresult\fR
نوشتن راه‌حل(ها) در این فایل.SH "همچنین ببینید (SEE ALSO)"
مستندات کامل
.B cryptominisat5
به‌صورت یک راهنمای Texinfo نگهداری می‌شود. اگر برنامه‌های
.B info
و
.B cryptominisat5
به‌درستی روی سیستم شما نصب شده باشند، دستور
.IP
.B info cryptominisat5
.PP
باید دسترسی به راهنمای کامل را فراهم کند.