RPython: Compiling Python to C (for the speed)

SAT Solver

Last night decided that I am going to write a SAT solver. But I had some conflicting requirements:

• I want it to be fast (SAT solvers are very resource heavy)
• I want it to be modular (Easily replace parts for more efficiency)
• I want the code to be very understandable.

SAT4J is the SAT solver I am most familiar with. It is as efficient as Java lets it be, it is very modular, and it is reasonably understandable on the surface, but the lower you get the more it is obfuscated.

SAT4J is based on the solver MiniSAT, which is meant to “to help researchers and developers alike to get started on SAT”. MiniSAT is fast, implemented in C, modular, however I ended up using the published papers about MiniSAT to translate the code that I was seeing.

Both of these are excellent projects, but I want to make the code easier to understand without sacrificing, speed or modularity.

RPython

RPython is a subset of python (i.e. rpython code is python code but not vice versa), it is hopefully my solution. It is described in this paper

and in this talk.

I will quickly go over the setup on my OSX system, and then later hopefully post about how my SAT solver implementation is going.

Setup

First thing is to install pypy:

brew install pypy

This will install pypy, but we need the pypy source for the translator:

cd /usr/local/Cellar/pypy
curl -O https://bitbucket.org/pypy/pypy/get/release-1.9.zip
unzip release-1.9.zip

This will create a horrible directory name with a SHA so…

mv pypy-pypy-341e1e3821ff/ pypy-src

Now that we have an installation lets get an rpython example up and running.

Simple Fibonacci Example

Lets do the default thing and create a Fibonacci calculator.

cd ~
mkdir fib
cd fib
touch fib.py

The final thing to do is to link the translate.py script which will compile the rpython

ln -s /usr/local/Cellar/pypy/pypy-src/pypy/translator/goal/translate.py

This code was taken from the above talk.

#fib.py
def fib(n):
  if n < 2:
    return 1
  else:
    return fib(n-1) + fib(n-2)
def main(argv):
  print fib(int(argv[1]))
  return 0
def target(*args):
  return main, None
if __name__ == '__main__':
  import sys
  main(sys.argv)

To make rpython work it requires a method called target, which must return an integer and to make it work as a python script it requires the final if statement.

Python script

Lets run this as a python script using CPython:

time python fib.py 34
9227465
real    0m3.319s
user    0m3.285s
sys    0m0.015s
Now with pypy:
time pypy fib.py 34
9227465
real    0m1.017s
user    0m0.586s
sys    0m0.032s

RPython

To run with RPython, we first we need to compile the script

pypy translate.py fib.py

This will generate the executable fib-c:

time ./fib-c 34
9227465
real    0m0.081s
user    0m0.077s
sys    0m0.003s

Summary

So pypy is about 3 times faster than CPython, and the compiled RPython is about 12 times faster than pypy.

However a Fibonacci calculator is a significantly less complicated than a SAT solver, both in terms of computation and code complexity.

Given the understandability of python code, and effeiency gained when compiling it to C, I think two of my initial requirements are satisfied.

Some potential modularity may be sacrificed because of the lack of som dynamic aspects of python. Soon, I hope to have a simple SAT solver implementation in RPython. At which point which I will write about it...