opened
ShubhamKJha
username_0
<!-- Your title above should be a short description of what
was changed. Do not include the issue number in the title. -->

#### References to other Issues or PRs
<!-- If this pull request fixes an issue, write "Fixes #NNNN" in that exact
format, e.g. "Fixes #1234". See
https://github.com/blog/1506-closing-issues-via-pull-requests . Please also
write a comment on that issue linking back to this pull request once it is
open. -->
Closes #9728. Build over #9813

#### Brief description of what is fixed or changed
This is an attempt to add [pycosat](https://pypi.org/project/pycosat/) as a soft dependency for SymPy.
#### Other comments
* [ ] Make tests pass

#### Release Notes

<!-- Write the release notes for this release below. See
https://github.com/sympy/sympy/wiki/Writing-Release-Notes for more information
on how to write release notes. The bot will check your release notes
automatically to see if they are formatted correctly. -->

<!-- BEGIN RELEASE NOTES -->
* logic
   * Added pycosat as an optional dependency to improve performance while solving SAT problems.
<!-- END RELEASE NOTES -->
Add pycosat as an optional dependency.
issue
created
ShubhamKJha
username_0
ping @username_2 @jksuom @oscarbenjamin, this is ready for review.
comment
created
oscargus
username_1
Are we sure that this is tested? Right now, it seems like it is only the doctests that possibly tests this. (But, of course, also the general tests may fall back to this.)

I think that you may to point out the tests in test_travis.sh, either just add them to the dependency section, or create a new explicit test run (as is done for e.g. Matplotlib).

Also, maybe one can clarify the doc-string for `satisfiable` which options are available for `algorithm` and how it works with the default value.

In general though: looks good! Do you have any numbers on possible speed-ups?
comment
created
asmeurer
username_2
I'd also be curious to see performance numbers. When I checked this before, it didn't help as much as I had hoped.
comment
created
asmeurer
username_2
You need to add assumptions and logic to the optional dependencies tests in test_travis.sh.
comment
created
ShubhamKJha
username_0
Using this,
```py
from sympy import *
import pyinstrument
profiler = pyinstrument.Profiler()
from sympy.abc import x 

# r = random_poly(x, 100, -100, 100)
r = -97*x**100 + 17*x**99 + 59*x**98 - 84*x**97 - 86*x**96 + 7*x**95 + 73*x**94 + 19*x**93 + 91*x**92 + 83*x**91 + 90*x**90 + 81*x**89 - 20*x**88 + 35*x**87 - 38*x**86 + 95*x**85 - 16*x**84 - 36*x**83 - 20*x**82 + x**81 + 84*x**80 + x**79 - 17*x**78 - 41*x**77 + 39*x**76 - 62*x**75 + 40*x**74 - 39*x**73 - x**72 + 81*x**71 - 17*x**70 - 63*x**69 + 10*x**68 + 21*x**67 - 56*x**66 - 43*x**65 + 96*x**64 + 26*x**63 + 55*x**62 + 90*x**61 - 12*x**60 + 72*x**59 - 74*x**58 + 98*x**57 - 98*x**56 - 25*x**55 + 91*x**54 + 7*x**53 + 67*x**52 + 30*x**51 + 59*x**50 - 94*x**49 + 32*x**48 + 51*x**47 - 30*x**46 - 23*x**45 - 50*x**44 - 41*x**43 - 88*x**42 + 60*x**41 - 100*x**40 - 31*x**39 + 32*x**38 + 20*x**37 - 52*x**36 + 25*x**35 - 93*x**34 + 86*x**32 - 17*x**31 + 52*x**30 - 92*x**29 + 80*x**28 + 29*x**27 + 54*x**26 + 2*x**25 - 88*x**24 + 79*x**23 + 6*x**22 + 97*x**21 - 74*x**20 - 37*x**19 - 44*x**18 - 2*x**17 + 54*x**16 + 5*x**15 + 25*x**14 + 80*x**13 + 43*x**12 - 88*x**11 + 37*x**10 - 85*x**9 + 87*x**8 - 84*x**7 + 66*x**6 + 44*x**5 + 36*x**4 - 69*x**3 + 71*x**2 + 43*x + 82

profiler.start()
ans = ask(Q.positive(r), Q.positive(x))
profiler.stop()

print(profiler.output_text())
```

The performance is like, (since it only affects the SAT solving part)
```
# In master
   |  |                 `- 0.145 to_NNF  sympy/assumptions/cnf.py:102
   |  `- 0.631 check_satisfiability  sympy/assumptions/satask.py:30
   |     `- 0.607 satisfiable  sympy/logic/inference.py:38
   |        `- 0.607 dpll_satisfiable  sympy/logic/algorithms/dpll2.py:21
   |           |- 0.325 __init__  sympy/logic/algorithms/dpll2.py:84
   |           |  `- 0.281 _initialize_clauses  sympy/logic/algorithms/dpll2.py:140
   |           `- 0.281 _find_model  sympy/logic/algorithms/dpll2.py:165
   |              `- 0.101 _simplify  sympy/logic/algorithms/dpll2.py:421
   |                 `- 0.096 _unit_prop  sympy/logic/algorithms/dpll2.py:450

# With pycosat
   |  |              `- 0.092 <setcomp>  sympy/assumptions/cnf.py:348
   |  `- 0.122 check_satisfiability  sympy/assumptions/satask.py:30
   |     `- 0.098 satisfiable  sympy/logic/inference.py:39
   |        `- 0.096 pycosat_satisfiable  sympy/logic/algorithms/pycosat_wrapper.py:11
```
comment