Online Help

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\}$