Ondrej has a branch that uses pycosat in SymPy. But I think we found for the problems I've tried so far in my newassump branch it didn't really make a difference. That could change if they get larger, though.
Aaron Meurer On Fri, Jan 24, 2014 at 9:22 PM, Sachin Joglekar <[email protected]> wrote: > @Aaron, I don't think getting rid of PropKB is a good idea. But what IS > needed is to make sure its foolproof. A PropKB(propositional knowledge base) > is essentially a tool to check whether a set of logic expressions 'A' > _entail_ a certain expression 'B'. Essentially, whether ALL models of A are > models of B. This is a nice tool to use for deductions. Currently, it calls > the dpll algo, but I guess wrongly. So that should be fixed. > > About satisfiable(), and especially for the assumptions system, may I > suggest looking at other, lighter SAT solvers like MiniSAT? We may have to > confirm the soundness and completeness, but thats still an avenue to > explore. > > @Soumya, I would suggest you send a PR with what modifications you propose, > and we take it from there. > > > On Friday, January 24, 2014 1:05:18 PM UTC+5:30, Soumya Biswas 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. >> >> 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.
