Archive for June, 2009

Preparing a new release

Tuesday, June 30th, 2009

Last days I’ve been busy preparing the first public beta of SymPy 0.6.5. Most of the time was spent solving a bug that made documentation tests fail under python2.4, but now that this is solved, I hope that by the end of the week we could have a final release.
When this release is published, we’ll […]

Efficient DPLL algorithm

Sunday, June 28th, 2009

Background: DPLL is the algorithm behind SymPy’s implementation of logic.inference.satisfiable
After reading the original papers by Davis & Putnam [1], I managed to implement a more efficient version of the DPLL algorithm. It is 10x times faster on medium-sized problems (40 variables), and solves some wrong result bugs [2].
As a side effect, the query module has […]

Queries and performance

Tuesday, June 23rd, 2009

After some hacking on the queries module, I finally got it right without the limitations of past versions. You can check it out from my repo http://fseoane.net/git/sympy.git, branch master.
It now relies even more on logic.inference.satisfiable(), which is just an implementation of the DPLL algorithm. Bad news is that (my implementation of ) dpll_satisfiable() is SLOW, […]

Reading CNF files

Saturday, June 20th, 2009

The DIMACS CNF file format is used to define a Boolean expression, written in conjunctive normal form, that may be used as an example of the satisfiability problem.
The new logic module (sympy.logic) can read the content of a cnf file and transform it into a boolean expression suitable for use in other methods.
For example, let […]

Logic module merged

Friday, June 19th, 2009

Yesterday I finally merged the logic module in sympy’s official master branch, and should be released together with SymPy 0.6.5.
Next thing to do: profile the code and write some docs before the release.

The boolean satisfiability problem

Monday, June 15th, 2009

Most annoying problem in my implementation of the query system is that it will not solve implications if the implicates are far away from each other. For instance, if the graph of known facts is something like this

Integer —-> Rational –> Real –> Complex
^ ^
| |
[…]

Initial implementation of the query system

Friday, June 12th, 2009

I sent some patches to sympy-patches with an initial implementation of the query system.
You can check it out by pulling from my branch:
git pull http://fseoane.net/git/sympy.git master
into your sympy repo.
Some examples of what you can do (sample isympy session):
In [1]: query(x, positive=True)
Returns None, as we do not know whether x is positive or not.
In [2]: query(abs(x), […]

Assumption system and automatic theorem proving. Should I be learning LISP ?

Wednesday, June 3rd, 2009

This is the third time I attempt to write the assumption system. Other attempts could be described as me following the rule:
“For any complex problem, there is always a solution that is simple, clear, and wrong.”
My first attempt (although better than the current assumption system) did use very rudimentary logic and was not very smart. […]

Homenaje a Antonio Vega en La Percha

Monday, June 1st, 2009

El pasado jueves estuvimos en La Percha tocando algunas canciones de Antonio Vega. El vídeo se lo ha currado mi padre mezclando el sonido del directo con una grabación que hicimos en casa de Migue

LOS ESCLAVOS: homenaje a Antonio Vega from Felipe Pedregosa on Vimeo.