On Fri, Jan 24, 2014 at 1:35 AM, Soumya Biswas <[email protected]> wrote: > Hello > > There are a couple of things present in the Logic module that I would like > to discuss: > > 1. Ask Function in PropKB: > If KB 'A' entails formula 'B' then A U {~B} is unsatisfiable. However the > current code seems to check if A U {B} is satisfiable. To the best of my > understanding, this will give the right answer in many case, but not all.
Can you point to the specific part of the code that you're referring to? Anyway, I'm not sure what PropKB is supposed to do. A simple grep shows that it's not used anywhere. I'm guessing it's a leftover from before the dpll algorithm was implemented, and should be removed if that's the case. The function you should focus on is satisfiable(), and the algorithms it calls. Aaron Meurer > > 2. Ask Function on a PropKB with no clauses: > The function returns False if there are no clauses. Theoretically, an empty > clause is unsatisfiable but empty clause set is valid. Hence, it is > satisfiable in all interpretations. So it only entails formulas that are > satisfiable in all interpretation i.e. valid. So shouldn't an empty KB > entail a tautology? > > 3. DNF Satisfiability: > As discussed before, the time taken by to_cnf is actually more than the time > taken by the SAT solver. A relatively quick and dirty way to decide whether > the formula resembles CNF or DNF can be to compare the number of conjuncts > and disjuncts present in the formula. This seems to be giving reasonable > results. So, I want to change the code to do this: If more conjunctive then > dpll, else dnf sat. DNF Satisfiability seems to be a linear problem and > would be easier to compute. Is this okay? > > I am done with the code for the above issues and will send a PR once someone > confirms my ideas. > > -- > 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 [email protected]. > To post to this group, send email to [email protected]. > 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 [email protected]. To post to this group, send email to [email protected]. Visit this group at http://groups.google.com/group/sympy. For more options, visit https://groups.google.com/groups/opt_out.
