satisfy_brute


satisfy_brute, a Python code which uses brute force to find all assignments of values to a set of logical variables which make a complicated logical statement true.

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 MIT license

Languages:

satisfy_brute is available in a C version and a C++ version and a Fortran90 version and a MATLAB version and an Octave version and a Python version.

Related Data and Programs:

change_diophantine, a Python code which sets up a Diophantine equation to solve the change making problem, which counts the number of ways a given sum can be formed using coins of various denominations.

change_dynamic, a Python code which uses dynamic programming to solve the change making problem, which counts the number of ways a given sum can be formed using coins of various denominations.

change_polynomial, a Python code which uses a polynomial multiplication algorithm to count the ways of making various sums using a given number of coins.

combo, a Python code which includes many combinatorial routines.

football_dynamic, a Python code which uses dynamic programming to count the ways of achieving a given score in football.

knapsack_01_brute, a Python code which uses brute force to solve small versions of the 0/1 knapsack problem;

knapsack_greedy, a Python code which uses a greedy algorithm to estimate a solution of the knapsack problem;

mcnuggets_diophantine, a Python code which uses Diophantine methods to find the ways a given number N of Chicken McNuggets can be assembled, given that they are only available in packages of 6, 9, and 20.

partition_brute, a Python code which uses a brute force method to find solutions of the partition problem, in which a set of integers must be split into two subsets with equal sum.

partition_greedy, a Python code which uses a greedy algorithm to seek a solution of the partition problem, in which a given set of integers is to be split into two groups whose sums are as close as possible.

subset_sum, a Python code which seeks solutions of the subset sum problem.

subset_sum_backtrack, a Python code which uses backtracking to solve the subset sum problem, to find a subset of a set of integers which has a given sum.

subset_sum_brute, a Python code which uses brute force to solve the subset sum problem, to find a subset of a set of integers which has a given sum.

tsp_brute, a Python code which reads a file of city-to-city distances and solves the traveling salesperson problem, using brute force.

tsp_descent, a Python code which is given a city-to-city distance table, chooses an initial tour at random, and then tries simple variations, seeking to quickly find a tour of lower cost for the traveling salesperson problem (TSP).

tsp_greedy, a Python code which reads a file of city-to-city distances, and solves a small traveling salesperson problem (TSP) using the greedy algorithm. It picks a starting city at random, and then successively visits the nearest unvisited city.

tsp_random, a Python code which is given a city-to-city distance table, seeks a solution of the Traveling Salesperson Problem (TSP), by randomly generating round trips that visit every city, returning the tour of shortest length.

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. Bryan Hayes,
    Can't Get No Satisfaction,
    American Scientist,
    Volume 95, Number 1, January-February 1997, pages 16-20.
  3. Michael Quinn,
    Parallel Programming in C with MPI and OpenMP,
    McGraw-Hill, 2004,
    ISBN13: 978-0071232654,
    LC: QA76.73.C15.Q55.
  4. Steven Skiena,
    The Algorithm Design Manual,
    Springer, 1997,
    ISBN: 0-387-94860-0,
    LC: QA76.9.A43S55.

Source Code:


Last revised on 28 October 2022.