CNF is a text-based file format for storing a Boolean expression in conjunctive normal form. The format was created by DIMACS (Center for Discrete Mathematics and Theoretical Computer Science).

The general-purpose commands Import and Export also support this format.

When importing data with Import, you can use the option variables in order to control the names used by Maple to represent the variables in the imported expression. The option takes the form variables=v where v is either a procedure or a list of variable names. In the first case, the procedure must accept a string input and return a name. In the second case, the list of variable names must be a list of unique unassigned names which Import will use when importing the CNF expression. By default, Import produces an expression with automatically generated names.

$\mathrm{expr}≔\mathrm{Import}\left(''example/3sat.cnf''\,\mathrm{base}=\mathrm{datadir}\right)$

$\mathrm{expr}≔\left(B\mathbf{or}\mathrm{B1}\mathbf{or}\mathbf{not}\mathrm{B0}\right)\mathbf{and}\left(\mathrm{B0}\mathbf{or}\mathrm{B1}\mathbf{or}\mathbf{not}B\right)\mathbf{and}\left(\mathrm{B1}\mathbf{or}\mathbf{not}B\mathbf{or}\mathbf{not}\mathrm{B0}\right)$

$\mathrm{expr}$

$\left(B\mathbf{or}\mathrm{B1}\mathbf{or}\mathbf{not}\mathrm{B0}\right)\mathbf{and}\left(\mathrm{B0}\mathbf{or}\mathrm{B1}\mathbf{or}\mathbf{not}B\right)\mathbf{and}\left(\mathrm{B1}\mathbf{or}\mathbf{not}B\mathbf{or}\mathbf{not}\mathrm{B0}\right)$

$\mathrm{expr}≔\mathrm{Import}\left(''example/3sat.cnf''\,\mathrm{base}=\mathrm{datadir}\,\mathrm{variables}=\left[x\,y\,z\right]\right)$

$\mathrm{expr}≔\left(x\mathbf{or}z\mathbf{or}\mathbf{not}y\right)\mathbf{and}\left(y\mathbf{or}z\mathbf{or}\mathbf{not}x\right)\mathbf{and}\left(z\mathbf{or}\mathbf{not}x\mathbf{or}\mathbf{not}y\right)$

$\mathrm{Logic}:-\mathrm{Satisfy}\left(\mathrm{expr}\right)$

$\left\{x=\mathrm{false}\,y=\mathrm{false}\,z=\mathrm{false}\right\}$