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 9. 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 small.cnf
Solve the problem in small.cnf, show the
result raw
$ sbsat -P {ExDc}3{ExSt}2{ExPr}10 small.cnf
Preprocess the problem in small.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 small.cnf
$ sbsat small.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).