Pietro Abate

minisat2 ocaml bindings

Release early, release often !

I’ve been working with Falvio Lerda to update the ocaml binding to minisat2.

The biggest change from Fabio’s original version is the object oriented interface (mimicking the library c++ interface) and the addition of a couple of bindings.

You can find the git repo here.

I’ve also been working on the debian package and I’ve committed a draft package on git.debian.org.

A simple example is includes in the source where this is the main function.

(* Reads a given file and solves the instance. *)
let solve file =
  let solver = new solver in
  let vars = process_file solver file in
  match solver#solve with
  | Minisat.UNSAT -> printf "unsat\n"
  | Minisat.SAT   ->
      printf "sat\n";
      Hashtbl.iter
        (fun name v ->
          printf "  %s=%s\n"
            name
            (Minisat.string_of_value (solver#value_of v))
        )
        vars

Now I plan to finish the binding to minisat2 and then to attach [http://minisat.se/MiniSat+.html minisat+]. It should not be too difficult, if anyone is interested to lend me a hand, drop me a line.

Open source android applications

I’ll try to keep an update list of FOSS android applications. If you search for “android applications” on your favorite engine, you will mainly find payware / ad-ware or freeware closed source applications. I really can’t stand the idea. This is a selections of links. I haven’t tried them all and I’ll write my impressions as I try them out. My experiences are on a freerunner running android cupcake.

Astrid, a Task/Todo Manager. It’s a simple task applications (with a lot of options if you look closely) that works as advertized.

I found the following applications using this simple search on code.google.com

Autosetting Allows to customize your settings in relation to the time of the day/week
WebSMS Allows you to send cheap/free sms using various sms privders.

*Five It’s a cool client/server application to organize your music on your PC , sync on you mobile and play it. It has a smart storage policy to avoid filing your sdcard and tries to minimize the use of the network.

Anstop it’s a simple watch/stop.
http://code.google.com/p/android-wifi-tether/ It’s a tether application.
smspopup It’s a widget that pop-ups an alert when you receive a new sms.
android-sky it’s a weather widget.
rsyndroid uses rsync to backup your android phone.
simsalabim manage contacts on the sim card
aegis-shield it’s a password manager.
openvpn-settings lets you manage your vpn connections
sibyl music player

[stop at http://code.google.com/hosting/search?q=label%3AAndroid&filter=0&start=230]

modify a django model without loosing your data

If you want to modify your model, the diango doc suggests change the model and then manually run ALTER TABLE statements in your db to propagate the changes. This is a bit annoying to do if you have more then X modifications to do. The good reason to avoid automation here, is that if something goes wrong, you loose your data (and backups ??), and nobody, not even a robot overlord, wants to assume this responsability. A different strategy, that still requires manual intervention was suggested to my on the django IRC channel.

Basically we save the data, remove everything, recreate the DB, reload the data. Let’s go thought the procedure:

First we save the data, storing everything in a fixture, that is a json marshaling of the DB using this command:./manage.py dumpdata udf > udf.json . Notice that my manage.py is often also referred as django-admin.py.
Now it’s time to clean up the DB. Since we are working on a module, we can generate automatically the DROP TABLE statements using the following command :

./manage.py sqlclear udf
BEGIN;
DROP TABLE "udf_solution";
DROP TABLE "udf_solver";
DROP TABLE "udf_conversion";
DROP TABLE "udf_cudf";
DROP TABLE "udf_dudf";
COMMIT;

Once we have the sql statements, we just need to open the db and cut and paste them on the command line.

OK ! it’s finally time to actually modify the model.py file, add attributes. Something to be careful about is to specify a default value for all the new attributes. This was the when loading the data, the django infrastructure will know who to fill these fields.
Once done, we can recreate the tables with the command : ./manage.py syncdb.
And Finally reload the data ./manage.py loaddata udf.json

I think this recipe only works if you are adding new fields. If you are removing a field, I’m not sure then loaddata routine is smart enough to ignore the field… to be tested. Feedback appreciated.

lazy me, BronKerbosh algorithm revisited.

A while ago I wrote about the Bron - kerbosch algorithm giving a brain dead implementation based on simple lists. Of course since the amount of maximal cliques can be exponential in the size of graph, my previous implementation is useless on big graphs (say more then 80 nodes and 150 edges). It just takes forever.

Now I give a more efficient version of the algorithm that uses a simple lazy data structure to hold solution. Each element of the data structure is a set of nodes. The first part is the definition of a lazy list and a couple of ocamlgraph data structures. Pretty standard :

module PkgV = struct
    type t = int
    let compare = Pervasives.compare
    let hash i = i
    let equal = (=)
end

module UG = Graph.Imperative.Graph.Concrete(PkgV)
module N = Graph.Oper.Neighbourhood(UG)
module O = Graph.Oper.Make(Graph.Builder.I(UG))
module S = N.Vertex_Set
module RG = Graph.Rand.I(UG)

type 'a llist = 'a cell Lazy.t
and 'a cell = LList of 'a * 'a llist | Empty

exception LListEmpty

let empty = lazy(Empty)
let push e l = lazy(LList(e,l))

let hd s =
    match Lazy.force s with
    | LList (hd, _) -> hd
    | Empty -> raise LListEmpty

let rec append s1 s2 =
    lazy begin
        match Lazy.force s1 with
        | LList (hd, tl) -> LList (hd, append tl s2)
        | Empty -> Lazy.force s2
    end

let rec iter f s =
    begin
        match Lazy.force s with
        | LList (hd, tl) -> f hd ; iter f tl
        | Empty -> ()
    end

let rec map f s =
    lazy begin
        match Lazy.force s with
        | LList (hd, tl) -> LList (f hd, map f tl)
        | Empty -> Empty
    end

let rec flatten ss =
    lazy begin
        match Lazy.force ss with
        | Empty -> Empty
        | LList (hd, tl) ->
            match Lazy.force hd with
            | LList (hd2, tl2) -> LList (hd2, flatten (lazy (LList (tl2, tl))))
            | Empty -> Lazy.force (flatten tl)
    end

This second part is the algorithm itself. The fold function creates a lazy list of sets of vertex to be check by the algorithm. The body of the function each time choose a new pivot and invoke the bronKerbosch2 function on each of them in turn. When we finally manage to build a clique we return it (push r empty) embedded in a list. The flatten (map f m) takes care of unwinding the results in a flat lazy list.

let rec bronKerbosch2 gr r p x =
  let n v = N.set_from_vertex gr v in
  let rec fold acc (p,x,s) =
    if S.is_empty s then acc
    else
      let v = S.choose s in
      let rest = S.remove v s in
      let r' = S.union r (S.singleton v) in
      let p' = S.inter p (n v) in
      let x' = S.inter x (n v) in
      let acc' = (push (r',p',x') acc) in
      fold acc' (S.remove v p, S.add v x, rest)
  in
  if (S.is_empty p) && (S.is_empty x) then (push r empty)
  else
    let s = S.union p x in
    let u = S.choose s in
    let l = fold empty (p,x,S.diff p (n u)) in
    flatten (map (fun (r',p',x') -> bronKerbosch2 gr r' p' x') l)
;;

let max_independent_sets gr =
  let cgr = O.complement gr in
  let r = S.empty in
  let p = UG.fold_vertex S.add cgr S.empty in
  let x = S.empty in
  bronKerbosch2 cgr r p x
;;

To test it we just create a random graph and we iterates thought the results. Noticed that if the algorithm was not lazy, for big graphs, the iteration will get stuck waiting for the computation to be over.

let main () =
  let v = int_of_string Sys.argv.(1) in
  let e = int_of_string Sys.argv.(2) in
  let gr = RG.graph ~loops:true ~v:v ~e:e () in
  let mis = max_independent_sets gr in
  let i = ref 0 in
  iter (fun s ->
    Printf.printf "%d -> %s\n" !i (String.concat " , " (List.map string_of_int (S.elements s)));
    incr i
  ) mis
;;
main ();;

UPDATE

Following the lead from the comment below, I modified my lazy algorithm to use a smarter pivot selection strategy. On a random graph of 50 vertex and 80 edges I get almost 50% speed up ! This is great !

$./mis.native 50 80
--------------------------
Timer Mis classic. Total time: 15.035211. 
Timer Mis pivot selection. Total time: 8.708919. 
--------------------------

This is the code :

let choose gr cands s =
  let n v = N.set_from_vertex gr v in
  fst (
    S.fold (fun u (pivot, pivot_score) ->
      let score = S.cardinal (S.inter (n u) cands) in
      if score > pivot_score then (u, score)
      else (pivot, pivot_score)
    ) s (-1, -1)
  )

let rec bronKerbosch_pivot gr clique cands nots =
  let n v = N.set_from_vertex gr v in
  let rec fold acc (cands,nots,s) =
    if S.is_empty s then acc
    else
      let pivot = choose gr cands s in
      let rest = S.remove pivot s in
      let clique' = S.add pivot clique in
      let cands' = S.inter cands (n pivot) in
      let nots' = S.inter nots (n pivot) in
      let acc' = (push (clique',cands',nots') acc) in
      fold acc' (S.remove pivot cands, S.add pivot nots, rest)
  in
  if (S.is_empty cands) && (S.is_empty nots) then (push clique empty)
  else
    let s = S.union cands nots in
    let pivot = choose gr cands s in
    let rest = S.diff cands (n pivot) in
    let l = fold empty (S.remove pivot cands,S.add pivot nots,rest) in
    flatten (map (fun (clique',cands',nots') -> bronKerbosch_pivot gr clique' cands' nots') l)

let max_independent_sets_pivot gr =
  let cgr = O.complement gr in
  let clique = S.empty in
  let cands = UG.fold_vertex S.add cgr S.empty in
  let nots = S.empty in
  bronKerbosch_pivot cgr clique cands nots

build android adb on debian sid amd64

I’ve installed android on my freerunner. I’ve to say that it works ! very nice and functional interface, finger friendly, voice, sms, wifi work out of the box. I’m very impressed.

Following the lead from http://lackingrhoticity.blogspot.com/2010/02/how-to-build-adb-android-debugger.html I’ve decided to build adb to connect to my phone without downloading the precompiled sdk and without checking-out the entire android git repository. It’s actually very easy, and I’m sure with a minimal effort, it should be possible to create a debian package. The android instructions give some hints regarding the cross-compilation of android on a x64 machine.

Cutting and pasting from Lacking Rhoticity blog you need to :

$ sudo apt-get install build-essential libncurses5-dev
$ git clone git://android.git.kernel.org/platform/system/core.git system/core
$ git clone git://android.git.kernel.org/platform/build.git build
$ git clone git://android.git.kernel.org/platform/external/zlib.git external/zlib
$ git clone git://android.git.kernel.org/platform/bionic.git bionic
$ echo "include build/core/main.mk" >Makefile

Now edit build/core/main.mk and comment out the parts labelled

# Check for the correct version of java

and

# Check for the correct version of javac

Since adb doesn’t need Java, these checks are unnecessary.

Also edit build/target/product/sdk.mk and comment out the “include” lines after

# include available languages for TTS in the system image

Now, since we are one a x64 machine we need to install the rest of the libraries to cross compile abd. I think this is the minimum you need to successfully build adb

sudo apt-get install libc6-dev-i386 lib32ncurses5-dev ia32-libs g++-multilib

The result should be something like this :

$make out/host/linux-x86/bin/adb
============================================
PLATFORM_VERSION_CODENAME=REL
PLATFORM_VERSION=2.1-update1
TARGET_PRODUCT=generic
TARGET_BUILD_VARIANT=eng
TARGET_SIMULATOR=
TARGET_BUILD_TYPE=release
TARGET_ARCH=arm
HOST_ARCH=x86
HOST_OS=linux
HOST_BUILD_TYPE=release
BUILD_ID=ECLAIR
============================================
find: `frameworks/base/api': No such file or directory
[ ... ]
host Executable: adb (out/host/linux-x86/obj/EXECUTABLES/adb_intermediates/adb)
true
host C: acp <= build/tools/acp/acp.c
host C++: libhost <= build/libs/host/pseudolocalize.cpp
host C: libhost <= build/libs/host/CopyFile.c
host StaticLib: libhost (out/host/linux-x86/obj/STATIC_LIBRARIES/libhost_intermediates/libhost.a)
ar crs  out/host/linux-x86/obj/STATIC_LIBRARIES/libhost_intermediates/libhost.a out/host/linux-x86/obj/STATIC_LIBRARIES/libhost_intermediates/pseudolocalize.o out/host/linux-x86/obj/STATIC_LIBRARIES/libhost_intermediates/CopyFile.o
host Executable: acp (out/host/linux-x86/obj/EXECUTABLES/acp_intermediates/acp)
true
Install: out/host/linux-x86/bin/acp
Notice file: system/core/adb/NOTICE -- out/host/linux-x86/obj/NOTICE_FILES/src//bin/adb.txt
Notice file: system/core/libzipfile/NOTICE -- out/host/linux-x86/obj/NOTICE_FILES/src//lib/libzipfile.a.txt
Notice file: external/zlib/NOTICE -- out/host/linux-x86/obj/NOTICE_FILES/src//lib/libunz.a.txt
Notice file: system/core/liblog/NOTICE -- out/host/linux-x86/obj/NOTICE_FILES/src//lib/liblog.a.txt
Notice file: system/core/libcutils/NOTICE -- out/host/linux-x86/obj/NOTICE_FILES/src//lib/libcutils.a.txt
Install: out/host/linux-x86/bin/adb

Running abd :

$out/host/linux-x86/bin/adb      
Android Debug Bridge version 1.0.25
[...]

Now something very important that made me wonder for a while. By default android does not allow any connection with adb. To use it you must enable it on the phone. Then go Applications then Development. Under here you want to switch on Stay awake so that your screen stays visible while connected to your main system.

Finally, you can talk to your phone. Success !

$ADBHOST=192.168.0.202 ./out/host/linux-x86/bin/adb devices
* daemon not running. starting it now *
* daemon started successfully *
List of devices attached 
emulator-5554   device