I'm scrambling at a new post-doc spot, so I don't have much time to join in the discussion, but wanted to mention a few things that came to mind:
1. SAT solvers are indeed mighty beasts. They can solve things you'd never expect them to be able to in mere milliseconds (if configured right). 2. The SAT solver implemented in SymPy is proof-of-concept, and although it is much better than what was there before it is much worse than what you could achieve with a wrapper around a C++ implementation that exists. 3. If you're going to use an external solver, look into MiniSAT, and try to interface with it at an API level (rather than calling it on the command line). I think there is already precedence for this, and it would be essential if you call the solver many times. 4. Rather than re-invent the wheel, I've long believed that what SymPy really needs is an adequately implemented Assumption Based Truth Maintenance System (it even sounds right ;)). This is some preliminary info on the topic: - http://en.wikipedia.org/wiki/Reason_maintenance - http://www.cis.temple.edu/~giorgio/cis587/readings/tms.html - http://www.ise.bgu.ac.il/faculty/kalech/MBD/ATMS_5.ppt -- Note: We start to leave my area of expertise with ATMS' -- I only know of them peripherally. Cheers, Christian On Sun, Oct 6, 2013 at 4:43 AM, Brian Granger <elliso...@gmail.com> wrote: > Yeah!!! > > On Fri, Oct 4, 2013 at 10:35 PM, Aaron Meurer <asmeu...@gmail.com> wrote: > > Hi all. > > > > I got bored, so I spent this evening hacking together a proof of > > concept for the new assumptions system, based on my ideas from > > https://code.google.com/p/sympy/issues/detail?id=3929. The code is at > > https://github.com/sympy/sympy/pull/2508. > > > > Basically, I realised this summer when I was hacking on the > > assumptions that the way the handlers currently work is fundamentally > > broken. For instance, if you do something like ask(Q.zero(x*y), > > Q.zero(x)), the way the handlers currently work is they see the > > Q.zero(x*y), and they know that this means Q.zero(x) or Q.zero(y), so > > they basically say "if any(ask(Q.zero(i)) for i in (x*y).args): return > > True". This works fine, except if you then do something a little more > > complicated, like ask(Q.zero(x*y), Q.zero(x) | Q.zero(y)), it falls > > apart, because neither ask(Q.zero(x)) nor ask(Q.zero(y) is true. What > > *is* true is that at least one of them is true. But since the logic in > > the handlers is done as a Python "or", not a SymPy "Or", there's no > > way to represent this. > > > > What I also learned this summer is that SAT solvers are awesome, and > > if your problem can be solved by one, you should do as little work as > > possible and basically let the SAT solver do the heavy lifting. Well, > > SymPy has a SAT solver, accessible from the satisfiable() function, so > > I realized that this problem (ask(Q.zero(x*y), Q.zero(x) | Q.zero(y))) > > could be solved using one, by simply knowing the fact > > Equivalent(Q.zero(x*y), Q.zero(x) | Q.zero(y)). > > > > At https://github.com/sympy/sympy/pull/2508, I've implemented this > > idea. The most annoying thing I've found when working with the new > > assumptions is that the code is very complicated, especially the code > > in ask.py, so instead of spending all night trying to understand it, I > > opted for the funner way that actually involved writing new code, > > which was to write a proof of concept from scratch. This code doesn't > > use anything from ask.py (except for the Q object of course). The > > result is that only those assumptions that I have manually entered > > will work, which are basically the obvious relationships between real, > > positive, zero, and nonzero, and the one non-trivial fact about a > > multiplication being zero if and only if one of the terms is zero. The > > good news is that the code for newask() is incredibly simple to > > understand (I think). > > > > To get you excited about what's possible, here are some simple things > > that work with newask() that don't work with ask(): > > > >>>> from sympy.assumptions.newask import newask > >>>> newask(Q.zero(x) | Q.zero(y), Q.zero(x*y)) > > True > >>>> newask(Implies(Q.zero(x), Q.zero(x*y))) > > True > >>>> newask(Q.zero(x) | Q.zero(y), Q.nonzero(x*y)) > > False > >>>> ask(Q.zero(x) | Q.zero(y), Q.zero(x*y)) > >>>> ask(Implies(Q.zero(x), Q.zero(x*y))) > >>>> ask(Q.zero(x) | Q.zero(y), Q.nonzero(x*y)) > > > >>>> newask(Q.zero(x*y), Q.zero(x) | Q.zero(y)) > > True > >>>> ask(Q.zero(x*y), Q.zero(x) | Q.zero(y)) > >>>> newask(Q.zero(x*y*z), Q.zero(x) | Q.zero(y)) > > True > >>>> ask(Q.zero(x*y*y), Q.zero(x) | Q.zero(y)) > >>>> > > > > and more importantly, as noted above, it is very difficult to > > impossible to make these work with ask(), because it doesn't know how > > to deal with implications with non-atomic premises, basically. > > > > Also note how I am able to ask what is basically the same thing in > > three different ways, and get the right answer in every case. Even if > > we could hack together something to make ask(Q.zero(x*y), Q.zero(x) | > > Q.zero(y)) work, ask(Implies(Q.zero(x), Q.zero(x*y)) or ask(Q.zero(x) > > | Q.zero(y), Q.zero(x*y)) might not (note that this second one > > wouldn't, because it is the reverse implication; but in newask, it's > > as easy as using Equivalent instead of Implies). > > > > So I'd like some feedback. It's getting late now, so hopefully I > > haven't written anything stupid as my brain is starting to shut down. > > I'd particularly like some feedback on how to structure the API for > > this, since what I have now is completely hacked together and won't > > scale at all. Please read the commit messages on my pull request if > > you want more information. > > > > Aaron Meurer > > > > -- > > You received this message because you are subscribed to the Google > Groups "sympy" group. > > To unsubscribe from this group and stop receiving emails from it, send > an email to sympy+unsubscr...@googlegroups.com. > > To post to this group, send email to sympy@googlegroups.com. > > Visit this group at http://groups.google.com/group/sympy. > > For more options, visit https://groups.google.com/groups/opt_out. > > > > -- > Brian E. Granger > Cal Poly State University, San Luis Obispo > bgran...@calpoly.edu and elliso...@gmail.com > > -- > You received this message because you are subscribed to the Google Groups > "sympy" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to sympy+unsubscr...@googlegroups.com. > To post to this group, send email to sympy@googlegroups.com. > Visit this group at http://groups.google.com/group/sympy. > For more options, visit https://groups.google.com/groups/opt_out. > -- You received this message because you are subscribed to the Google Groups "sympy" group. To unsubscribe from this group and stop receiving emails from it, send an email to sympy+unsubscr...@googlegroups.com. To post to this group, send email to sympy@googlegroups.com. Visit this group at http://groups.google.com/group/sympy. For more options, visit https://groups.google.com/groups/opt_out.
