Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Towards a new SymPy

oscarbenjamin.github.io

Post reply on HN
Print view View original

21–30 of 72 posts

Re: Towards a new SymPy

#21

Post by bouchard »

scoresmoke wrote: post #14
StableAlkyne wrote: post #4

Earlier quoted context omitted.

Not an expert in SAT solvers, personally. What would the benefit be in using one? Anaconda's absurdly slow dependency resolver (it takes up to 15 minutes for things Pip installs in seconds, with no way of disabling it outside of installing a third party solver) is based on SAT and left a bad taste in my mouth for them (slow, clunky, etc), but maybe it's just a poor implementation on their part.

Yes, this is a big disadvantage. But have you tried Mamba that aims at implementing Anaconda more efficiently? It works really well in most cases. https://mamba.readthedocs.io/

You can use mamba's much faster solver directly with conda.

  conda install -n base conda-libmamba-solver
  conda config --set solver libmamba

Re: Towards a new SymPy

#22

Post by StableAlkyne »

scoresmoke wrote: post #14
StableAlkyne wrote: post #4

Earlier quoted context omitted.

Not an expert in SAT solvers, personally. What would the benefit be in using one? Anaconda's absurdly slow dependency resolver (it takes up to 15 minutes for things Pip installs in seconds, with no way of disabling it outside of installing a third party solver) is based on SAT and left a bad taste in my mouth for them (slow, clunky, etc), but maybe it's just a poor implementation on their part.

Yes, this is a big disadvantage. But have you tried Mamba that aims at implementing Anaconda more efficiently? It works really well in most cases. https://mamba.readthedocs.io/

Mamba is great, and I use it when possible. It's probably the single best thing to happen to Anaconda in years. Nowadays it's installed automatically, but up until a month ago you had to deal with the slow solver to install it.

And fortunately it will become the default by Q4!

The point I was making is the old solver left an impression on me that SAT is slow and inefficient, that's all really :)

Re: Towards a new SymPy

#23

Post by bonzini »

StableAlkyne wrote: post #4
mathisfun123 wrote: post #3

The unfortunate thing is that core CAS functionality (and performance) should be based on a SAT/SMT engine to discover the rewrite rules and it goes without saying (but I'll say it anyway) implementing that is "hard". Naively (i.e., I haven't really thought through it), I think sympy should be built on top of z3 or cvc5 or at least very tighly integrated (e.g., support as a backend). And (again naively) I think until…

Not an expert in SAT solvers, personally. What would the benefit be in using one? Anaconda's absurdly slow dependency resolver (it takes up to 15 minutes for things Pip installs in seconds, with no way of disabling it outside of installing a third party solver) is based on SAT and left a bad taste in my mouth for them (slow, clunky, etc), but maybe it's just a poor implementation on their part.

Fedora's dnf also uses SAT and it's way faster (with caching) than the handwritten resolver it replaced.

Re: Towards a new SymPy

#24

Post by mathisfun123 »

StableAlkyne wrote: post #4
mathisfun123 wrote: post #3

The unfortunate thing is that core CAS functionality (and performance) should be based on a SAT/SMT engine to discover the rewrite rules and it goes without saying (but I'll say it anyway) implementing that is "hard". Naively (i.e., I haven't really thought through it), I think sympy should be built on top of z3 or cvc5 or at least very tighly integrated (e.g., support as a backend). And (again naively) I think until…

Not an expert in SAT solvers, personally. What would the benefit be in using one? Anaconda's absurdly slow dependency resolver (it takes up to 15 minutes for things Pip installs in seconds, with no way of disabling it outside of installing a third party solver) is based on SAT and left a bad taste in my mouth for them (slow, clunky, etc), but maybe it's just a poor implementation on their part.

> Anaconda's absurdly slow dependency resolver

On the one hand this is like comparing apples and oranges. On the other hand SAT is slow for dependency management not because the solver itself is slow (it might well be - I don't know which solver they packaged) but because it's an NP-complete problem.

Back to sympy: a computer algebra system (CAS) is primarily (IMHO) an algebra system, not a matrix manipulation library or a pde solver or whatever kitchen sink collection of things is in all of them. Algebra in this context means manipulating algebraic expressions and that's term rewriting and that's also NP-complete (well at least in some form or fashion, eg egraph extraction).

So in summary - there's no way out of using SAT/SMT here.

> slow, clunky, etc

Just to put a finer point on this - it's a very shallow thing to look at conda's or whomever's implementation and then paint over SAT/SMT with that same brush. The way that I usually describe z3 is that it is nuclear weapons grade industrial software. I mean jesus christ its stated goal is solving NP complete/hard problems and it frequently succeeds at this goal on problems with millions of decision variables and clauses. It is absolutely the highest tech piece of tech out there (XYZ pytorch/tensorflow ai ml thing pales in comparison) and we are all extremely lucky that it is licensed permissively and developed completely in the open (and basically by one guy!). And it is being used in many many places for very serious engineering.

Re: Towards a new SymPy

#25

Post by mathisfun123 »

toth wrote: post #8
mathisfun123 wrote: post #3

The unfortunate thing is that core CAS functionality (and performance) should be based on a SAT/SMT engine to discover the rewrite rules and it goes without saying (but I'll say it anyway) implementing that is "hard". Naively (i.e., I haven't really thought through it), I think sympy should be built on top of z3 or cvc5 or at least very tighly integrated (e.g., support as a backend). And (again naively) I think until…

Is Mathematica built like this?

Yes but I doubt they're using z3 or cvc5 or any other oss sat/smt solver.

Re: Towards a new SymPy

#26

Post by [deleted] »

viscousviolin wrote: post #20
staunton wrote: post #18

Earlier quoted context omitted.

That's an entirely different thing though. Good luck getting Lean to help you do any symbolic computation whatever. You can use it to prove that a given manipulation is correct. You cannot use it to find a result (there may be a symbolic math library for Lean eventually but currently there isn't).

That's not my point. In the comment I made below the other post I talked about how Mathlib is just a piece of the puzzle, the way I see it [0]. I don't want to see Lean do symbolic computation - although I'm sure that would be great as well - what I want to see is to have Mathlib's library of mathematics being used in a way that any CAS can read definitions and theorems from it. Then a significant part of the CAS cod…

[deleted]

Re: Towards a new SymPy

#27

Post by maple3142 »

mathisfun123 wrote: post #3

The unfortunate thing is that core CAS functionality (and performance) should be based on a SAT/SMT engine to discover the rewrite rules and it goes without saying (but I'll say it anyway) implementing that is "hard". Naively (i.e., I haven't really thought through it), I think sympy should be built on top of z3 or cvc5 or at least very tighly integrated (e.g., support as a backend). And (again naively) I think until…

I am not sure current SAT solver is good at solving things that a good CAS can do. It is fast at a lot of operations related to bits (xor, shift, and, or ...) but it performs way worse for things like solving a linear system in a finite field. (This is all from my personal experiences, so I may be wrong.)

Re: Towards a new SymPy

#29

Post by mathisfun123 »

maple3142 wrote: post #27
mathisfun123 wrote: post #3

The unfortunate thing is that core CAS functionality (and performance) should be based on a SAT/SMT engine to discover the rewrite rules and it goes without saying (but I'll say it anyway) implementing that is "hard". Naively (i.e., I haven't really thought through it), I think sympy should be built on top of z3 or cvc5 or at least very tighly integrated (e.g., support as a backend). And (again naively) I think until…

I am not sure current SAT solver is good at solving things that a good CAS can do. It is fast at a lot of operations related to bits (xor, shift, and, or ...) but it performs way worse for things like solving a linear system in a finite field. (This is all from my personal experiences, so I may be wrong.)

> linear system in a finite field

I said it below, but I'll repeat it here: in my humble opinion, this is not what you want from a CAS. This is functionality better delegated to a BLAS (yes even with the finite field qualifier). And just because both CAS and BLAS have A in them, does not mean they are the same thing.

Re: Towards a new SymPy

#30

Post by logicchains »

staunton wrote: post #18
viscousviolin wrote: post #12

Earlier quoted context omitted.

How about Lean? [0] There's a whole library of mathematics written down in Lean called Mathlib, which spans most of the undergraduate maths curriculum upto some cutting edge research-level maths. I've commented under the Part II post you linked to as well, describing how I think Mathlib could help the CAS ecosystem. [0] https://leanprover-community.github.io/

That's an entirely different thing though. Good luck getting Lean to help you do any symbolic computation whatever. You can use it to prove that a given manipulation is correct. You cannot use it to find a result (there may be a symbolic math library for Lean eventually but currently there isn't).

In Coq, the tactics system supports writing solvers than can both find a result and give you the proof that it's correct. If Lean also has a similar tactics system, then solvers could be written in that.
Post reply on HN