minisat -V (return code: 10)
WARNING: for repeatability, setting FPU to use double precision
============================[ Problem Statistics ]=============================
| |
| Number of variables: 0 |
| Number of clauses: 0 |
| Parse time: 0.00 s |
| Simplification time: 0.00 s |
| |
============================[ Search Statistics ]==============================
| Conflicts | ORIGINAL | LEARNT | Progress |
| | Vars Clauses Literals | Limit Clauses Lit/Cl | |
===============================================================================
===============================================================================
restarts : 1
conflicts : 0 (-nan /sec)
decisions : 1 (0.00 % random) (inf /sec)
propagations : 0 (-nan /sec)
conflict literals : 0 (-nan % deleted)
Memory used : 22.00 MB
CPU time : 0 s
SATISFIABLE
minisat --help (return code: 0)
USAGE: minisat [options] <input-file> <result-output-file>
where input may be either in plain or gzipped DIMACS.
CORE OPTIONS:
-rnd-init, -no-rnd-init (default: off)
-luby, -no-luby (default: on)
-rnd-freq = <double> [ 0 .. 1] (default: 0)
-rnd-seed = <double> ( 0 .. inf) (default: 9.16483e+07)
-gc-frac = <double> ( 0 .. inf) (default: 0.2)
-rinc = <double> ( 1 .. inf) (default: 2)
-var-decay = <double> ( 0 .. 1) (default: 0.95)
-cla-decay = <double> ( 0 .. 1) (default: 0.999)
-rfirst = <int32> [ 1 .. imax] (default: 100)
-phase-saving = <int32> [ 0 .. 2] (default: 2)
-ccmin-mode = <int32> [ 0 .. 2] (default: 2)
MAIN OPTIONS:
-pre, -no-pre (default: on)
-cpu-lim = <int32> [ 0 .. imax] (default: 2147483647)
-mem-lim = <int32> [ 64 .. imax] (default: 2147483647)
-verb = <int32> [ 0 .. 2] (default: 1)
-dimacs = <string>
SIMP OPTIONS:
-elim, -no-elim (default: on)
-rcheck, -no-rcheck (default: off)
-asymm, -no-asymm (default: off)
-simp-gc-frac = <double> ( 0 .. inf) (default: 0.5)
-sub-lim = <int32> [ -1 .. imax] (default: 1000)
-grow = <int32> [imin .. imax] (default: 0)
-cl-lim = <int32> [ -1 .. imax] (default: 20)
HELP OPTIONS:
--help Print help message.
--help-verb Print verbose help message.
WARNING: for repeatability, setting FPU to use double precision