// sat.ntm  The classic problem of determining if a boolean formula
//          is satisfiable.
//          Given a formula with n boolean variables, is there a
//          n-bit binary number where the first bit is the value of
//          the first variable, and so forth, such that the formula
//          is true.  This is a satisfying assignment.
//
// We code the boolean formula on the input tape in normal form
// as the logical-and of terms where each term is a n-bit ternary number
// with interpretation: a 1 in the i-th position means the i-th
// variable, a 0 in the i-th position means the complement
// of the i-th variable and an x in the i-th position means the
// i-th variable is a don't care. The variables in a term are logically-ored.
// An ampersand, "&", separates each term. The nondeterministic
// Turing machine accepts if the boolean formula has a satisfying assignment.
//
// This is a version of Satisfiability from "Handbook of Theoretical
// Computer Science" edited by J. van Leeuwen. P 83 with the substitution:
// If ui and its complement are both in a term, delete the term because it
// is satisfied and if neither ui nor its complement are in a term,
// use x for the i-th position of that term.
//
// Note some special cases: Any input tape with syntax errors is
// rejected. Any term of all x's can not be true (or false) thus causes
// reject.
//
// For convenience, we start with the first n tape positions blank and
// an ampersand. A blank is typed as  #b . #[ and #] are internal, begin-end
// Then nondeterministically generate 2^n assignments in
// these blank positions. Given one path with assignments g1 g2 g3 say 010
//
// Algorithm: start with  #[ g1 g2 g3 &  0  1  x  &  x  x  0  #]
//                           &  g2 g3 g1 &                       check
//                              &  g3 g1 g2 &                    copy
//                                 &  g1 g2 g3 &                 copy
//                                    &  g1 g2 g3 &              shift
//                                       &  g2 g3 g1 &           check
//                                          &  g3 g1 g2 &        check
//                                             &  g1 g2 g3 &     shift
//                                                &  g1 g2 g3 #] accept
// any term failure causes that path to die

start s
final f

s   #b  s    0  R  // these two lines generate 2^n assignments
s   #b  s    1  R  // and are the only nondeterministic transitions
s   &   b0   ## L  // finished generating
s   #]  fail ## N  // null tape fail

b0  1   b0   ## L  // go to beginning of assignment
b0  0   b0   ## L  // go to beginning of assignment
b0  #[  c    ## R  // ready to start checking first term
b0  &   c    ## R  // ready to start next variable of next term check

b1  &   b2   ## L  // back up one
b2  1   b2   ## L  // go to beginning of assignment
b2  0   b2   ## L  // go to beginning of assignment
b2  &   d    ## R  // ready to start next variable of next term copy

c   0   c0   &  R  // go check and set next term variable after &
c   1   c1   &  R  // go check and set next term variable after &

d   0   d0   &  R  // go set next term variable after &
d   1   d1   &  R  // go set next term variable after &

c0  0   c0   ## R  // just move to next &, zero mode
c0  1   c0   ## R  // just move to next &, zero mode
c0  &   c2   0  R  // just move to next &, zero mode
c0  #]  f    ## N  // accept

d0  0   d0   ## R  // just move to next &, zero mode
d0  1   d0   ## R  // just move to next &, zero mode
d0  &   d2   0  R  // just move to next &, zero mode
d0  #]  f    ## N  // accept

c2  0   c4   &  R  // term OK, finish copying assignment
c2  1   b0   &  L  // keep checking 
c2  x   b0   &  L  // keep checking

d2  0   c4   &  R  // term OK, finish copying assignment
d2  1   c4   &  R  // finish copying assignment 
d2  x   c4   &  R  // finish copying assignment

c4  #]  f    ## N  // accept
c4  &   sh   ## L  // shift
c4  1   b1   ## L  // pass
c4  0   b1   ## L  // pass
c4  x   b1   ## L  // pass

c1  0   c1   ## R  // just move to next &, one mode
c1  1   c1   ## R  // just move to next &, one mode
c1  &   c3   1  R  // just move to next &, one mode
c1  #]  f    ## N  // accept

d1  0   d1   ## R  // just move to next &, one mode
d1  1   d1   ## R  // just move to next &, one mode
d1  &   d2   1  R  // just move to next &, one mode
d1  #]  f    ## N  // accept

c3  0   b0   &  L  // keep checking
c3  1   c4   &  R  // term OK, finish copying assignment 
c3  x   b0   &  L  // keep checking

sh  0   sh0  &  R  // all below just shift assignment right
sh  1   sh1  &  R
sh  &   sh   ## L

sh0 0   shb  0  R
sh0 1   shb  0  R
sh0 &   b0   0  L

sh1 0   shb  1  R
sh1 1   shb  1  R
sh1 &   b0   1  L

shb 0   sh   ## L
shb 1   sh   ## L

enddef

tape             // null rejected
tape #b&1        // accept 1       A
tape #b&0        // accept 0       not A
tape #b&x        // reject         x
tape #b&1&0      // reject         A & not A 
tape #b&0&1      // reject         not A & A
tape #b&1&x      // reject
tape #b&x&0      // reject
tape #b#b&11&10  // accept 10 or 11 (A | B) & (A | not B)
tape #b#b&01&00  // accept 00 or 01 (not A | B) & (not A | not B)
tape #b#b&11&01  // accept 11 or 01 (A | B) & (not A | B)
tape #b#b&00&10  // accept 00 or 10 (not A | not B) & (A | not B)
tape #b#b&1x&x0  // accept 10      A & not B
tape #b#b#b&1xx&x01&xx1&10x&x01&1x1 // accept 101
tape #b#b#b#b&1010&1010             // accept 1010
tape #b#b#b#b&1110&1011&0101&1000&0111&0110&0011&0000 // accept 8 possible 0000,...