cnf_io, a Fortran90 code which reads or writes DIMACS Conjunctive Normal Form (CNF) files defining satisfiability problems in terms of a boolean formula.
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.
The information on this web page is distributed under the MIT license.
cnf_io is available in a C++ 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_brute, a Fortran90 code which demonstrates, for a particular circuit, an exhaustive search for solutions of the circuit satisfiability problem.