next up previous contents
Next: An input in canonical Up: Quick Start - The Previous: Command line   Contents


A CNF formula as input

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 [*].

Figure: Contents of the ascii file small.cnf
\begin{figure}\begin{verbatim}p cnf 6 8
c This is a demonstration of the CNF...
...5 6 0
-1 -2 -3 0
-2 -3 -4 0
-3 -4 -5 0
-4 -5 -6 0\end{verbatim}
\end{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 [*].

Figure: Output generated by the command $ sbsat small.cnf.
\begin{figure}\begin{verbatim}Reading File small.cnf ....
Reading CNF ... Do...
...processing .... Done
Satisfiable
Total Time: 0.008\end{verbatim}
\end{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 one above.


$ 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).

Figure: Output generated by command $ sbsat -R r small.cnf.
\begin{figure}\begin{verbatim}Reading File small.cnf ....
Reading CNF ... Do...
... Done
1 2 -3 4 5 -6
Satisfiable
Total Time: 0.009\end{verbatim}
\end{figure}

The default output mixes solution information with execution information. Solution information may be separated from execution information as follows.


$ 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 [*].

Figure: Beginning of output generated by the command sbsat -help.
\begin{figure}\footnotesize {
\begin{verbatim}SBSAT is a SAT solver.
Usage: sb...
... (n=no result, r=raw, f=fancy) [default=\lq\lq n'']
...\end{verbatim}
}
\end{figure}


next up previous contents
Next: An input in canonical Up: Quick Start - The Previous: Command line   Contents
John Franco 2011-09-15