Hacker News Reader

Comment by mathisfun123 | Hacker News Reader

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 such time, sympy will remain a toy.

I will say though that symengine is a great project and congrats to that guy for pulling it off under the constraints of a phd.

View on HN

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.

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 :)

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

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

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

Miniconda has a better dependency resolver, and it can resolve in less than a minute in most cases.

Miniconda is faster (I prefer it, personally)...

...but Miniconda and Anaconda are the same package manager, the difference is that Anaconda comes batteries-inclused with a ton of common packages.

The reason Miniconda is faster isn't the solver, it's because it doesn't have 250 packages to go through the long checking process on.

If you have a large, complex environment in Miniconda, that environment will get slower and slower to resolve over time.

250 is not a big number... :(

They have the same resolver (Conda)

You just have fewer packages installed with miniconda, so the sat problem is much smaller

You might enjoy ruler https://github.com/uwplse/ruler

It would be very interesting for SMT and CAS to converge a bit more. SMT in expressiveness and domains and CAS in rigor.

The modality of their usage is different. CAS tends to return some expressions of interest, which it is hard to get SMT to do. Either you get "unsat" or a particular model from an SMT solver, not a simplified expression (ok, z3 has a simplify command, which is pretty cool).

SMT today is not obviously expressive enough to handle most of the domains and questions that come up in CAS systems.

Most SMT solvers do not intrinsically handle transcendental functions or any notions of calculus, abstract algebra, etc.

CAS systems are largely interested in problems of equational reasoning, whereas SMT's bread and butter is gluing together "trivialities" like linear inequalities and congruence closure with SAT search.

There's a workshop exploring that: http://www.sc-square.org/CSA/welcome.html . They're trying to bridge cas and smt.

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.

Is there an existing CAS built on top of a SAT or SMT solver?

oss? none that i'm aware of that use a SAT/SMT solver for the term rewriting (like i'm suggesting). closed source, my strong intuition is both mathematica and magma work this way.

Sounds like a great project idea to make a toy demo of this direction you'd like to see. Maybe comparable to https://github.com/norvig/paip-lisp/blob/main/docs/chapter15... and https://github.com/norvig/paip-lisp/blob/main/docs/chapter8.... which are a few hundred lines of Lisp each, but do enough to be interesting.

Toy? SymPy has room for improvement but it has made a tremendous impact in research and industry.

"Toy" is solver jargon that sort of means there's an alternative that blows it out of the water.

Is Mathematica built like this?

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

Do you have any evidence for that? My impression is that Mathematica is built on a rewriting language along with thousands of built-in procedures (some of which are sat/smt). I don't think its core engine itself is smt.

> core CAS functionality (and performance) should be based on a SAT/SMT engine to discover the rewrite rules

Why is that? What are the alternatives?

Reply on news.ycombinator.com