Usage: vallst [file] [options]
Solve the specified boolean constraint problem (or tsp).
Options, with defaults in [ ]:
For more on what the options mean, see the documentation of vallstAPI.h.
--abort-threshold <non-negative integer>
Search will abort if at least this many vars are
set, to truthvalue or to other equ-class. Search
will also abort if fewer vars are set but more
time has passed. [4294901496]
--atsp[=no|yes] Indicate if the input file is on atsp format. [no]
--breadth-fst-opt-strat[=no|yes]
Set optimization strategy. No arg means yes. [yes]
--buffer-reset-frequency <positive integer>
Set frequency. [4]
--buffer-size-const <value>
Set value. [24000]
--buffer-size-non-ax-dep <value>
Set value. [3.4]
--buffer-size-var-dep <value>
Set value. [3.8]
--cc-leeway <leeway> Set proof improvement leeway. [1.001]
--char-prefix-pb-var Yes means that pb variables are on the form
<char><positive_integer>. [no]
--changing-setting-file-name <file>
The changing setting will be printed to this file
at time-out and interupt. 'NULL' means no string.
Also sets print-changing-setting flag to 'yes' if
file is not NULL. - means stdout.
[vallst_changing_setting.options]
--complete-model[=no|yes]
Set flag. Determines if partial models will be
printed as complete. [no]
--convert-3-clauses[=no|yes]
Set flag. No argument means yes. [yes]
--create-phantom-conflict-clauses[=no|yes]
Set flag. No argument means yes. [no]
-f --file <file> Specify the in-theory file. - means stdin. [stdin]
If missing, the first non-option, if any, is used.
--first-restart <positive integer>
Set initial/base restart. [80]
--fst-nr-of-levels-alloc-size <size>
Set size. [2500]
--good-clause-size <positive integer>
Set what's to be considered good. [5]
--good-level <positive integer>
Set what's to be considered good. [5]
--help Print this message.
--heuristic-axiom-size <size>
Set size; 'inf' is acceptable. [inf (4294967295)]
--ignore-prologue[=no|yes]
Set flag. No argument means yes. [yes]
--improve-proof-level [=unsigned integer]
Set level. No arg means inf. 'inf' is acceptable.
0 will turn proof improvements off. [4294967295]
--keep-aboves[=no|yes] Set flag. No argument means yes. [no]
--keep-cc-meta-meta-threshold <threshold>
Set threshold. [3]
--keep-conflict-clause-length-threshold <threshold>
Set threshold. [50]
--loose-theory-meta-size-leeway <float>
Set meta value. [4.1]
--loose-theory-size-leeway <float>
Set meta meta value. [2.5]
--loose-theory-size-leeway-keep <float>
Set value. [6.5]
--loose-time-limit-base <unsigned int>
Set mode limit parameter (millisecs). [180000]
--loose-time-limit-mod <unsigned int>
Set mode limit parameter. [18]
--make-search-assumption [-]<variable>
Make a search assumption, using DIMACS format.
--max-hash-load <value> Set max load. [0.85]
--max-skipped-simps <value>
Set max skipped search simplifications. [0]
--meta-meta-prune-end <endPoint>
Set value. 'inf' is acceptable. [14]
--meta-meta-prune-frequency <positive integer>
Set frequency. [96]
--meta-meta-prune-start <startPoint>
Set value. [9]
--meta-prune-end <endPoint>
Set value. 'inf' is acceptable. [inf (4294967295)]
--meta-prune-frequency <positive integer>
Set frequency. [16]
--meta-prune-start <startPoint>
Set value. [30]
--next-batch-size-const <value>
Set value. Negative value is acceptable. [0.25]
--no-abort-time <secs> Given that enough vars are set, search will not
abort until secs seconds have passed. [240]
--non-axiom-chunk-size-ax-dep <value>
Set value. [0.5]
--non-axiom-chunk-size-const <value>
Set value. [2400]
--non-axiom-chunk-size-var-dep <value>
Set value. [1.4]
--nr-of-3-clauses <nrOf3Clauses>
Set the number of ternary clauses estimate.
--nr-of-free-chunks-cap <cap>
Set cap. [3]
--nr-of-literal-occs <nrOfLitOccs>
Set the number of literal occurrences estimate.
--nr-of-vars-set-at-start-is-zero[=no|yes]
Set flag indicating if set vars at start haven't
been handled already. Set it to false if you are
doing a restart, otherwise to true. [yes]
-o --result-file <file> Specify the result file where models are printed.
Will also set the print-model verbosity vector
flag to true. - means stdout. [stdout]
--out-theory-file-name <file>
The theory will be printed to this file at time-out
and interupt. 'NULL' means no string. Also sets
print-out-theory flag to 'yes' if file is not NULL.
- means stdout. [vallst_out_theory.vnf]
--pb[=no|yes] Indicate if the input file is on (restricted)
(o)pb format. No arg means yes. [no]
--positive-heur-ax-sign[=no|yes]
Set branching flag. No argument means yes. [yes]
--positive-sign[=no|yes]
Set branching flag. No argument means yes. [yes]
--print-changing-setting[=no|yes]
Set flag determining if the changing setting will
be printed at time-out and interupt. [yes]
--print-options Print option settings and then quit.
E.g., to fine-tune the verbosity, run e.g.
'./vallst -v30 --print-options' and then tune the
printed verbosity vector.
--print-out-theory[=no|yes]
The theory will be printed at time-out and
interupt. [yes]
-q --quiet --silent Run silently; only print error messages.
--random-branch-sign-prob <prob>
Set value. The sign of branching literals will be
chosen randomly with probability <prob>/1000. [200]
--random-formula-lit-prob <prob>
Set value. A literal from a formula will be chosen
randomly with probability <prob>/1000. [999]
--remove-tmp-causes[=no|yes]
Set flag. No argument means yes. [yes]
--reset-buffers-between-searches[=no|yes]
Set flag. No argument means yes. [yes]
--restart-func <0|1> Set function. 0 means Luby strategy. 1 means
incrementing with next-batch-size-const. [1]
--restart-prolong-cap <cap>
Set restart batch prolong cap. [5.9]
--restart-start <size>
Set start phase size. [0]
-s --seed <seed> Set the seed. [current time]
--simp-setting <level>-<sublevel>-<nrOfVars>-<nrOfIterations>
Set setting. Note that the numbers must be
separated by '-' with no space in between.
--simp-setting-slow <level>-<sublevel>-<nrOfVars>-<nrOfIterations>
Similar to --simp-setting but used less frequently.
--simp-time-limit-fast <millisecs>
Set time limit for fast simplifications. [1800]
--simp-time-limit-slow <millisecs>
Set time limit for slow simplifications. [16000]
--start-const <unsigned integer>
The main constant to start with in (a)tsp. [sum-1]
--start-with-bin-fst-bcp[=no|yes]
Set flag. No argument means yes. [no]
--strength-leeway Set the heuristic strength leeway. [1.3]
--strength-leeway-formula
Set the heuristic strength leeway for formulas.[1.8]
--strength-leeway-size Set a cap of the strength leeway space size. [256]
--strength-leeway-size-formula
Set cap of str leeway space for formulas. [256]
--subst-equs[=no|yes] Set flag. No argument means yes. [yes]
-t --time-limit <sec> Set the time limit in seconds. [inf]
--tight-cc-leeway <leeway>
Set tight proof improvement leeway. [1.0001]
--tight-keep-cc-threshold <unsigned integer>
Set value used in tight mode. [23]
--tight-meta-meta-prune-end <unsigned integer>
Set value used in tight mode. [9]
--tight-meta-meta-prune-start <unsigned integer>
Set value used in tight mode. [6]
--tight-meta-prune-start <unsigned integer>
Set value used in tight mode. [12]
--tight-theory-meta-size-leeway <float>
Set meta value. [3.1]
--tight-theory-size-leeway <float>
Set meta meta value. [1.4]
--tight-theory-size-leeway-keep <float>
Set value. [5.4]
--tight-time-limit-base <unsigned int>
Set mode limit parameter (millisecs). [180000]
--tight-time-limit-mod <unsigned int>
Set mode limit parameter. [20]
--time-limit-in-millisec <millisec>
Set the time limit in milliseconds. [inf]
--tsp[=no|yes] Indicate if the input file is on tsp format. [no]
--use-doppelganger[=no|yes]
Set flag. No argument means yes. [yes]
-v --verbose [level] Set verbosity level (0-99). No arg means 80. [40]
--var-map-file-name <file>
Set file name for (pb) variable mapping (or prefix
character). [vallst_var_map]
--verbosity-vector <unsigned integer>
Set the verbosity vector. [0xa07ef]
The integer can be bin (0b), hex (0x), octal (0) or
plain decimal.
--version Print the version number.
For more on what the options mean, see the documentation of vallstAPI.h.
Vallst is open source licensed under the Reciprocal Public License,
version 1.1; Copyright (C) 2004-2005 Daniel Vallstrom.
Send bug reports, feedback, etc. to vallst@gmail.com.
Generated on Mon Jul 18 11:34:15 2005 for Vallst by doxygen 1.4.3.