satisfy_brute, an Octave 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.
The information on this web page is distributed under the MIT license.
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.
closest_pair_brute, an Octave code which uses brute force to solve a 2D version of the closest pair problem, which identifies the closest pair of points in a given collection.
knapsack_01_brute, an Octave code which uses brute force to solve small versions of the 0/1 knapsack problem;
matrix_chain_brute, an Octave code which finds the cost of the most efficient ordering to use when multiplying a sequence of matrices, using brute force.
octave_combinatorics, an Octave code which considers a variety of problems in combinatorics involving counting, combinations, permutations, and so on.
partition_brute, an Octave 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.
subset_sum_brute, an Octave 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, an Octave code which is given a city-to-city distance table, and solves a (small) traveling salesperson problem (TSP), using brute force.