function satisfy_brute ( n, formula )

%*****************************************************************************80
%
%% satisfy_brute() uses brute force to satisfy a logical formula.
%
%  Licensing:
%
%    This code is distributed under the MIT license. 
%
%  Modified:
%
%    27 October 2022
%
%  Author:
%
%    John Burkardt
%
%  Reference:
%
%    Michael Quinn,
%    Parallel Programming in C with MPI and OpenMP,
%    McGraw-Hill, 2004,
%    ISBN13: 978-0071232654,
%    LC: QA76.73.C15.Q55.
%
%  Input:
%
%    integer n: the number of variables in the formula.
%
%    integer formula ( integer bvec[] ): a function which evaluates the formula.
%
  fprintf ( 1, '\n' );
  fprintf ( 1, 'satisfy_brute():\n' );
  fprintf ( 1, '  We have a logical function of N logical arguments.\n' );
  fprintf ( 1, '  We do an exhaustive search of all 2^N possibilities,\n' );
  fprintf ( 1, '  seeking those inputs that make the function true.\n' );
%
%  Compute the number of binary vectors to check.
%
  ihi = 2^n;

  fprintf ( 1, '\n' );
  fprintf ( 1, '  The number of logical variables is N = %d\n',  n );
  fprintf ( 1, '  The number of input vectors to check is %d\n', ihi );
  fprintf ( 1, '\n' );
  fprintf ( 1, '   #       Index    ---------Input Values------------------------\n' );
  fprintf ( 1, '\n' );
%
%  Check every possible input vector.
%
  solution_num = 0;

  for i = 0 : ihi - 1

    bvec = i4_to_bvec ( i, n );

    value = formula ( bvec );

    if ( value == 1 )
      solution_num = solution_num + 1;
      fprintf ( 1, '  %2d  %10d   ', solution_num, i );
      for j = 1 : n
        fprintf ( 1, ' %1d', bvec(j) );
      end
      fprintf ( 1, '\n' );
    end

  end
%
%  Report.
%
  fprintf ( 1, '\n' );
  fprintf ( 1, '  Number of solutions found was %d\n', solution_num );

  return
end
