SATISFY
Seek Binary Circuit Inputs that Output 1


SATISFY is a C program which demonstrates, for a particular circuit, an exhaustive search for solutions of the circuit satisfy problem.

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

The example circuit considered here has been described in conjunctive normal form ("CNF"). This is a standard format for logical formulas. At the highest level, the formula consists of clauses joined by the AND (conjunction) operator. Each clause consists of signed literals joined by the OR (disjunction) operator. Each signed literal is either the name of a variable (positive literal), or the name of a variable preceded by the NOT (negation) operator (a negative literal). There is a CNF file format that can be used to store logical formulas that have been cast into conjunctive normal form.

Licensing:

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

Languages:

SATISFY is available in a C version and a C++ version and a FORTRAN77 version and a FORTRAN90 version and a MATLAB version and a Python version.

Related Data and Programs:

CHANGE_MAKING, a C library which considers the change making problem, in which a given sum is to be formed using coins of various denominations.

CNF, a data directory which describes the DIMACS CNF file format for defining instances of the satisfy problem for boolean formulas in conjunctive normal form.

COMBINATION_LOCK, a C program which simulates the process of determining the secret combination of a lock.

COMBO, a C library which includes many combinatorial routines.

KNAPSACK_01, a C library which uses brute force to solve small versions of the 0/1 knapsack problem;

SATISFY_MPI, a C program 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.

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.

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

SUBSET_SUM, a C library which seeks solutions of the subset sum problem.

TSP_BRUTE, a C program which reads a file of city-to-city distances and solves the traveling salesperson problem, using brute force.

Reference:

  1. Rina Dechter,
    Enhancement Schemes for constraint processing: Backjumping, learning, and cutset decomposition,
    Artificial Intelligence,
    Volume 41, Number 3, January 1990, pages 273-312.
  2. Michael Quinn,
    Parallel Programming in C with MPI and OpenMP,
    McGraw-Hill, 2004,
    ISBN13: 978-0071232654,
    LC: QA76.73.C15.Q55.
  3. Steven Skiena,
    The Algorithm Design Manual,
    Springer, 1997,
    ISBN: 0-387-94860-0,
    LC: QA76.9.A43S55.

Source Code:

List of Routines:

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


Last revised on 03 May 2008.