El que esta ahí­ y dice cosas

Preparing a new release

Posted by fabian under sympy, Tecnologí­a, General

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 merge my query module and work on getting it right for 0.7.

Efficient DPLL algorithm

Posted by fabian under General

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 become 2x faster

Source code lives in my sympy repo, http:/fseoane.net/git/sympy.git, branch logic

References:
[1]: http://portal.acm.org/citation.cfm?coll=GUIDE&dl=GUIDE&id=321034
[2] http://people.sc.fsu.edu/~burkardt/data/cnf/dubois22.cnf

Queries and performance

Posted by fabian under sympy, Tecnologí­a, General

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, so inevitably queries are SLOW. But everything is not lost, since the algorithm is quite fast, and in fact other variants of the algorithm (MiniSAT) perform 6600x times faster than my implementation on medium-sized problems (60 variables, 170 clauses). So this looks like something smells bad on the programming side …

However, I spent the day profiling the function (link to source code used for profiling) without much success

Reading CNF files

Posted by fabian under sympy, Tecnologí­a, General

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 quinn.cnf be a file with the following content:

c  an example from Quinn's text, 16 variables and 18 clauses.
c Resolution: SATISFIABLE
c
p cnf 16 18
  1    2  0
 -2   -4  0
  3    4  0
 -4   -5  0
  5   -6  0
  6   -7  0
  6    7  0
  7  -16  0
  8   -9  0
 -8  -14  0
  9   10  0
  9  -10  0
-10  -11  0
 10   12  0
 11   12  0
 13   14  0
 14  -15  0
 15   16  0

Then we can load the file and test for satisfiability:

In [1]: from sympy.logic.utilities.dimacs import load_file

In [2]: expr = load_file("quinn.cnf")

In [3]: from sympy.logic.inference import satisfiable

In [4]: satisfiable(expr)
Out[4]:
{cnf_1: True, cnf_11: False, cnf_12: True, cnf_13: True, cnf_14: False, cnf_15: False, cnf_16: True,
 cnf_2: False, cnf_3: True, cnf_4: False, cnf_5: True, cnf_6: True, cnf_7: True, cnf_8: True, cnf_9:
 True}

References: more on the DIMACS CNF file format
BUGS: For large files like this one it exits prematurely with an error in the DPLL algorithm.

Logic module merged

Posted by fabian under sympy, Tecnologí­a, General

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

Posted by fabian under sympy, Tecnologí­a, General

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
   ^  ^
   |  |
   |   -------
   |         |
 Prime      Even
   ^
   |
   |
 MersennePrime

Then it will not know how to handle the query: Is x complex assuming it is a Mersenne prime ?. This is because the vertices MersennePrime and Complex are far away from each other and the query function does not load the complete graph of known facts, but rather a small subgraph centered on the assumed facts …

This was done so for efficiency reasons, because in the initial implementation I feared that the graph of known facts could become huge and thus making it unfeasible to search into.

But things have changed now. Known facts is not huge at all, roughly having over 20 vertices, so it is feasible to build the complete graph the first time query() is called and store it for future uses. And, most important, we have implemented fast algorithms for the problem of boolean satisfiability (DPLL under sympy.logic.algorithms.dpll), so all is ready to implement these ideas in the following days.

Interestingly, there seems to me many open source libraries for solving this problem. One that caught my attention early is MiniSAT, a nice little program written in C++ which is really fast

Initial implementation of the query system

Posted by fabian under sympy, Tecnologí­a, General

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), positive=True)
Out[2]: True


because abs() is always positive. Because exp() is always positive, the following should also be True:


In [3]: query(exp(x), positive=True)


but why then does it return None ?. Well, it simply is not True that exp() is always positive, it is always positive for real values, but SymPy does not assume that x is real, so you would have to specify that. This is now done with the keyword assumptions:


In [5]: query(exp(x), positive=True, assumptions=Assume(x, real=True))
Out[5]: True


As you can see, now assumptions are independent objects and are not tied to symbols any more. For more examples, see the file sympy/query/tests/test_query.py

still in the TODO list:
- support for global assumptions
- solve more complex implications, like query(x, positive=True, assumptions=Assume(x, even=True)) where it should build the chain of implications even => integer => rational => real. This chain of implications currently stops at rational for efficiency reasons, because the number of facts grows in each step which makes the number of possible paths grow exponentially.

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

Posted by fabian under sympy, Tecnologí­a, General

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. It could infer some basic rules, like Integer => Rational, but could not construct long paths like Prime => Integer => Rational => Real => Complex. You would have to specify by hand that prime numbers are also complex … and this just what makes the old assumption system unmanageable.

I know that state-of-the art CAS like Mathematica use advanced resolution techniques to get smart results. And in the open source world, well, the only CAS that I could find that has this sort of algorithms in Maxima, but in order to understand that I would have to learn LISP, and ironically enough I started to contribute to SymPy because I didn’t feel like learning LISP …

Homenaje a Antonio Vega en La Percha

Posted by fabian under Canciones, Grupo, General

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.

Fun with the new Logic module

Posted by fabian under sympy, Tecnologí­a

The logic module is slowly becoming useful. This week I managed to get some basic inference in propositional logic working. This should be enough for the assumption sysmtem (although having first-order inference would be cool).

You can pull from my branch:

git pull http://fseoane.net/git/sympy.git logic


Here are some examples of what it can do:

First, importing and defining our symbols

In [1]: A, B, C = symbols('ABC')
In [2]: from sympy.logic import *

It works with Symbols just as you would expect

In [3]: And(A, B)
Out[3]: And(A, B)

It applies De Morgan Rules automatically

In [4]: Not(Or(A, B))
Out[4]: And(Not(A), Not(B))

converts to conjuntive normal form (CNF)

In [5]: to_cnf(Implies(A, And(B, C)))
Out[5]: And(Or(B, Not(A)), Or(C, Not(A)))

Some basic inference:

In [6]: pl_true( Or(A, B), {A : True})  # what can we say about Or(A, B) if A is True ?
Out[6]: True

In [7]: pl_true ( And(A, B), {B: False}) # what is And(A, B) if B is False
Out[7]: False

To be discussed:
- I’m not sure if we should override &&, || on Symbol so that we can do A && B instead of And(A, B). If would make the code
cleaner, but also I don’t want to bloat Symbol any more. What do you think ?

I’m very proud of this in the sense that it is a nice clean module that will hopefully serve as the foundation of the new assumption
system.

Boolean algebra, first steps

Posted by fabian under sympy, Tecnologí­a

The first task for my Summer of Code project is to write a nice boolean algebra module. I wanted a clean module that follows SymPy’s object model and that plays well with other objects. In practice this means that it should inherit from Basic and that it should behave well with python’s boolean values (True, False) as well as with unknown values (SymPy’s Symbol).

To implement boolean expressions, my first thought was to implement And, Or, Not as subclass of AssocOp, just as Add and Mul. At the beginning I had some problems with commutativity, since my expressions are commutative but AssocOp does not have this feature. No problem, I thought, I’ll just override .flatten(). That seemed to work until I wanted to implement double-negation rule for Not (Not(Not(x)) –> x). Maybe I could have used .flatten() also for that, but that was ugly. Overriding __new__ was even uglier, so I began to think for an alternative approach.

Then I tried to think as a mathematician: And and Or are functions: B^2 –> B, and Not: B –> B, where B is the boolean space, so why don’t I implement them as subclasses of Function?. Turned out that Function is very inheritance-friendly and all you have to do is override the .eval() method. This is a minimalistic And function:

class And(Function):
    @classmethod
    def eval(cls, *args):
        if all(map(lambda x: isinstance(x, bool), args)):
            return all(args)
        sargs = sorted(flatten(args, cls=cls))
        return Basic.__new__(cls, *sargs)

You can see full source code here Lot’s of features are missing, of course, but it is capable of doing some simplifications and it plays nicely with Symbol and boolean types.

Logic modules in python

Posted by fabian under sympy, Tecnologí­a

As a prerequisite of my GSOC project I have to do some modifications on sympy’s current logic module (see previous post), so I decided to go out and take a look at what others are doing in this area.

aima-python is a project that tries to implement all algorithms found in the excellent book AI: A Modern Approach (AIMA for short). Code is concise and well written, but is has some (solvable) incompatibilities with SymPy’s design. In this module, all logic expressions (no matter if it’s and, or, xor etc) are implemented as an Expr class, but in SymPy we prefer to have a base class and implement logic expressions (And, Or, etc.) as subclasses, as this has proven to be a good modularization technique sympy’s core objects (Add, Mul, etc.). The book is also my primary source of information, as I only learned very rudimentary logic at college.

Pylog is a very interesting project implementing a logic module (although it’s primary goal is to write a Prolog interpreter in Python). It’s logic module seems to be written in a fashion very similar to SymPy’s standards, with a term class and variables predicates deriving from this. Makes extensive use of python generators, something that is lacking in my Python knowledge (and shouldn’t!)

Google Summer of Code

Posted by fabian under sympy, Tecnologí­a, General

First post on my GSOC adventure.

This year I got accepted in Google’s summer of code program as student, and my job will be to implement the assumptions framework in SymPy.

Although the project officially is only about implementing an assumptions framework, I have to prepare the ground before the official start of the program so that I can finish in time. Basically, this means refactoring the logic module, as this is the foundation of the assumption system. Current logic module was written with the old assumption system in mind, and has done a great job with that, but has some limitations:

- Non-standard API. From what I’ve read, everybody is calling the knowledge base KB, whereas we call it FactRules. Ask method is normally called Ask(), but we call it deduce_all_facts(), etc.

- Does not implement backward chaining, and I really need backward-chaining to make the assumption system a bit smart.

- No support for first-order logic, only propositional logic This is a must for anyone doing serious work in logic.

- Seems over complex. This is only an impression, but I’ve read other logic modules (aima-python), and they are much easier to understand.

Books I am reading on the topic:
- AI: A modern approach, Rusell & norvig
- Combinatorial Theory, Martin Aigner (has some useful info about graphs)

Django and request.POST

Posted by fabian under Tecnologí­a, General

I spent a lot of time trying to figure out why django removed the ‘+’ character from the POST data retrieved via request.POST.

Still don’t know the reason of this behaviour, but using request.raw_post_data saved my day …

Con la pasta por delante - día 2: Martos

Posted by fabian under Grupo, General

Después de Mengíbar vino Martos. En este caso se trataba del “Blooms Day”, un sitio para el que “un pub irlandés” es una descripción aceptable. Llegamos primero Oscar y yo, en una de esas raras ocasiones en que llegamos antes de tiempo (no hay explicación, simplemente sucedió), así que tuvimos tiempo para montar, probar, sonorizar … tranquilamente. Incluso tuve tiempo de comprar pilas para mis pedales (ha habido algún concierto en el que no haya tenido este problema?).

Se acerca el momento de subir al escenario. Migue pide unas copas, volvemos a afinar los instrumentos, bebo un poco de mi copa, vuelvo a afinar mi guitarra y dejo la copa en el escenario. Luego Oscar se toca la barriga y dice “yo estoy malo!” , esa es la señal y subimos al escenario.

Finalmente el concierto estuvo bien, la acústica de la sala era buena y aunque las guitarras no habían sido microfoneadas yo me oía bastante bien y toqué a gusto. Por cierto, eso que tengo delante mío es un micrófono (siiiii, ya me dejan hacer coros!)

Además, se pasaron un buen número de amigos, incluído Gollo, que hizo el viaje (en bus!) desde Granada (gracias !!).

Luego nos acostamos en un pisito de por ahí y constaté lo que ya me temía: Oscar ronca como un rinoceronte con paperas …

Mi ordenador

Posted by fabian under General

Realmente mi ordenador no hace nada … sólo le echo la culpa de todo

sympy 0.6.3

Posted by fabian under Tecnologí­a

I don’t know how it happened exactly, but when i realized, I had already submitted more than 10 patches for sympy, a program in which I was deeply involved one year ago but in which I was not active anymore.

Some interesting things happened in this release, like ports for jython and python2.6, buildbots, benchmarks, etc. , but the future is far more interesting, for example the newsolve branch, that will solve far more types of equations that the rather few supported now, or the new assumptions system, scheduled for the next release …

Con la pasta por delante - Día cero

Posted by fabian under Grupo, General

En la ciudad fabrican a las personas en serie. En el campo, los siguen haciendo a mano: los moldean, los secan al sol y luego los pintan, por eso son tan especiales.

Primer concierto de la nueva gira en Mengíbar, y uno de los fines de semana más intensos que recuerdo … todo salió tan bien que aún no me lo creo.

Nos vemos el próximo finde en Martos, vale?

Un premio para Goyo

Posted by fabian under General

Mi “sosio” de trabajo, el gran Goyal, acaba de ganar el primer premio del concurso yodona.

Si al final voy a tener que tratarte con respeto y todo …

cuándo era que lo íbamos a celebrar?

Los viejos amigos …

Posted by fabian under General

Nuevo repertorio, nuevos arreglos.

Nueva gira, nuevos lugares.

Sin olvidarse de los viejos amigos.

Empezamos la gira esta vez en Mengíbar, y mañana jueves (30 de Octubre) estaremos por la pecha, celebrando la publicación del EP y el cumpleaños de Hugo!

Felicidades!