How does one enter in a boolean expression into an SAT solver?
Typically, the huge SAT instance is generated by a reduction from some other problem, so it's computer-generated in the first place.  You write it to a file and tell the SAT solver to read it.