SBSAT supports conversion between some of its input formats. For example, an input format such as xor may be converted to cnf. In order to get as direct a translation as possible, the preprocessing should be disabled when performing conversions. This can be achieved by using -In 0 -All 0 switches on the command line.
However, in some cases conversion is done so as to take advantage of preprocessing. Thus, given a file in smurf format, one could preprocess with a result in the same format or a different format like cnf.
One might also want to convert between formats so that a problem might be attempted on a variety of solvers. For example, many problems come in trace or BDD formats but traditional SAT solvers do not recognize those formats so they must be converted to cnf.
Format conversions supported by SBSAT are listed in the following table
(more functionality is currently being developed). To determine whether
format A can be converted to format B, locate A's row and
the answer appears in B's column. For example, format xor
converts to cnf but not from cnf to xor.
| cnf | dnf | bdd | smurf | trace | prove | xor | |
| cnf | yes | no | no | yes | no | no | no |
| dnf | yes | no | no | yes | no | no | no |
| bdd | yes | no | no | yes | no | no | no |
| smurf | yes | no | no | yes | no | no | no |
| trace | yes | no | no | yes | no | no | no |
| prove | yes | no | no | yes | no | no | no |
| xor | yes | no | no | yes | no | no | no |
A sample command for translating a file of one format to another is:
$ sbsat -c flowers.ite > flowers.cnf
which translates a file in trace format to one in cnf format. To get
a direct translation, preprocessing must be turned off. Thus:
$ sbsat -c -All 0 -In 0 flowers.ite > flowers.cnf
or
$ sbsat -c -All 0 -In 0 flowers.ite flowers.cnf
or
$ sbsat -c -All 0 -In 0 flowers.ite -output-file flowers.cnf
would be acceptable.