Add docstrings to sat solver.
Remove unnecessay copy in sat solver.
Separate check from thread queueing.

Reasons:
- faster execution but greater variance from upper bound.