CNF_IO
Read or Write a CNF File

CNF_IO is a FORTRAN90 library which reads or writes a file, in the DIMACS CNF format, containing information about a boolean formula written in conjunctive normal form.

Boolean expressions, written in conjunctive normal form, may be used as test cases for the satisfiability problem. That problem seeks to determine all possible combinations of variable values that result in the formula being evaluated as TRUE.

The routines in CNF_IO are intended to make it possible to transfer information between a CNF file and a computer program.

Licensing:

The computer code and data files described and made available on this web page are distributed under the GNU LGPL license.

Languages:

CNF_IO is available in a C++ version and a FORTRAN90 version.

Related Data and Programs:

CNF, a data directory which describes the DIMACS CNF file format for specifying instances of the satisfiability problem for boolean formulas in conjunctive normal form.

SATISFY, a FORTRAN90 program which demonstrates, for a particular circuit, an exhaustive search for solutions of the circuit satisfiability problem.

Reference:

1. Rina Dechter,
   Enhancement Schemes for constraint processing: Backjumping, learning, and cutset decomposition,
   Artificial Intelligence,
   Volume 41, Number 3, January 1990, pages 273-312.

Source Code:

• cnf_io.f90, the source code.

Examples and Tests:

• cnf_io_test.f90, a sample calling program.
• cnf_io_test.txt, the output file.
• test01_v3_c2.cnf, a CNF file, for 3 variables and 2 clauses, written by the sample program.
• test02_v16_c18.cnf, a CNF file, for 16 variables and 18 clauses, written by the sample program.

List of Routines:

• CH_CAP capitalizes a single character.
• CH_EQI is a case insensitive comparison of two characters for equality.
• CH_IS_SPACE is TRUE if a character is a whitespace character.
• CNF_EVALUATE evaluates a formula in CNF form.
• CNF_DATA_READ reads the data of a CNF file.
• CNF_DATA_WRITE writes data to a CNF file.
• CNF_HEADER_READ reads the header of a CNF file.
• CNF_HEADER_WRITE writes the header for a CNF file.
• CNF_PRINT prints CNF information.
• CNF_WRITE writes the header and data of a CNF file.
• GET_UNIT returns a free FORTRAN unit number.
• LVEC_NEXT generates the next logical vector.
• S_BLANKS_DELETE replaces consecutive blanks by one blank.
• S_EQI is a case insensitive comparison of two strings for equality.
• S_TO_I4 reads an integer value from a string.
• S_WORD_EXTRACT_FIRST extracts the first word from a string.
• TIMESTAMP prints the current YMDHMS date as a time stamp.

You can go up one level to the FORTRAN90 source codes.