SATISFIABILITY_MPI
Circuit Satisfiability Using MPI

SATISFIABILITY_MPI is a FORTRAN90 program which demonstrates, for a particular circuit, an exhaustive search for solutions of the circuit satisfiability problem. This version of the program uses MPI to carry out the solution in parallel.

This problem assumes that we are given a logical circuit of AND, OR and NOT gates, with N 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.

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 was a natural candidate for parallel computation, since the individual evaluations of the circuit are completely independent.

Related Data and Programs:

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.

HEAT_MPI is a FORTRAN90 program which solves the 1D Time Dependent Heat Equation using MPI.

LAU_NP is a FORTRAN90 library which implements heuristic algorithms for various NP-hard combinatorial problems.

MPI is a directory of FORTRAN90 examples which illustrate the use of the MPI application program interface for carrying out parallel computatioins in a distributed memory environment.

MPI_STUBS is a FORTRAN90 library which contains "stub" MPI routines, allowing a user to compile, load, and possibly run an MPI program on a serial machine.

QUAD_MPI is a FORTRAN90 program which approximates an integral using a quadrature rule, and carries out the computation in parallel using MPI.

RANDOM_MPI, a FORTRAN90 program which demonstrates one way to generate the same sequence of random numbers for both sequential execution and parallel execution under MPI.

SATISFIABILITY is a FORTRAN90 program which solves the circuit satisfiability problem.

SATISFIABILITY_MPI is available in a C version and a C++ version and a FORTRAN77 version. a FORTRAN90 version.

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.

SUBSET is a FORTRAN90 library which enumerates combinations, partitions, subsets, index sets, and other combinatorial objects.

Reference:

Michael Quinn,
Parallel Programming in C with MPI and OpenMP,
McGraw-Hill, 2004,
ISBN13: 978-0071232654,
LC: QA76.73.C15.Q55.

Source Code:

satisfiability_mpi.f90, the source code.

Examples and Tests:

It is possible to run the code with a dummy version of MPI called "MPI_STUBS". To do this, the source code must replace the line

use mpi

include 'mpi_stubs_f90.h'

and, of course, the compile and load statements must be changed. The resulting code will run as though it were using MPI on one processor.

satisfiability_mpi_stubs.csh, C Shell commands to compile and run the source code.
satisfiability_mpi_stubs_output.txt, the output file.

Here the code is run with a standard MPI library.

satisfiability_mpi.sh, BASH shell commands to compile and run the source code.
satisfiability_mpi_output.txt, the output file.

List of Routines:

MAIN is the main program for SATISFIABILITY_MPI.
BVEC_NEXT generates the next binary vector.
CIRCUIT_VALUE returns the value of a circuit for a given input set.
TIMESTAMP prints the current YMDHMS date as a time stamp.

You can go up one level to the FORTRAN90 source codes.