DIMACS

Format to represent Boolean formulae in conjunctive normal form. It is used to interact with SAT solvers. Description of the format as was given for the SAT competition in 2009: http://www.satcompetition.org/2009/format-benchmarks2009.html