5 ms·

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 say

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.

philzook 3y ago
You might enjoy ruler https://github.com/uwplse/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.
- c-cube 3y ago
  There's a workshop exploring that: http://www.sc-square.org/CSA/welcome.html http://www.sc-square.org/CSA/welcome.html . They're trying to bridge cas and smt.
Q6T46nT668w6i3m 3y ago
Toy? SymPy has room for improvement but it has made a tremendous impact in research and industry.
- sheepshear 3y ago
  "Toy" is solver jargon that sort of means there's an alternative that blows it out of the water.
bmitc 3y ago
> 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?
StableAlkyne 3y ago
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.
- abdullahkhalids 3y ago
  Miniconda has a better dependency resolver, and it can resolve in less than a minute in most cases.
  - StableAlkyne 3y ago
    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.
    - taeric 3y ago
      250 is not a big number... :(
  - VHRanger 3y ago
    They have the same resolver (Conda) You just have fewer packages installed with miniconda, so the sat problem is much smaller
- scoresmoke 3y ago
  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/ https://mamba.readthedocs.io/
toth 3y ago
Is Mathematica built like this?
- mathisfun123 3y ago
  Yes but I doubt they're using z3 or cvc5 or any other oss sat/smt solver.
  - c-cube 3y ago
    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.
maple3142 3y ago
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.)
- mathisfun123 3y ago
  > 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.
abecedarius 3y ago
Is there an existing CAS built on top of a SAT or SMT solver?
- mathisfun123 3y ago
  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.
  - abecedarius 3y ago
    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.md https://github.com/norvig/paip-lisp/blob/main/docs/chapter15... and https://github.com/norvig/paip-lisp/blob/main/docs/chapter8.md 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.
  - deleted 3y ago
    [deleted]

philzook 3y ago

You might enjoy ruler https://github.com/uwplse/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.

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

Q6T46nT668w6i3m 3y ago

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

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

bmitc 3y ago

> 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?

StableAlkyne 3y ago

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.

abdullahkhalids 3y ago
Miniconda has a better dependency resolver, and it can resolve in less than a minute in most cases.
- StableAlkyne 3y ago
  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.
  - taeric 3y ago
    250 is not a big number... :(
- VHRanger 3y ago
  They have the same resolver (Conda) You just have fewer packages installed with miniconda, so the sat problem is much smaller
scoresmoke 3y ago
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/ https://mamba.readthedocs.io/

toth 3y ago

Is Mathematica built like this?

mathisfun123 3y ago
Yes but I doubt they're using z3 or cvc5 or any other oss sat/smt solver.
- c-cube 3y ago
  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.

maple3142 3y ago

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

mathisfun123 3y ago
> 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.

abecedarius 3y ago

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

mathisfun123 3y ago
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.
- abecedarius 3y ago
  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.md https://github.com/norvig/paip-lisp/blob/main/docs/chapter15... and https://github.com/norvig/paip-lisp/blob/main/docs/chapter8.md 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.
- deleted 3y ago
  [deleted]