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 standard⁵. Such an input file begins with a line such as the following

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 3.

**Figure 3:** 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 4.

**Figure 4:** 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 matter⁶ 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 5.

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 5:** 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 6.

**Figure 6:** 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}$