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]> 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] > > > 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. -- 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.
