SATISFY_MPI
Circuit Satisfiability Using MPI


SATISFY_MPI is a C program which demonstrates, for a particular circuit, an exhaustive search for solutions of the circuit satisfy 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.

Licensing:

The computer code and data files made available on this web page are distributed under the GNU LGPL license.

Languages:

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

Related Data and Programs:

COMMUNICATOR_MPI, a C program which creates new communicators involving a subset of initial set of MPI processes in the default communicator MPI_COMM_WORLD.

HEAT_MPI, a C program which solves the 1D Time Dependent Heat Equation using MPI.

HELLO_MPI, a C program which prints out "Hello, world!" using the MPI parallel programming environment.

LAPLACE_MPI, a C program which solves Laplace's equation on a rectangle, using MPI for parallel execution.

MOAB, examples which illustrate the use of the MOAB job scheduler for a computer cluster.

MPI, C programs which illustrate the use of the MPI application program interface for carrying out parallel computatioins in a distributed memory environment.

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

MULTITASK_MPI, a C program which demonstrates how to "multitask", that is, to execute several unrelated and distinct tasks simultaneously, using MPI for parallel execution.

POISSON_MPI, a C program which computes a solution to the Poisson equation in a rectangle, using the Jacobi iteration to solve the linear system, and MPI to carry out the Jacobi iteration in parallel.

PRIME_MPI, a C program which counts the number of primes between 1 and N, using MPI for parallel execution.

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

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

RING_MPI, a C program which uses the MPI parallel programming environment, and measures the time necessary to copy a set of data around a ring of processes.

SATISFY, a C program which solves the circuit satisfy problem.

SATISFY_OPENMP, a C program which demonstrates, for a particular circuit, an exhaustive search for solutions of the circuit satisfy problem, using OpenMP for parallel execution.

SEARCH_MPI, a C program which searches integers between A and B for a value J such that F(J) = C, using MPI.

WAVE_MPI, a C program which uses finite differences and MPI to estimate a solution to the wave equation.

Reference:

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

Source Code:

Examples and Tests:

SATISFY_LOCAL compiles and runs the program on the local machine, which presumably has a version of MPI installed.

SATISFY_FSU compiles and runs the program on the FSU HPC cluster.

SATISFY_SYSX compiles and runs the program on Virginia Tech's System X cluster.

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


Last revised on 04 May 2008.