The DIMACS CNF file format is used to define a Boolean expression, written in conjunctive normal form, that may be used as an example of the satisfiability problem. The new logic module (sympy.logic) can read the content of a cnf file and transform it into a boolean expression suitable for use in other methods. For example, let quinn.cnf be a file with the following content:

c  an example from Quinn's text, 16 variables and 18 clauses.
c Resolution: SATISFIABLE
c
p cnf 16 18
  1    2  0
 -2   -4  0
  3    4  0
 -4   -5  0
  5   -6  0
  6   -7  0
  6    7  0
  7  -16  0
  8   -9  0
 -8  -14  0
  9   10  0
  9  -10  0
-10  -11  0
 10   12  0
 11   12  0
 13   14  0
 14  -15  0
 15   16  0

Then we can load the file and test for satisfiability:

In [1]: from sympy.logic.utilities.dimacs import load_file

In [2]: expr = load_file("quinn.cnf")

In [3]: from sympy.logic.inference import satisfiable

In [4]: satisfiable(expr)
Out[4]:
{cnf_1: True, cnf_11: ...

References: more on the DIMACS CNF file format
BUGS: For large files like this one it exits prematurely with an error in the DPLL algorithm.