satisfy_mpi, a C++ code 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.
The latest versions of MPI no longer support the special C++ MPI bindings, so the examples given here have reverted to using the C MPI bindings.
The information on this web page is distributed under the MIT license.
satisfy_mpi is available in a C version and a C++ version and a Fortran90 version.
cnf, a data directory which describes the DIMACS CNF file format for defining instances of the satisfy problem in for boolean formulas in conjunctive normal form.
mpi_test, a C++ code which uses the message passing interface (MPI) for parallel computations in a distributed memory environment.
satisfy, a C++ code which solves the circuit satisfy problem.
satisfy_openmp, a C++ code which solves the circuit satisfy problem using the OpenMP parallel programming system.