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..
How does one enter in a boolean expression into an SAT solver?
computability;np complete