Command Line Options ==================== Minion supports a number of switches to augment default behaviour, these are listed here. We begin with the most useful, and then list other, less common flags. Choosing how much search to perform (time, number of solutions) --------------------------------------------------------------- -nodelimit ~~~~~~~~~~~~~~~~~~~~~~ To stop search after N nodes: -sollimit ~~~~~~~~~~~~~~~~~~~~~ To stop search after N solutions have been found: -timelimit ~~~~~~~~~~~~~~~~~~~~~~ To stop search after N seconds (real time): -cpulimit ~~~~~~~~~~~~~~~~~~~~~ To stop search after N seconds (CPU time): -findallsols ~~~~~~~~~~~~~~~~~~~~~~~~ Find all solutions and count them. This option is ignored if the problem contains any minimising or maximising objective. Control search --------------------------------------------------------------- -parallel ~~~~~~~~~~~~~~~~~~~~~ Make Minion run in parallel. When using this option, you should use `-solsout` to put the solutions in a file, as solutions may get mixed up on the terminal. -cores ~~~~~~~~~~~~~~~~~~~~~~ Number of cores to use when running in parallel -steallow ~~~~~~~~~~~~~~~~~~~~ When doing parallel search, "steal low" in the tree (that is, start new threads from low pieces of the tree) instead of "steal high" (default, take high bits of the tree). Is usually slower. -varorder ~~~~~~~~~~~~~~~~~~~~~ Enable a particular variable ordering for the search process. The available orders are: - sdf - smallest domain first, break ties lexicographically - sdf-random - sdf, but break ties randomly - srf - smallest ratio first, chooses unassigned variable with smallest percentage of its initial values remaining, break ties lexicographically - srf-random - srf, but break ties randomly - ldf - largest domain first, break ties lexicographically - ldf-random - ldf, but break ties randomly - random - random variable ordering - conflict - conflict-directed variable ordering - static - lexicographical ordering - wdeg - Weighted degree - domoverwdeg - Domain size over weighted degree -valorder ~~~~~~~~~~~~~~~~~~~~~ Choose the value ordering (overruling any selection in the input file). Current orders are, ascend, descend and random. -restarts ~~~~~~~~~ Enable restart-based search. When enabled, Minion restarts the search from the top of the search tree periodically, retaining learned information. -restarts-multiplier ~~~~~~~~~~~~~~~~~~~~~~~~ Set the restart multiplier. The restart schedule is geometric: the first restart occurs after 10 conflicts, and each subsequent restart occurs after the previous limit multiplied by this value. Default is 1.5. -no-restarts-bias ~~~~~~~~~~~~~~~~~ Disable the restart bias heuristic. By default, Minion biases the restart schedule based on the number of variables. -prop-node ~~~~~~~~~~~~~~~~~~~~~~ Allows the user to choose the level of consistency to be enforced during each node of search. See -preprocess for the allowed values for `` -preprocess ~~~~~~~~~~~~~~~~~~~~~~~ This switch allows the user to choose what level of preprocess is applied to their model before search commences. The default level is "GAC" The choices are: - GAC - Default setting - All propagators are run to a fixed point - Incorrectly named (but kept for historical reasons), because some propagators do not achieve GAC. - Used as the basis for all other, better, levels below. - SACBounds - singleton arc consistency on the upper and lower bounds of each variable - GAC is run on every assignment to the upper and lower bound of each variable - SAC - singleton arc consistency - GAC is run on every assignment to every variable - SSACBounds - singleton singleton bounds arc consistency - SAC is run on every assignment to the upper and lower bound of each variable - SSAC - singleton singleton arc consistency - SAC is run on every assignment to every variable These are listed in order of roughly how long they take to achieve. Preprocessing is a one off cost at the start of search. The success of higher levels of preprocessing is problem specific; SAC preprocesses may take a long time to complete, but may reduce search time enough to justify the cost. Each of the SAC variants can have '_limit' added (for example SACBound_limit). The '_limit' variants of these algorithm add checks which limit the algorithms if they are taking a very long time and not making progress. -randomseed ~~~~~~~~~~~~~~~~~~~~~~~ Set the pseudorandom seed to N. This allows 'random' behaviour to be repeated in different runs of minion. Control output --------------------------------------------------------------- -quiet ~~~~~~~~~~~~~~~~~~ Do not print parser progress (default) -verbose ~~~~~~~~~~~~~~~~~~~~ Print parser progress -printsols ~~~~~~~~~~~~~~~~~~~~~~ Print solutions (default). -noprintsols ~~~~~~~~~~~~~~~~~~~~~~~~ Do not print solutions. -printsolsonly ~~~~~~~~~~~~~~~~~~~~~~~~~~ Print only solutions and a summary at the end. -printonlyoptimal ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ In optimisation problems, only print the optimal value, and not intermediate values. -tableout ~~~~~~~~~~~~~~~~~~~~~ Append a line of data about the current run of minion to a named file. This data includes minion version information, arguments to the executable, build and solve time statistics, etc. See the file itself for a precise schema of the supplied information. -jsontableout ~~~~~~~~~~~~~~~~~~~~~~~~ Append a line of data about the current run as JSON to a named file. Contains the same information as ``-tableout``, but formatted as a JSON object. -solsout ~~~~~~~~~~~~~~~~~~~~ Append all solutionsto a named file. Each solution is placed on a line, with no extra formatting. Less common flags ----------------- -outputCompressedDomains ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Try to reduce the initial domains of variables, and output them. This is in general not useful for users, but is provided as a pre-preprocessing step for other systems. -outputCompressed ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Output a Minion instance with some basic reasoning performed to reduce the size of the file, such as reducing domain size. This file should produce identical output the original instance but may solve faster. -redump ~~~~~~~~~~~~~~~~~~~ Print the minion input instance file to standard out. No search is carried out when this switch is used. This can be used to update files in old versions of the Minion file format. -instancestats ~~~~~~~~~~~~~~~~~~~~~~~~~~ Output various statistics about the minion file, which can be used for machine learning. -map-long-short ~~~~~~~~~~~~~~~~~~~~~~~~~~~ Automatically generate a short tuple list from each long tuple list. The methods of compression are: - none : No short tuple list generated (default) - eager : Use a fast algorithm to produce a reasonable short tuple list (best as first choice) - lazy : Work harder (possibly exponentially) to produce a shorter short tuple list - keeplong : Make a 'short tuple list' with no short tuples (only useful for benchmarking) -nocheck ~~~~~~~~~~~~~~~~~~~~ Do not check solutions for correctness before printing them out. -check ~~~~~~~~~~~~~~~~~~ Check solutions for correctness before printing them out. This should only make a difference if Minion contains a bug. -dumptree ~~~~~~~~~~~~~~~~~~~~~ Print out the branching decisions and variable states at each node. -dumptreejson ~~~~~~~~~~~~~~~~~~~~~~~~~ Print out the branching decisions and variable states at each node as a JSON file to a filename. -dumptreesql ~~~~~~~~~~~~~~~~~~~~~~~~~ Print out the branching decisions and variable states at each node to an SQL database. -skipautoaux ~~~~~~~~~~~~~~~~~~~~~~~~ By default Minion adds all variables to the varorder, to ensure that all variables are branched assigned before a solution is outputted. This option disables that behaviour. This means minion Minion *may output solutions incorrectly*, or *incorrect numbers of solutions*. This flag is provided because some users require this low-level control over the search, but is in general useless and dangerous. In particular, it will not speed up search (except when the speed up is due to producing garbage of course!) -randomiseorder ~~~~~~~~~~~~~~~~~~~~~~~~~~~ Randomises the ordering of the decision variables, and the value ordering. If the input file specifies as ordering it will randomly permute this. If no ordering is specified a random permutation of all the variables is used. -jsonsolsout ~~~~~~~~~~~~~~~~~~~~~~~~ Append all solutions to a named file, as JSON objects. Each solution is store as a seperate JSON object. -makeresume ~~~~~~~~~~~~~~~~~~~~~~~ Write a resume file on timeout or being killed. -noresume ~~~~~~~~~~~~~~~~~~~~~ Do not write a resume file on timeout or being killed. (default) -gap ~~~~ Give name of gap executable (defaults to gap.sh) -command-list ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Read a list of commands from ``infile`` and write the results to ``outfile``. This allows batch processing of multiple Minion commands without restarting the solver. -split ~~~~~~~~~~~~~~~~~~ When Minion is terminated before the end of search, write out two new input files that split the remaining search space in half. Each of the files will have all the variables and constraints of the original file plus constraints that rule out the search already done. In addition, the domain of the variable under consideration when Minion was stopped is split in half with each of the new input files considering a different half. This feature is experimental and intended to facilitate parallelisation --to parallelise the solving of a single constraint problem, stop and split repeatedly. Please note that large-scale testing of this feature was limited to Linux systems and it might not work on others (especially Windows). The name of the new input files is composed of the name of the original instance, the string 'resume', a timestamp, the process ID of Minion, the name of the variable whose domain is being split and 0 or 1. Each of the new input files has a comment identifying the name of the input file which it was split from. Similarly, Minion's output identifies the new input files it writes when splitting. The new input files can be run without any special flags. This flag is intended to be used with the -timelimit, -sollimit, -nodelimit or -cpulimit flags. Please note that changing other flags between runs (such as -varorder) may have unintended consequences. Implies -makeresume. -split-stderr ~~~~~~~~~~~~~~~~~~~~~~~~~ The flag -split-stderr has the same function as the flag -split, however the two new Minion input files are sent to standard error rather than written to files. See documentation for -split.