Pietro Abate homepage

Despite the fact I can't stop talking about xfce4, what I'm have been missing lately is the functionality of gnome-terminal... I know I could install gnome terminal and use it, but this will imply a lot of unwanted dependencies and I prefer not go that way. Chatting on #xfce in IRC it was suggested to give a try to terminator https://launchpad.net/terminator/. I've used it for a couple of days now and I feel very comfortable with it. It has a lot of configuration options, the possibility to have multiple profiles and to group windows together, it has tabs and all bells and whistles you can ask.

The only thing I didn't like from the default settings is the red title bar on top... to remove it you need to edit the config file in ~/.config/terminator/config and add show_titlebar = False . This is my conf file :

Something else I'd like to do is to reduce the size and font of the tab on top of the terminal. Since this is a gtk applications, I should hack my gtk theme in order to style the tab, but I don't know how to do it only for one application. If somebody has an answer I'm all ears.

just a quicky. If you use the xfce terminal and you like to have more then one tab-terminal open, you might have niticed the the middle button closes it, without confirmation... I just discovered that this annoying feature can be turned off.

Following the freedesktop spec, you can just edit the file .config/Terminal/terminalrc and set the option MiscTabCloseMiddleClick to False.

There are many other settings . The full list is here : http://docs.xfce.org/apps/terminal/advanced

Below you can find an implementation in ocaml of the algorithm described in this paper by D. B. Johnson

  Finding all the elementary circuits of a directed graph.
  D. B. Johnson, SIAM Journal on Computing 4, no. 1, 77-84, 1975.
  http://dx.doi.org/10.1137/0204007

This is only the main function, you can find everything else in the git repo given below. If I've time I'll also give a shot to implement tarjan algorithm and to compare the two... Johnson is supposed to be better complexity wise, but I'm curious to check the difference on my domain specific input.

You can get the code here : git clone http://mancoosi.org/~abate/repos/cycles.git . There are two versions of the algorithm. One is a translation in ocaml of the imperative algorithm, the other, presented above, adds a bit of functional flavor ...

Update 1

the code repository now contains also two implementations of approximate algorithms the feedback arc set problem

Update 2

Since the number of cycles in a graph can be very large, I've added a lazy version of the algorithm using ExtLib enums (but can be easily done without). It would be cool to avoid using a global data structure to keep track of which nodes I've already visited like the persistent array of filliatr ... the code could be further optimized of course as many operations on lists and set can be avoided with a smarter DS to build the connected component of the subgraph at each iteration ... Complete code in the git repo above.

Recently I've discovered a subtle consequence of how the order in which dependencies are specified in debian actually matters. While re-factoring the code of dose3, I changed the order in which dependencies are considered by our sat solver (of edos-fame) . I witnessed a twofold performance loss just by randomizing how variables were presented to our sat solver. This highlights, on one hand, how our solver is strongly dependent on the structure of the problem and, on the other hand the standard practice of debian maintainers to assign an implicit priority in the disjunctive dependencies where the first is the most preferred packages (and maybe the most tested, at least dependency-wise).

The basic idea of distcheck is to encode the dependencies information contained in a Packages file in CNF format and then to feed them to a sat solver to find out if a package has broken dependencies or if its dependencies are such that no matter what, it would be impossible to install this package on a user machine.

Conflicts are encoded as binary clauses. So if package A conflicts with package B, I add a constraint they says "not (A and B)" , that is A and B cannot be considered together. The dependencies encoding associates to each disjunction of the depends field a clause that says "A implies B". If a package foo depends on A,B | C,D , I'll add "foo implies A and B" & "foo implies C and D" . This encoding is pretty standard and it is easy to understand.

The problem is how the sat solver will search for a solution to the problem "Is is possible to install package foo in an empty repository". The solver we use is very efficient and can easily deal with 100K packages or more. But in general is not very good at dealing with random CNF instances. The reason because edos-debcheck is so efficient lies in the way it exploits the structure of the sat problems.

The goal of a sat solver is to find a model (that is a variable assignment list) that is compatible with the given set of constraints. So if my encoding of the debian repository is a set of constraints R, the installability problem boils down to add an additional constraint to R imposing that the variable associated to the package foo must be true, and then ask the solver to find a model to make this possible. This installation, in sat terms, would be just an array of variables that must be true in order to satisfy the given set of constraints.

If you look at the logic problem as a truth table, the idea is to find a row in this table. This is the solution of your problem. Brute force of course is not an option and modern sat solvers use a number of strategies and heuristic to guide the search in the most intelligent way possible. Some of them try to learn from previous attempts, some of them, when they are lost try to pick a random variable to proceed.

If we consider problems that have a lot of structure, award winning sat solver do not back track very much. By exploiting the structure of the problem, their algorithm allows them to considerably narrow down the search only to those variables that are really important to find a solution.

All this long introduction was to talk about the solver that is currently used in edos-debcheck and distcheck (that is a rewrite of the edos-debcheck).

So why dependency order matters ? If we consider any package, even if the policy does not specify any order in the dependencies, it's common practice to write disjunctive dependencies specifying the most probable and tested alternative first and all other, more esoteric choices later. Moreover real packages are considered *before* virtual packages. Since every developer seems be doing the same, some kind of structure might be hidden in the order in which dependencies are specified.

Part of the efficiency of the the solver used in our tools is actually due to the fact that its search strategy is strongly dependent on the order in which literal are specified in each clause. Saying the package foo depends on A and B is "different" then saying it depends on B and A, even if semantically equivalent.

In my tests, I found about a twofold performance loss if the order of literals is either randomized or inverted. This is clearly a specific problem related to our solvers, while other solvers might not be susceptible to such small structural changes. Sat competitions often employs some form of obfuscation strategies of well known problems with well known structures in order to make useless to encode a search strategy that exploits the specific structure of a problem.

Since here we're not trying to win a sat competition, but to provide tool to solve a specific problem, we are of course very happy to exploit this structure.