So uhm, I wrote a sketch of a Turing Machine for SAT

sat_turing_machine.py

# pseudo-assembly for a turing machine

# tape layout for SAT problem in nvar variables with CNF of length len
# (convenient to assume len >= nvar to make a single measure of complexity)
# we will be deleting clauses as we go, but otherwise the tape stays constant

# nvar variables, 3 bits each
nvar * <notSIGIL=0><mut mark=0><value>
# sigil separating variable table from CNF
<SIGIL=1>
# len=sum(for i in Clen: Dlen_i) CNF atoms
# each inner (disjunctive) clause starts with a 1
# (so we can read a nat forwards and back and stop
# when we see a <1X> pair of bits)
# each outer (conjunctive) clause starts with a 0
mut Clen *
  (for i in Clen: mut Dlen_i *
    <noEOF=0><D=1><not><var:nat…><endOfNat=1><notSIGIL=0>
  )
  <noEOF=0><C=0>
# end of tape
<EOF=1>

# alias: unary representation of nats
# interlaved with 0 bits
# padded with 1 flags for constant size for copying/deleting
# horrible encoding, but simple and effective
<var:nat…> =
  (nvars - var) * <notEndOfNat=0><accountedFor=1>
  var * <notEndOfNat=0><mut accountedFor=0>

# subroutines:

def main(), in O(nvar^2 * len^3) = O(len^5):
  1. seek to <SIGIL>, in O(nvar)
  2. tailcall loop(), in O(nvar^2 * len^3)
def loop(), in O(nvar^2 * len^3):
  1. call lookup(), in O(nvar^2)
  2. call compress(value), in O(nvar^2 * len^2)
  3. tailcall loop()

def compress(value: BOOL), in O(nvar^2 * len^2) = O(len^4):
  1. start at SIGIL
  2. skip <noEOF=0><D=1> # we were just processing an atom
  3. read <not>
  4. result := value XOR not
  5. delete this atom, in O(nvar^2 * len)
  6. if result: delete the other atoms in this disjunctive clause, in O(nvar^2 * len^2)
  7. return result # this goes to a single well-defined state in loop()

# by deleting, I mean copying all the rest of the CNF up by one atom O(nvar^2 * len),
# (copy O(nvar) bits across O(nvar) distance, O(len) times for each atom)
# so that we are always operating on the head atom right after sigil
# and eat this cost that depends on len in this subroutine,
# as opposed to every time we traverse the tape looking for a variable

def lookup(), in O(nvar^2):
  01. precondition: all variables are unmarked
  02. start at SIGIL
  03. read <EOF=1|noEOF=0>
  04. if EOF: exit(1) # verified true, no conjunctive clause was falsified
  05. read <D=1|C=0>
  06. if C: exit(0) # verified false, false disjunctive clause among conjuctive clauses
  07. skip <not>
  08. for each successor in <var:nat…> (i.e. each pair of bits in the encoding),
      we want to mark the second bit, then turn around and mark one more var
      on the other side (the last unmarked one), in O(nvar^2)
  09. when we’ve marked all bits, seek back to the last unmarked var, in O(nvar)
  10. read its <value>
  11. read forward to SIGIL, unmarking variables as you go, in O(nvar)