How does one enter in a boolean expression into an SAT solver? For example, if we had an extremely large expression, how do we even first get it into the program? I can't imagine entering each clause in one by one..
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.