next up previous contents
Next: General options Up: SBSAT User Manual and Previous: Quick Start - Getting   Contents


Reference - Command line

The executable file that does the work of SBSAT is called sbsat and is run from the command prompt of a Unix shell. The command line has the following structure:


sbsat [options] [inputfile [outputfile]]


where inputfile is the name of a file containing a problem to be solved, and outputfile names a file to which output from a run of sbsat can be directed. The inputfile can take several formats, all somewhat different from each other, which are described in Section [*]. Options customize the execution of sbsat: they control preprocessing, search, input, and output specifics and more. Observe that options, inputfile, and outputfile are all optional, but that if outputfile is used, it is expected to be placed after inputfile.

Options are invoked using switches. A switch is preceeded by one or two dashes ('-' or '-) and should be immediately followed by a parameter which is either an integer or a string, depending on the switch (at the moment there are no integer switches associated with sbsat. If a switch requires a parameter, one or more blank characters separates it from the parameter. Switch/parameter pairs are separated from each other and the file names by blanks. There are many switches and they are organized below by type.

Some example runs are as follows:


$ sbsat -help
Lists all command line options


$ sbsat -R r example.cnf
Solve the problem in example.cnf, show the result raw


$ sbsat -P {ExDc}3{ExSt}2{ExPr}10 example.cnf
Preprocess the problem in example.cnf a certain way, then solve.

Switch-parameter pairs and file names may be placed anywhere on a command line after sbsat. Thus, the following two runs are identical:


$ sbsat -R r example.cnf
$ sbsat example.cnf -R r

A switch may appear more than once on a command line. In that case the rightmost switch applies. In case contradictory switches are given, the rightmost applies. For example:


$ sbsat -b -w

will invoke the BDD WalkSAT search (see Page [*] for option -w). Some switch combinations cooperate with each other. For example:


$ sbsat -All 0 -St 1

turns all preprocessing off then turns strengthening on (see Page [*] for preprocessing switches).



Subsections
next up previous contents
Next: General options Up: SBSAT User Manual and Previous: Quick Start - Getting   Contents
John Franco 2011-09-15