next up previous contents
Next: Quick Start - Some Up: Quick Start - The Previous: Choosing a search procedure   Contents

Converting the input file

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 example.ite > example.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 example.ite > example.cnf

or


$ sbsat -c -All 0 -In 0 example.ite example.cnf

or


$ sbsat -c -All 0 -In 0 example.ite -output-file example.cnf

would be acceptable.


next up previous contents
Next: Quick Start - Some Up: Quick Start - The Previous: Choosing a search procedure   Contents
John Franco 2011-09-15