SATISFIABILITY_OPEN_MP is a C 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.24 seconds |
| 2 | 8,388,608 | 2.15 seconds |
| 4 | 8,388,608 | 2.28 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 a 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 C 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 C program which carries out a molecular dynamics simulation using OpenMP.
MXV_OPEN_MP is a C 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 C examples which illustrate the use of the OpenMP application program interface for carrying out parallel computations in a shared memory environment.
OPEN_MP_ITHACA C programs which illustrate the use of OpenMP on the Virginia Tech ITHACA cluster.
QUAD_OPEN_MP is a C program which approximates an integral using a quadrature rule, and carries out the computation in parallel using OpenMP.
SATISFIABILITY is a C program which demonstrates, for a particular circuit, an exhaustive search for solutions of the circuit satisfiability problem.
SATISFIABILITY_MPI is a C 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.
SGEFA_OPEN_MP is a C program which solves a linear system by Gaussian elimination, using OpenMP.
SATISFIABILITY_PARALLEL is a MATLAB program which is intended to be run in parallel using MATLAB's "PARFOR" feature.
SUBSET is a C++ library which enumerates combinations, partitions, subsets, index sets, and other combinatorial objects.
ZIGGURAT_OPEN_MP, a C 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 C source codes.