cnf_io

cnf_io, a FORTRAN77 code 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 FORTRAN77 version and a FORTRAN90 version.

Related Data and Programs:

cnf_io_test

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 FORTRAN77 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.
2. dimacs_cnf.pdf, a writeup of the DIMACS CNF file format.

Source Code:

• cnf_io.f, the source code.
• cnf_io.sh, commands to compile the source code.