On Feb 23, 2014, at 10:26 AM, Sachin Joglekar <srjoglekar...@gmail.com> wrote:
Adding a 'deep' parameter to pl_true seems a better idea. We wouldn't want to break backwards compatibility for users who may have written code assuming the former input/output combos of pl_true. But yes, the modification you suggest to pl_true does seem a good idea to me. About the idea of using a Semantic Tableau, we should probably stick to using a traditional SAT solver for the logic module (Since users looking to use a SAT solver usually need it to return a model, or atleast expect it to). However, what we _can_ do is use the tableau method for the Assumptions system (maybe) - or anywhere else in the core, where a model is not essential. @asmeurer, do you think we should implement that? I don't know a ought about it to say. I can confirm that in the assumptions, the model is not important. Also, satisfiable is called twice in the assumptions system, once to see if the expression can be true and once to see if it can be false. In the cases where it returns an answer (not None), one of the two is unsatisfiable. Do semantic tableaux give proofs of unsatisfiability? That could be useful to the user in some cases, even in the assumptions, to answer 'why' (the model is also important for this). Aaron Meurer @Soumya, you could probably run a few tests and check out the timing results. But before that, you may want to get your current pipeline-PRs merged. I guess there are 2-3 of them? -- 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.
