Currently I have 4 outstanding pull requests which target 6 issues but are blocked due to many reasons.
#2869 <https://github.com/sympy/sympy/pull/2869>: 1. Support for Equivalent with multiple arguments (Ready to be merged) #2964 <https://github.com/sympy/sympy/pull/2964>: 1. Added Semantic Tableaux (Explanation below) 2. improved pl_true (Ready to be merged, but blocked because of 1) #2830 <https://github.com/sympy/sympy/pull/2830>: 1. Fixed PropKB (Ready to be merged but blocked because of 2) 2. Added Valid Function (complete but configuring it to use semantic tableaux will make it MUCH faster) #2852 <https://github.com/sympy/sympy/pull/2852> 1. Added Tseitin Transformation (Explanation below) Explaination Both Semantic Tableaux and Tseitin work towards a common goal i.e. faster SAT solving. A significant part of my GSoC proposal is to make the overall SAT solving faster and depending upon the result these functions could become obsolete in future. 1. I plan on implementing much faster to_cnf (to_dnf). This is based on rudimentary benchmarks rather than just a willingness. The Semantic Tableaux works by iteratively manipulating sets<http://en.wikipedia.org/wiki/Method_of_analytic_tableaux#Set-labeled_tableau>, and is quite fast. I came up with a modification of the same algorithm for conversion to cnf/dnf. The formula generated by Tseitin takes longer SAT solving time than the same formula converted to CNF using to_cnf. But the overall time taken, encoding + SAT is very much smaller. Now, with the new to_cnf and new SAT solver, will this overall time remain much smaller? Theoretically it still should, but I can't comment on the numbers. So it is probably better to benchmark this with the new system in place. 2. Semantic Tableaux is currently acting as a lightweight decision procedure. This might very well change once the new system is in place (same reasoning as above). It is critical to benchmark to_cnf+SAT, Tseitin+SAT and SemTab together 3. Currently both SemTab and Tseitin call eliminate_implications to remove (bi)implications, but this step can be prevented in exchange of efficiency gain (considerably so in some cases). The traditional algorithm requires this elimination, but using some hacks supported because of the sympy architecture (by the virtue of applying de morgan automatically), this step can be removed. 4. One of the points in the open issues is regarding stopping automatic evaluation of Xor, ITE, 'Not pushed to literals' etc. What is the current stance of the community on this? My evaluation of the situation is following: It is quite helpful to the developer and decreases code complexity as certain things become deterministic (for e.g. if a Not exists then the arg is either a literal or an (bi)implication) and can lead to some interesting hacks (see above). However automatic eval could turn out to be quite confusing to the user and introduce a certain lack of obviousness. The answer to whether automatic evaluation is to be followed or not determines the code for both SemTab and Tseitin to a certain extent, and also whether I would add it as a part of my proposal. The whole point of this quite long post was to tell that while I have spent some good time with the code already and most are either complete or almost so, I would prefer deferring the actual merging to a later date. However, I still need a customary patch to be merged into master before the deadline, and #2869 will do the job, as it is both small and independent. Please comment on whether I should consider getting the PRs merged in their current form (in the spirit of the Zen of SymPy) and improve later or otherwise. -- 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 sympy+unsubscr...@googlegroups.com. To post to this group, send email to sympy@googlegroups.com. Visit this group at http://groups.google.com/group/sympy. To view this discussion on the web visit https://groups.google.com/d/msgid/sympy/CAGypG-M%3DCigfu3MsqZGmSBz47bwjR50m2unR5K6OPpNOTkb8XA%40mail.gmail.com. For more options, visit https://groups.google.com/d/optout.
