Improved pl_true

1. Completely refactored pl_true to use subs.
2. Added parameter 'deep' which can return better results in case of partial interpretations.
This code is a little more intelligent that the original code such that it can detect either tautology or unsatisfiability under partial assignment using 1 SAT call.
```python
>>> pl_true((A | B) & ~A, {B: False}, deep=True)
False
```
In the above example, given the partial model, the expr becomes unsatisfiable (or in some other case tautological). Setting the deep parameter detects these conditions and returns a more accurate answer under the given model.