Reference - Input formats

Problems to be solved are typically presented to sbsat as a file formatted in a particular way (input is also allowed from standard input). This section describes the various input formats accepted by sbsat. The canonical format is the most general and is described first. An important format is DIMACS CNF which is specified in

ftp://dimacs.rutgers.edu/pub/challenge/satisfiability/doc/satformat.dvi

and a description is given here. Other useful formats include XOR, for handling a rather specific type of problem where each conjunct is an xor of conjuncts, DNF, Trace (a language used in CMU benchmarks), Prove (automatically generated by the CMU tool named BMC), and SMURF (a special form directly tied to SBSAT data structures).

The inputs formats support up to five different types of statements and each applicable type is described separately in a subsection of the format's description section. The types are as follows:

1. Comment: A comment is text beginning with a special character (depending on the input format) and ending with the first newline following that character. All comments are ignored by sbsat hence comments can be placed anywhere as separate lines or on the same line after other line types.

2. File Header: There is one file header and it occupies one line of the file. It specifies the type of input format and must be placed before all other lines except fully commented lines. The header is immediately checked by sbsat which then applies the appropriate parser to the remainder of the file.

3. Boolean Function: Certain syntax, given below, is used to express a Boolean function in a file. Arguments may be variables or Boolean functions or, in some formats, references to Boolean functions. If an assignment to the variables of the file results in values of $T$ for all of a particular subset of (possibly all) Boolean function statements then that assignment is a solution to the problem represented in the input file.

4. Manipulator: A manipulator is a Boolean function composed from one or more Boolean functions it takes as arguments. Its purpose is to provide alternative, simpler, or modified forms of its input functions which will lead to faster search.

5. Directive: A directive is a statement of control, for example, of search or output, or of substitution. A directive is applied at the point it occurs in the input file while the file is being parsed. A directive does not apply to any of the input file that has not been parsed by the time the directive is executed.

Directives, Boolean functions, and manipulators can appear in any order after the file header.