CNF_IO\
Read or Write a CNF File {#cnf_io-read-or-write-a-cnf-file align=”center”}
========================
CNF_IO is a C++ library which can read or write 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: {#licensing align=”center”}
The computer code and data files described and made available on this
web page are distributed under the GNU LGPL
license.
Languages: {#languages align=”center”}
CNF_IO is available in a C++
version and a FORTRAN77
version and a FORTRAN90
version.
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 C++ program which
demonstrates, for a particular circuit, an exhaustive search for
solutions of the circuit satisfiability problem.
Reference: {#reference align=”center”}
- 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: {#source-code align=”center”}
Examples and Tests: {#examples-and-tests align=”center”}
List of Routines: {#list-of-routines align=”center”}
- CH_CAP capitalizes a single character.
- CH_EQI is true if two characters are equal, disregarding case.
- CH_IS_SPACE is TRUE if a character represents “white space”.
- CNF_DATA_READ reads the data of a CNF file.
- CNF_DATA_WRITE writes data to a CNF file.
- CNF_EVALUATE evaluates a formula in CNF form.
- 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.
- I4_POWER returns the value of I\^J.
- LVEC_NEXT generates the next logical vector.
- S_ADJUSTL flushes a string left.
- S_BLANKS_DELETE replaces consecutive blanks by one blank.
- S_EQI reports whether two strings are equal, ignoring case.
- S_LEN_TRIM returns the length of a string to the last
nonblank.
- S_TO_I4 reads an I4 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 C++ source codes.
Last revised on 09 June 2008.