In case of a Sematic Tableau, an open branch (not containing conflicting literals) is a proof of satisfiability. In other words, if all branches close, the formula is _definitely_ unsatisfiable. So checking for validity would mean checking for the unsatisfiability of the negation. If assumptions don't require models in the general case, then this method makes sense. And since its a DFS over the semantic tree, the overheads may not be much (or we can try out an iterative version too). But if we DO require models, then a traditional SAT solver is the way to go.
On Sun, Feb 23, 2014 at 10:17 PM, Aaron Meurer <asmeu...@gmail.com> wrote: > > 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 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+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.
