SATISFIABILITY_OPEN_MP is a FORTRAN90 program which demonstrates, for a particular circuit, an exhaustive search for solutions of the circuit satisfiability problem, using OpenMP for parallel execution.
This problem assumes that we are given a logical circuit of AND, OR and NOT gates, with N=23 binary inputs and a single output. We are to determine all inputs which produce a 1 as the output.
The general problem is NP complete, so there is no known polynomial-time algorithm to solve the general case. The natural way to search for solutions then is exhaustive search of all 2^N possible inputs.
In an interesting way, this is a very extreme and discrete version of the problem of maximizing a scalar function of multiple variables. The difference is that here we know that both the input and output only have the values 0 and 1, rather than a continuous range of real values!
This problem is a natural candidate for parallel computation, since the individual evaluations of the circuit are completely independent.
On an Apple PowerPC G5 with two processors, the following results were observed:
| Threads | 2^N | Time |
|---|---|---|
| 1 | 8,388,608 | 4.38 seconds |
| 2 | 8,388,608 | 2.29 seconds |
| 4 | 8,388,608 | 2.29 seconds |
In the BASH shell, the program could be run with 2 threads using the commands:
export OMP_NUM_THREADS=2
./satisfiability_open_mp
The computer code and data files described and made available on this web page are distributed under the GNU LGPL license.
CNF is data directory which describes the DIMACS CNF file format for defining instances of the satisfiability problem in for boolean formulas in conjunctive normal form.
COMBO is a FORTRAN90 library which includes many combinatorial routines.
FFT_OPEN_MP is a FORTRAN90 program which demonstrates the computation of a Fast Fourier Transform in parallel, using OpenMP.
LAU_NP is a FORTRAN90 library which implements heuristic algorithms for various NP-hard combinatorial problems.
MD_OPEN_MP is a FORTRAN90 program which carries out a molecular dynamics simulation using OpenMP.
MXV_OPEN_MP is a FORTRAN90 program which compares the performance of plain vanilla Fortran and the FORTRAN90 intrinsic routine MATMUL, for the matrix multiplication problem y=A*x, with and without parallelization by OpenMP.
OPEN_MP is a directory of FORTRAN90 examples which illustrate the use of the OpenMP application program interface for carrying out parallel computations in a shared memory environment.
OPEN_MP_ITHACA FORTRAN90 programs which illustrate the use of OpenMP on the Virginia Tech ITHACA cluster.
QUAD_OPEN_MP is a FORTRAN90 program which approximates an integral using a quadrature rule, and carries out the computation in parallel using OpenMP.
SATISFIABILITY is a FORTRAN90 program which demonstrates, for a particular circuit, an exhaustive search for solutions of the circuit satisfiability problem.
SATISFIABILITY_MPI is a FORTRAN90 program which demonstrates, for a particular circuit, an exhaustive search for solutions of the circuit satisfiability problem, using MPI to carry out the calculation in parallel.
SATISFIABILITY_OPEN_MP is available in a C version and a C++ version and a FORTRAN77 version and a FORTRAN90 version.
SATISFIABILITY_PARALLEL is a MATLAB program which is intended to be run in parallel using MATLAB's "PARFOR" feature.
SGEFA_OPEN_MP is a FORTRAN90 program which solves a linear system by Gaussian elimination, using OpenMP.
SUBSET is a FORTRAN90 library which enumerates combinations, partitions, subsets, index sets, and other combinatorial objects.
ZIGGURAT_OPEN_MP, a FORTRAN90 program which demonstrates how the ZIGGURAT library can be used to generate random numbers in an OpenMP parallel program.
SATISFIABILITY_OPEN_MP_RUN runs SATISFIABILITY_OPEN_MP interactively.
SATISFIABILITY_OPEN_MP_BATCH runs SATISFIABILITY_OPEN_MP through the batch system.
You can go up one level to the FORTRAN90 source codes.