Formats

Solvers take as input one of the following file formats.  

cnf

A cnf file represents a propositional formula in Conjunctive Normal Form (CNF). The DIMACS cnf format is the standard format for SAT solvers, and is also a popular format for MaxSAT solvers, model counters, and knowledge compilers. This format is described in this pdf (from the DIMACS FTP site) and by the SAT competitions.

weighted cnf

Solvers for weighted (partial) MaxSAT commonly use an extended DIMACS format for CNFs. In particular, this format adds weights to each clause and a way to specify hard constraints (for partial MaxSAT). This extended format is used and described by MaxSAT competitions.

quantified cnf

QBF solvers can support a number of input formats, but QDIMACS is one popular format, which represents quantified CNF formulas. The QDIMACS format is described here.

first-order cnf

First-order model counters and first-order knowledge compilers support a variety of input formats, such as parfactor graphs and Markov logic networks. Many formats can be converted to first-order CNFs, via an extend DIMACS format.