I worked on improving the way the formulas are converted to CNF. Using Tseitin-Transformation <http://en.wikipedia.org/wiki/Tseitin-Transformation>the conversion to CNF can be optimized (a lot). The summary for the test is as follows:
Atoms: 20, Clauses: 100 (Using a propositional statement generator), a = average number of arguments to And/Or for a=2: Both algorithms producing almost similar results. Normal producing better results with DPLL2 while Tseitin producing better results with DPLL for a=3: Tseitin producing much better result than normal (Both algorithms) for a=4 and above: Tseitin showing remarkable improvement over normal A sample test: No. of formulas = 10, a=3 Tseitin: 1,982,682 uS Normal: 6,989,382 uS Will post the detailed test results once I finish testing more formally SD Soumya Dipta Biswas BITS, Pilani - K. K. Birla Goa Campus Contact: +918087953906 E-Mail: [email protected] On Sat, Jan 25, 2014 at 10:08 AM, Aaron Meurer <[email protected]> wrote: > 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 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 > [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.
