On Sun, Oct 6, 2013 at 5:05 AM, Christian Muise <christian.mu...@gmail.com> wrote: > >> Proof of concept or not, it's already used by the new assumptions system >> to detect inconsistencies. If you have any suggestions on how to improve the >> algorithm in pure Python, we'd love to hear them. > > > There's always more that can be done ;). I'd say the next obvious step > would be to implement the 1UIP clause learning scheme when a conflict is > found: > - http://en.wikipedia.org/wiki/Constraint_learning > - http://gauss.ececs.uc.edu/SAT/articles/FAIA185-0131.pdf
The code says that is supports simple clause learning, but it seems to always be disabled by default. Do you know why that is? > >> Does MiniSAT have Python bindings? I know of pycosat, which are the python >> bindings of picosat. This is the SAT solver used by the conda package >> manager, which I worked on this summer. > > > Picosat is nice and lightweight (i.e., easy to hack around with), but > MiniSAT is much more established as the heavy hitter in the SAT world. An > example python wrapper: > - https://pypi.python.org/pypi/satispy/1.0a4 OK. We can support many backends, and do benchmarks and pick the best one that is installed. pycosat is nice because, as I mentioned, it is used by conda, so it will always be installed in the Anaconda Python environment for example. > >> >> 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. >> >> >> It seems that these are a replacement for the SAT solver, no? The >> advantage it seems is that they can give information about *why* a fact is >> true or not, or what would be required to make it true. >> >> That sounds cool, but I'm personally more concerned with how to >> effectively do the forward chaining of the facts and how to avoid generating >> expressions that are too large for satisfiable() to solve within a >> reasonable amount of time. Also, how to write the fact generation data down >> in such a way that it's readable, scalable, extensible, and such that we can >> do any reasoning on it that we may wish to do. >> >> Or did I miss the part of ATMSs that would help with that too? > > > I think ATMS' can be used differently than what you describe. With SymPy, > if I knew every assumption that would be used in advance, I could just > pre-compile all of the implied facts and use lookups whenever needed. The > issue is that the assumptions are dynamic, and new chains of inference are > created. ATMS' would maintain the facts derivable given a set of assumptions > (again, this is tending more towards an educated guess since it falls > outside of what I really know). That's basically true. There are two kinds of facts, those free of the expression and those that aren't. An example of a free fact would be Implies(Q.positive, Q.real). This fact is "free" because it doesn't matter what we evaluate the assumption keys at. A non-free fact would be Equivalent(Q.zero(x*y), Or(Q.zero(x), Q.zero(y))). The difficulty with this fact is that the actual concrete fact that matters depends on what Mul objects appear in our expression. If we have an expression with x*y and y*z*t, we need to construct two facts, Equivalent(Q.zero(x*y), Or(Q.zero(x), Q.zero(y))), and Equivalent(Q.zero(y*z*t), Or(Q.zero(y), Q.zero(z), Q.zero(t))). The current new assumptions basically only use the SAT solver for the first kind. After that, they use a bunch of heuristics to try to get at more advanced facts. But the difficulty is that these only work if the expression is in the form expected by the heuristic. You can make ask(Q.zero(x*y), Or(Q.zero(x), Q.zero(y))) work, but ask(Implies(Or(Q.zero(x), Q.zero(y)), Q.zero(x*y)), which is logically the same thing, won't work. > > Bottom line is, if you can find a polynomial way to solve your problem > (even if the solution you find seems shitty in practice), then chances are > there is some specially designed knowledge reasoning technique that would > blow the SAT solving approach out of the water (even if you used the best > SAT solver out there). This falls along the lines of what I was getting at > during my final weeks of the SoC project: > - http://haz-tech.blogspot.com.au/2010/08/soc-wrap-up.html OK, thanks for pointing that out. So I think one thing we can do right away is to try to use some heuristics to avoid the full SAT solver when we don't need it, especially if it ends up being slow. For instance, we can use the known_facts_dict. We can also try solving against free propositions only first before constructing non-free ones. And if all Q keys in question are over the same expression, we can use only the free version. I'm not sure if the general problem will be polynomial. There are some rather complicated facts, which I'm a little worried may grow to be rather large. For instance, if we have a product, like x*y*z, and we know that each term in the product is either positive or negative, then the sign of the product is the parity of the number of negative terms: if there are an even number of negative terms the product is positive, and if there are an odd number of negative terms the sign is negative. The only way I know to represent this last part would be to enumerate the cases, like Implies(Or(Q.negative(x) & Q.positive(y) & Q.positive(z), Q.positive(x) & Q.negative(y) & Q.positive(z), Q.positive(x) & Q.positive(y) & Q.negative(z), ..., Q.negative(x*y*z)). I don't know if this is polynomial or not, but I wouldn't be surprised if it isn't. Another example is facts that say things like, "if you have a product where every term is known to be either rational or irrational, and exactly one of the terms is irrational, then the product is irrational". I guess I'll try implementing these as facts, and if they get too slow, I'll have to think about adding some pre-parsing heuristics similar to the existing handler system, and only fallback to the full power of SAT when it is necessary. I don't really like this plan, though, because we have to be really smart how we write our data, or else we will end up duplicating the fact logic, which is a recipe for disaster because it so easily can lead to contradictory assumptions. Also, I have no idea how things will look when we start to implement some rules for dealing with facts on Adds a la dealing with equalities and inequalities, but I wouldn't be surprised if they end up being fundamentally non-polynomial. Aaron Meurer > > Cheers, > Christian > > -- > 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.
