satisfy_openmp, a C++ code 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.
In the BASH shell, the program could be run with 2 threads using the commands:
export OMP_NUM_THREADS=2
./satisfy_openmp
The information on this web page is distributed under the MIT license.
satisfy_openmp 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.
openmp_test, a C++ code which uses the OpenMP application program interface for parallel computations in a shared memory environment.
satisfy, a C++ code which demonstrates, for a particular circuit, an exhaustive search for solutions of the circuit satisfy problem.
satisfy_MPI, a C++ code which demonstrates, for a particular circuit, an exhaustive search for solutions of the circuit satisfy problem, using MPI to carry out the calculation in parallel.