diff options
Diffstat (limited to 'src/prop/cryptominisat/man/cryptominisat.1')
| -rw-r--r-- | src/prop/cryptominisat/man/cryptominisat.1 | 228 |
1 files changed, 0 insertions, 228 deletions
diff --git a/src/prop/cryptominisat/man/cryptominisat.1 b/src/prop/cryptominisat/man/cryptominisat.1 deleted file mode 100644 index 2fffa82e8..000000000 --- a/src/prop/cryptominisat/man/cryptominisat.1 +++ /dev/null @@ -1,228 +0,0 @@ -.TH "CRYPTOMINISAT" "1" "@VERSION@" "Mate Soos" "User Commands" -.SH "NAME" -cryptominisat \- conflict-driven SAT solver -.SH "SYNOPSIS" -.B cryptominisat -[\fIOPTIONS\fP] <\fIinput\-file\fP> <\fIoutput\-file\fP> -.SH "DESCRIPTION" -.PP -CryptoMiniSat is a SAT solver, solving problems given in CNF, or conjunctive -normal form. CryptoMiniSat retains much of the API of MiniSat, but -offers more versatility and better speed on many problems. - -The program is a classical conflict-driven solver, with variable activities, -clause learning and clause deletion. It however incorporates a number of -advanced CNF simplification functionalities which should help the speed of -solving. Further, it incorporates some advanced memory-management features -that should help in getting the most out of modern CPU caches. - -The input format is that of DIMACS CNF, i.e. a header of the form - -p cnf VARS CLAUSES - -where VARS is the number of variables, and CLAUSES is the number of clauses in -the problem. It then lists the set of clauses such as: - -1 -2 0 - -which is equivalent to the 2-long clause "v1 OR NOT v2 = TRUE" - -.SH "OPTIONS" -.TP -\fB\-\-polarity\-mode\fP = \fI{true,false,rnd,auto}\fP [default: auto] -Selects the polarity mode. Auto is the Jeroslow&Wang method. -.TP -\fB\-\-rnd\-freq\fP = <\fInum\fP> [0-1] How often should decision variables -be picked randomly. -.TP -\fB\-\-verbosity\fP = <\fInum\fP> [0-2] Verbosity 1 is default. Verbosity 0 -only prints the results, and verbosity 2 prints many useful debug info. -.TP -\fB\-\-randomize\fP = <\fIseed\fP> [0 - 2^32-1] -Sets the random seed, used for picking decision variables (default = 0). -.TP -\fB\-\-restrict\fP = <\fInum\fP> [1 - varnum] -When picking random variables to branch on, pick one that is in the \fInum\fP -most active vars useful for cryptographic problems, where the question is the -key, which is usually small (e.g., 80 bits). -.TP -\fB\-\-gaussuntil\fP = <\fInum\fP> -Depth until which Gaussian elimination is active. Giving 0 switches off -Gaussian elimination. -.TP -\fB\-\-restarts\fP = <\fInum\fP> [1 - 2^32-1] -No more than the given number of restarts will be performed during search. -.TP -\fB\-\-nonormxorfind\fP -Don't find and collect >2-long xor-clauses from regular clauses. -.TP -\fB\-\-nobinxorfind\fP -Don't find and collect 2-long xor-clauses from regular clauses. -.TP -\fB\-\-noregbxorfind\fP -Don't regularly find and collect 2-long xor-clauses from regular clauses. -.TP -\fB\-\-doextendedscc\fP -Do strongly connected component finding using non-existent binary clauses. -Makes binary XOR findig slower, but somewhat more accurate. -.TP -\fB\-\-noconglomerate\fP -Don't conglomerate 2 xor clauses when one var is dependent. This allows for -elimination of variable y if it is only in the two XOR clauses "y XOR a XOR b" and -"y XOR c XOR d" -.TP -\fB\-\-nosimplify\fP -Don't do regular simplification rounds. These simplification rounds greatly -simplify the CNF, but cost time. If your problem is very small, it may be -only a waste of time to execute these simplification rounds. Typically, however, -these simplification methods save significant amount of time (>60%) -.TP -\fB\-\-greedyunbound\fP -Greedily unbound variables that are not needed for the final satisfying -assignement. -.TP -\fB\-\-debuglib\fP -Solve at specific \fBc Solver::solve()\fP points in the CNF file. Used to -debug file generated by Solver's \fBneedLibraryCNFFile()\fP function. -.TP -\fB\-\-debugnewvar\fP -Add new vars at specific \fBc Solver::newVar()\fP points in the CNF file. -Used to debug file generated by Solver's \fBneedLibraryCNFFile()\fP function. -.TP -\fB\-\-novarreplace\fP -Don't perform variable replacement. Needed for programmable solver feature. -.TP -\fB\-\-restart\fP = \fI{auto, static, dynamic}\fP -Which kind of restart strategy to follow. Default is \fIauto\fP. -.TP -\fB\-\-dumplearnts\fP = <\fIfilename\fP> -If interrupted or reached restart limit, dump the learnt clauses to the -specified file. Maximum size of dumped clauses can be specified with the -\fB\-\-maxdumplearnts\fP option. -.TP -\fB\-\-maxdumplearnts\fP = [0 - 2^32-1] -When dumping the learnts to file, what should be maximum length of the clause -dumped. Useful to make the resulting file smaller. Default is 2^32-1. Note: -2-long XORs are always dumped. -.TP -\fB\-\-dumporig\fP = <\fIfilename\fP> -If interrupted or reached restart limit, dump the original problem instance, -simplified to the current point. -.TP -\fB\-\-alsoread\fP = <\fIfilename\fP> -Also read this file in. Can be used to re-read dumped learnts, for example. -.TP -\fB\-\-maxsolutions\fP = <\fInum\fP> -Search for given amount of solutions. Can only be used in single-threaded -mode (\fB--threads=1\fP). -.TP -\fB\-\-pavgbranch\fP -Print average branch depth. -.TP -\fB\-\-nofailedlit\fP -Don't search for failed literals, and don't search for literals propagated -both by \fIvarX\fP and \fI-varX\fP. -.TP -\fB\-\-noheuleprocess\fP -Don't try to minimise XORs by XOR-ing them together. Algorithm as per -global/local substitution in Heule's thesis. -.TP -\fB\-\-nosatelite\fP -Don't do clause subsumption, clause strengthening and variable elimination -(implies \fB\-\-novarelim\fP and \fB\-\-nosubsume1\fP). -.TP -\fB\-\-noxorsubs\fP -Don't try to subsume xor-clauses. -.TP -\fB\-\-nosolprint\fP -Don't print the satisfying assignment if the solution is SAT. -.TP -\fB\-\-novarelim\fP -Don't perform variable elimination as per Een and Biere. -.TP -\fB\-\-nosubsume1\fP -Don't perform clause contraction through resolution. -.TP -\fB\-\-noparthandler\fP -Don't find and solve subroblems with subsolvers. -.TP -\fB\-\-nomatrixfind\fP -Don't find distinct matrixes. Put all xors into one big matrix. -.TP -\fB\-\-noordercol\fP -Don't order variables in the columns of Gaussian elimination. Effectively -disables iterative reduction of the matrix. -.TP -\fB\-\-noiterreduce\fP -Don't reduce iteratively the matrix that is updated. -.TP -\fB\-\-maxmatrixrows\fP = [0 - 2^32-1] -Set maximum number of rows for gaussian matrix. Too large matrixes should be -discarded for reasons of efficiency. Default: 1000. -.TP -\fB\-\-minmatrixrows\fP = [0 - 2^32-1] -Set minimum number of rows for gaussian matrix. Normally, too small matrixes -are discarded for reasons of efficiency. Default: 20. -.TP -\fB\-\-savematrix\fP = [0 - 2^32-1] -Save matrix every Nth decision level. Default: 2. -.TP -\fB\-\-maxnummatrixes\fP = [0 - 2^32-1] -Maximum number of matrixes to treat. Default: 3. -.TP -\fB\-\-nohyperbinres\fP -Don't add binary clauses when doing failed lit probing. -.TP -\fB\-\-noremovebins\fP -Don't remove useless binary clauses. -.TP -\fB\-\-noremlbins\fP -Don't remove useless learnt binary clauses. -.TP -\fB\-\-nosubswithbins\fP -Don't subsume with binary clauses. -.TP -\fB\-\-nosubswithnbins\fP -Don't subsume with non-existent binary clauses. -.TP -\fB\-\-noclausevivif\fP -Don't perform clause vivification. -.TP -\fB\-\-nosortwatched\fP -Don't sort watches according to size: bin, tri, etc. -.TP -\fB\-\-nolfminim\fP -Don't do on-the-fly self-subsuming resolution (called 'strong minimisation' in -PrecoSat). -.TP -\fB\-\-nocalcreach\fP -Don't calculate reachability and interfere with variable decisions accordingly. -.TP -\fB\-\-nobxor\fP -Don't find equivalent literals during failed literal search. -.TP -\fB\-\-norecotfssr\fP -Don't perform recursive/transitive OTF self-subsuming resolution. -.TP -\fB\-\-nocacheotfssr\fP -Don't cache 1-level equeue. Less memory used, but disables trans OTFSSR, -adv. clause vivifier, etc. Throw the clause away on backtrack. -.TP -\fB\-\-threads\fP = <\fInum\fP> -Number of threads (default is 1). -.SH "EXIT STATUS" -.PP -The output is a solution, together with some timing information. -The exit status indicates the following: -.IP 10 -The problem is satisfiable. -.IP 15 -The problem's satisfiability was not determined. -.IP 20 -The problem is unsatisfiable. -.SH AUTHOR -Mate Soos (soos@srlabs.de) -.SH "SEE ALSO" -The DIMACS input format can be looked up here: - -http://www.satcompetition.org/2009/format-benchmarks2009.html |