subroutine i4_to_bvec ( i4, n, bvec )

!*****************************************************************************80
!
!! i4_to_bvec() converts an integer into a binary vector.
!
!  Licensing:
!
!    This code is distributed under the MIT license.
!
!  Modified:
!
!    20 March 2009
!
!  Author:
!
!    John Burkardt
!
!  Input:
!
!    integer I4, the integer.
!
!    integer N, the dimension of the vector.
!
!  Output:
!
!    integer BVEC(N), the vector of binary remainders.
!
  implicit none

  integer n

  integer bvec(n)
  integer i
  integer i4
  integer i4_copy

  i4_copy = i4

  do i = n, 1, -1
    bvec(i) = mod ( i4_copy, 2 )
    i4_copy = i4_copy / 2
  end do

  return
end
subroutine satisfy_brute ( n, formula )

!*****************************************************************************80
!
!! satisfy_brute() seeks all logical variable assignments that satisfy a 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.
!
  implicit none

  integer, allocatable :: bvec(:)
  integer, external :: formula
  integer i
  integer ihi
  integer n
  integer solution_num
  integer value

  allocate ( bvec(1:n) )

  write ( *, '(a)' ) ' '
  write ( *, '(a)' ) 'satisfy_brute():'
  write ( *, '(a)' ) '  We have a logical function of N logical arguments.'
  write ( *, '(a)' ) '  We do an exhaustive search of all 2^N possibilities,'
  write ( *, '(a)' ) '  seeking those inputs that make the function TRUE.'
!
!  Compute the number of binary vectors to check.
!
  ihi = 2**n

  write ( *, '(a)' ) ' '
  write ( *, '(a,i8)' ) '  The number of logical variables is N = ',  n
  write ( *, '(a,i8)' ) '  The number of input vectors to check is ', ihi
  write ( *, '(a)' ) ' '
  write ( *, '(a)' ) &
    '   #       Index    ---------Input Values------------------------'
  write ( *, '(a)' ) ' '
!
!  Check every possible input vector.
!
  solution_num = 0

  do i = 0, ihi - 1

    call i4_to_bvec ( i, n, bvec )

    value = formula ( bvec )

    if ( value == 1 ) then
      solution_num = solution_num + 1

      write ( *, '(2x,i2,2x,i10,3x,23i2)' )  solution_num, i, bvec(1:n)
    end if

  end do
!
!  Report.
!
  write ( *, '(a)' ) ' '
  write ( *, '(a,i8)' ) '  Number of solutions found was ', solution_num

  deallocate ( bvec )

  return
end