cnfgen.utils.parsedimacs module

Read and write DIMACS format

DIMACS format is the industry standard for the encoding of CNF formulas. It is the most popular input format for SAT solvers [1].

References

[1]	http://www.cs.ubc.ca/~hoos/SATLIB/Benchmarks/SAT/satformat.ps

from_dimacs_file(cnfclass, fileorname=None)

Read DIMACS into a CNF object

Parameters:

cnfclass: subclass of cnfgen.basecnf.BaseCNF

the type of CNF object to produce

fileorname: file object or string (or stdin if None)

destination file given either as object or as filename

parse_dimacs(infile)

Parse a dimacs cnf in file object

Given a file object, this function extracts the number of variables and clauses, and the sequence of clauses in the file.

The generator emits - n : the number of variables - m : the number of clauses - c1, c2, c3, … : a sequence of m clauses

Parameters:

infile: file object

the file containing the dimacs text

Returns:

a generator object

Raises:

ValueError : in case there are mistakes in the file content

to_dimacs_file(formula, fileorname=None, export_header=True, export_varnames=False)

Save the DIMACS encoding of a formula to a file

Parameters:

formula:

a cnf formula

fileorname: file object or string (or stdout if None)

destination file given either as object or as filename

export_header : bool

determines whether the formula header should be inserted as a comment in the DIMACS output.

export_varnames : bool, optional

determines whether a map from variable indices to variable names should be appended to the header.