SBSAT recognizes a CNF formula as input if it is expressed in an ascii file that is formatted according to the DIMACS standard5. Such an input file begins with a line such as the following
p cnf <number_of_variables> <number_of_clauses>
where <number_of_variables> is the number of distinct variables present in the file and <number_of_clauses> is the number of clauses present in the input file. Lines starting with the character c indicate a comment and are ignored. Variables are represented as positive numbers, beginning with 1. A positive literal is a positive number and a negative literal is a negative number. Each clause is expressed on one line as a 0 terminated list of numbers, separated by blanks, and representing the literals of the clause. The contents of a file named small.cnf is shown in Figure .
Use the following commands to run sbsat on file small.cnf
(assume the starting point is the root directory of the SBSAT tree):
$ cd examples
$ sbsat small.cnf
The output is shown in Figure .
In order to get the actual satisfiable assignment from the solver we
need to add the input parameter to the command line which instructs the
solver to output the solution. The following command is this:
$ sbsat -R r small.cnf
Remark: The format of small.cnf is automatically determined by sbsat so a command line switch to set a format is not necessary.
Remark: The order of the parameters on the
command line usually does not matter6 provided the values remain
immediately to the right of the switches they associate with. So, in
this case the following command line would do exactly the same as the
$ sbsat small.cnf -R r
Output from the above command is shown in Figure .
Remark: In case the same switch is used more than
once on the command line, the rightmost switch applies. For example,
$ sbsat small.cnf -R r -R f
prints fancy instead of raw output format (see Pages and for the meaning of these formats).
The default output mixes solution information with execution information.
Solution information may be separated from execution information as
$ sbsat small.cnf -R r -output-file output.txt
Output from this run is sent to the file output.txt as follows:
1 2 -3 4 5 -6
Remark: Some of the command line options have both a short and a long flag which can be used interchangably. For example the '-show-result' switch is interchangeable with '-R'.
All available switches can be printed using the following command:
$ sbsat -help
which gives the output shown, in part, in Figure .