I guess Aaron is right. But looking at issue 4075, I think our first focus SHOULD be to improve the 'to_cnf' function in the logic module. @Soumya, could you send a WIP PR to let us see how you are going about it? As Aaron said, the auxiliary variables may create problems, so we need to be sure about whats happening both before and after the CNF conversion.
On Wednesday, January 29, 2014 7:02:33 AM UTC+5:30, Aaron Meurer wrote: > > You have to be careful, though. Apparently Tseitin formulas can slow > down the SAT solver, due to the auxiliary variables that are > introduced. See > https://code.google.com/p/sympy/issues/detail?id=4075#c2. > > Aaron Meurer > > On Tue, Jan 28, 2014 at 1:40 PM, Soumya Biswas > <[email protected]<javascript:>> > wrote: > > I worked on improving the way the formulas are converted to CNF. Using > > 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] <javascript:> > > > > > > On Sat, Jan 25, 2014 at 10:08 AM, Aaron Meurer > > <[email protected]<javascript:>> > 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] <javascript:>> 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] <javascript:>. > >> > To post to this group, send email to > >> > [email protected]<javascript:>. > > >> > 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] <javascript:>. > >> > >> To post to this group, send email to [email protected]<javascript:>. > > >> 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] <javascript:>. > > To post to this group, send email to [email protected]<javascript:>. > > > 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.
