0
$\begingroup$

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..

$\endgroup$
2
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.