DIMACS CNF (.cnf) Format - Maple Programming Help

Online Help

All Products    Maple    MapleSim


Home : Support : Online Help : Programming : Input and Output : File Formats : Formats/CNF

DIMACS CNF (.cnf) Format

DIMACS file format

 

Description

Examples

Description

• 

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.

Examples

Import a DIMACS CNF file encoding a Boolean expression.

Import with automatically generated variable names

exprImportexample/3sat.cnf,base=datadir

exprBorB1ornotB0andB0orB1ornotBandB1ornotBornotB0

(1)

expr

BorB1ornotB0andB0orB1ornotBandB1ornotBornotB0

(2)

Import with a specified list of variable names and find a satisfying assignment

exprImportexample/3sat.cnf,base=datadir,variables=x,y,z

exprxorzornotyandyorzornotxandzornotxornoty

(3)

Logic:-Satisfyexpr

x=false,y=false,z=false

(4)

See Also

Formats

Logic