With my work with the assumptions, I am able to keep it as CNF, or nearly CNF, although in some cases, I have to be careful how I do things. For example, there are simple CNF and DNF forms for "exactly one of x1, ..., xn is true". You need to use the DNF one if it is the first part of an implication and the CNF form if it is the second (because p >> q == q | ~p). See https://github.com/asmeurer/sympy/blob/newassump/sympy/assumptions/newhandlers.py#L163.
There expression passed to satisfiable is basically a large And, mostly of implications. They are often something like x | And(...) (i.e., x >> And(...) or some similar), meaning it is necessary to do a very small distribution. So far, this hasn't seemed to be an issue. One thing I am not sure how to do is "an even number of x1, ..., xn is true" (n-ary XOR). CNF or DNF of this is exponential. But unfortunately some facts are like this (e.g., if you know that each of x1, ..., xn is positive or negative, then x1*...*xn is positive iff an even number are negative). My best thought for this is to just put a limit in the code for how large it tries to get. For now, though, I think it would be great if I basically didn't have to worry about using the correct form of a fact to get good performance. That will make it a lot easier for people to extend the system in the future, without having to have a deep knowledge of logic. Aaron Meurer On Sat, Feb 1, 2014 at 6:25 PM, Christian Muise <christian.mu...@gmail.com> wrote: > Two big CNF expressions with an OR tying them together is just a special > case I reckon. We'll start to face feature creep with all of the different > types of input that might be used -- ultimately what is needed is an > assessment of the types of input the satisfiable function actually sees. > There will /always/ be some other corner case that you can solve better, but > it's not worth the effort unless that corner case is commonly used. > > Cheers, > Christian > > > On Sat, Feb 1, 2014 at 11:22 AM, Aaron Meurer <asmeu...@gmail.com> wrote: >> >> I disagree about the symmetry. Consider the case if you have Or(big >> expression 1, big expression 2). Instead of trying to convert the >> whole thing into CNF or DNF, you can recursively apply the algorithm. >> First just try satisfiable(big expression 1). If it's satisfiable, >> that's your model. If not, then apply satisfiable(big expression 2). >> >> Superficially, it doesn't matter what the args are to do this. In >> reality it might be more efficient to convert the whole thing to CNF >> instead of doing this, or applying some other heuristic. So it would >> need to be balanced. >> >> But this again is something I am not sure about. Would it be a bad >> idea to unconditionally have something like >> >> def satisfiable(expr): >> if isinstance(expr, Or): >> return any(satisfiable(i) for i in expr.args) >> else: >> return dpll2(to_cnf(expr)) # or whatever >> >> Aaron Meurer >> >> On Fri, Jan 31, 2014 at 11:44 AM, Sachin Joglekar >> <srjoglekar...@gmail.com> wrote: >> > Agree with Christian. However, we would need a very good heuristic to >> > calculate how 'far' a formula is from CNF or DNF. Frankly, if the number >> > of >> > variables is small, I don't think any method would be that bad - like >> > for >> > even 6-7 variables, the number of models would be at max 64-128 - a >> > decent >> > number to iterate over directly. >> > But as Aaron suggests, maybe we don't want to add too much of >> > complexity? In >> > that direction, I do think we should deprecate dpll1. dpll2, with clause >> > learning involved, is certainly better. >> > >> > >> > On Friday, January 31, 2014 12:37:09 PM UTC+5:30, Christian Muise wrote: >> >> >> >> If the formulae are small, then the approach there is just fine. If >> >> the >> >> formulae is huge but the number of variables small, then just >> >> enumerating >> >> the models should be done. If neither of those cases hold, then the >> >> best you >> >> could hope for is to try and detect "how far" the input is from either >> >> CNF >> >> or DNF (note -- a way to predict one could be used to predict the >> >> other). >> >> With that in hand, you can do the following: >> >> - if easy to convert to DNF, do so (at least partially) until at least >> >> one >> >> term is produced >> >> - else if easy to convert to CNF, do so and run the SAT procedure >> >> - else convert to CNF with tseitin and run the SAT procedure >> >> >> >> Cheers, >> >> Christian* >> >> >> >> *: Can be considered a pseudo-expert on the subject, as I've done >> >> graduate >> >> work in the area and had a hand in implementing the current DPLL solver >> >> in >> >> sympy. >> >> >> >> >> >> On Fri, Jan 31, 2014 at 12:04 PM, Aaron Meurer <asme...@gmail.com> >> >> wrote: >> >>> >> >>> I would time the various ways. Unless someone really understands the >> >>> theory of DPLL well to know what will and won't be fast, I think this >> >>> is the only way we can know what tricks to use when. >> >>> >> >>> In general, though, if something is only faster for very small inputs, >> >>> it's not really worth doing, because it's already not slow the way it >> >>> is. It only serves to add unnecessary complexity. >> >>> >> >>> By the way, a good GSoC idea for someone would be to set up a good >> >>> benchmarking system for us. We are good at avoiding behavioral >> >>> regressions with testing and Travis, but performance regressions are >> >>> tougher to guard against, because we don't check it very often. >> >>> >> >>> Aaron Meurer >> >>> >> >>> On Thu, Jan 30, 2014 at 7:29 AM, Sachin Joglekar >> >>> <srjogl...@gmail.com> wrote: >> >>> > This may seem like an ad-hoc way of doing things, but can we think >> >>> > of >> >>> > using >> >>> > DNF for satisfiability of formulae with small number of atoms? Since >> >>> > DNF >> >>> > generally causes an extremely dangerous explosion in the size of an >> >>> > expression, its use to check satisfiability is usually frowned upon >> >>> > by >> >>> > the >> >>> > logic community. However, checking the SAT of a DNF is trivial. >> >>> > Therefore, >> >>> > since _we_ can check for the number of atoms used in a given >> >>> > expression, can >> >>> > we just use the DNF method when the number of atoms falls below a >> >>> > certain >> >>> > threshold (say 5 or 6)? >> >>> > @asmeurer, what do you think? >> >>> > >> >>> > >> >>> > On Wed, Jan 29, 2014 at 4:41 PM, Soumya Biswas <sdb...@gmail.com> >> >>> > wrote: >> >>> >> >> >>> >> It seems somehow I had missed this conversation (on the issues >> >>> >> page). >> >>> >> It >> >>> >> is definitely true that this transformation adds many auxiliary >> >>> >> variables >> >>> >> (as many as the number of non-atomic clauses). However what I am >> >>> >> working on >> >>> >> is to optimize this encoding to such an extent that the encoding >> >>> >> plus >> >>> >> satisfiability time is reduced overall. Firstly (as observed on the >> >>> >> issues >> >>> >> thread) handling duplicate subexpressions optimizes the process to >> >>> >> some >> >>> >> extent. Additionally, I worked out a way (I don't know if it is an >> >>> >> obvious >> >>> >> generalization or something new) such that And(a, b, c, ...) can be >> >>> >> treated >> >>> >> as only one operator (though the number of clauses this encoding >> >>> >> will >> >>> >> produce will still increase linearly with the number of arguments). >> >>> >> This is >> >>> >> what makes the method much faster for cases where the average >> >>> >> number >> >>> >> of >> >>> >> arguments to And/Or is around 3 (or more). I find the point made in >> >>> >> the >> >>> >> issues page to be quite interesting that many of the encodings are >> >>> >> quite >> >>> >> redundant. Will look into optimization from this approach. There is >> >>> >> yet >> >>> >> another polarity based optimization, that I am yet to look into. I >> >>> >> think we >> >>> >> will have to look at encoding plus solving as the unit of >> >>> >> comparison >> >>> >> i.e. is >> >>> >> the entire process faster or slower. >> >>> >> >> >>> >> -- >> >>> >> You received this message because you are subscribed to a topic in >> >>> >> the >> >>> >> Google Groups "sympy" group. >> >>> >> To unsubscribe from this topic, visit >> >>> >> https://groups.google.com/d/topic/sympy/wknFPGmTw0w/unsubscribe. >> >>> >> To unsubscribe from this group and all its topics, send an email to >> >>> >> sympy+un...@googlegroups.com. >> >>> >> >> >>> >> To post to this group, send email to sy...@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+un...@googlegroups.com. >> >>> > To post to this group, send email to sy...@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+un...@googlegroups.com. >> >>> To post to this group, send email to sy...@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. >> >> -- >> 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. -- 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.
