Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add pycosat as an optional dependency. #17440

Merged
merged 23 commits into from Aug 22, 2019
Merged

Add pycosat as an optional dependency. #17440

merged 23 commits into from Aug 22, 2019

Conversation

@ShubhamKJha
Copy link
Member

@ShubhamKJha ShubhamKJha commented Aug 17, 2019

References to other Issues or PRs

Closes #9728. Build over #9813

Brief description of what is fixed or changed

This is an attempt to add pycosat as a soft dependency for SymPy.

Other comments

  • Make tests pass

Release Notes

  • logic
    • Added pycosat as an optional dependency to improve performance while solving SAT problems.
@sympy-bot
Copy link

@sympy-bot sympy-bot commented Aug 17, 2019

Hi, I am the SymPy bot (v147). I'm here to help you write a release notes entry. Please read the guide on how to write release notes.

Your release notes are in good order.

Here is what the release notes will look like:

This will be added to https://github.com/sympy/sympy/wiki/Release-Notes-for-1.5.

Note: This comment will be updated with the latest check if you edit the pull request. You need to reload the page to see it.

Click here to see the pull request description that was parsed.

<!-- 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
* [x] 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 -->

Update

The release notes on the wiki have been updated.

@ShubhamKJha ShubhamKJha force-pushed the pycosat branch 2 times, most recently from 8267cc7 to c88b4e6 Aug 17, 2019
@ShubhamKJha
Copy link
Member Author

@ShubhamKJha ShubhamKJha commented Aug 18, 2019

ping @asmeurer @jksuom @oscarbenjamin, this is ready for review.

@oscargus
Copy link
Contributor

@oscargus oscargus commented Aug 20, 2019

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?

algorithm = "pycosat"
else:
# Silently fall back to dpll2 if pycosat
# is not installed
Copy link
Member

@asmeurer asmeurer Aug 20, 2019

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

If the algorithm is given explicitly as "pycosat" it should raise an exception in this case.

@asmeurer
Copy link
Member

@asmeurer asmeurer commented Aug 20, 2019

I'd also be curious to see performance numbers. When I checked this before, it didn't help as much as I had hoped.

@asmeurer
Copy link
Member

@asmeurer asmeurer commented Aug 20, 2019

You need to add assumptions and logic to the optional dependencies tests in test_travis.sh.

…if algorithm is defined pycosat explicitly in satisfiable
@ShubhamKJha
Copy link
Member Author

@ShubhamKJha ShubhamKJha commented Aug 21, 2019

I'd also be curious to see performance numbers.

Using this,

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

@@ -227,6 +234,15 @@ EOF
unset USE_SYMENGINE
fi

if [[ "${TEST_OPT_DEPENDENCY}" == *"pycosat"* ]]; then
Copy link
Member

@asmeurer asmeurer Aug 21, 2019

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is already done by the above 5688c89#diff-97e2e3c68308a6044377595c72c26cedR199

Copy link
Member

@asmeurer asmeurer Aug 21, 2019

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I guess you removed those lines. Having it in those lists is the correct way, with a single test/doctest run for all the modules that use optional dependencies.

Copy link
Member Author

@ShubhamKJha ShubhamKJha Aug 22, 2019

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ok, done

@@ -187,6 +191,9 @@ doctest_list = [
# codegen
'sympy/codegen/',
# pycosat
'sympy/logic',
Copy link
Member

@asmeurer asmeurer Aug 21, 2019

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Add assumptions here too.

@ShubhamKJha ShubhamKJha reopened this Aug 22, 2019
@codecov
Copy link

@codecov codecov bot commented Aug 22, 2019

Codecov Report

Merging #17440 into master will increase coverage by 0.116%.
The diff coverage is 10.638%.

@@              Coverage Diff              @@
##            master    #17440       +/-   ##
=============================================
+ Coverage   74.708%   74.825%   +0.116%     
=============================================
  Files          632       632               
  Lines       164360    164140      -220     
  Branches     38576     38708      +132     
=============================================
+ Hits        122791    122818       +27     
+ Misses       36185     35985      -200     
+ Partials      5384      5337       -47

@asmeurer asmeurer merged commit 99c6670 into sympy:master Aug 22, 2019
2 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Linked issues

Successfully merging this pull request may close these issues.

7 participants