In a previous post on my SAT solver I promised to post about a dead end using functional priority queues. I believe the most efficient data structure for the dynamic variable ordering should be a priority queue. In fact, it looks like a job for a Fibonacci heap (animation). According to CLRS, “Fibonacci heaps are especially desirable when the number of Extract-Min and Delete operations is small relative to the number of other operations performed.” At least if just a few decisions will lead to a conflict, then we might end up adjusting the priority of many variables (to handle the conflict) so that there’s more adjusting than making decisions.
The asymptotic complexity of the Fibonacci heap works out because of its mutable tree structure. Specifically, adjusting the key of a node in the heap requires the caller to provide a pointer to that node in the heap, and that node needs to be able to navigate anywhere else in the heap. This can be done in Haskell (either with the IO monad or the ST monad), but the result isn’t elegant by any means. It also feels wrong — I program in a functional language because it lets me do equational reasoning, and think about data dependencies rather than state machine models of computation.
Functional Fibonacci Heap?
I tried for a while to see if I could come up with a Zipper view of the heap instead of the traditional linked-lists-of-heap-ordered-trees approach. That is, maybe a zipper could approximate a pointer. What I’d really need is a zipper with arbitrarily-many points of access into the heap (instead of one), and I’ve no idea how to write that. But any update of the heap requires updating all these zippers, which seems to destroy the complexity of the Decrease-Key operation.
Another option is to implement Decrease-Key by searching for the node to update, instead of providing a pointer. But I couldn’t figure out a way to integrate searching within the structure of a Fibonacci heap.
Eventually I considered this a dead end and posted to comp.lang.functional, where Ben Franksen pointed me to finger trees.
Finger Trees
Finger trees are a functional data structure for persistent sequences. Ralf Hinze described a Haskell implementation of 2-3 finger trees which is available from Hackage, so I used this. In the paper Hinze even describes how to implement max-priority queues on top of finger trees, which seemed like a good idea at first. Unfortunately, I don’t think it admits an efficient Decrease-Key, so I used the paper’s description of ordered sequences instead. This seems like the right thing to do, given that the paper says:
Ordered sequences subsume priority queues, as we have immediate access to the smallest and the greatest element, and search trees, as we can partition ordered sequences in logarithmic time.
The ability to do search trees gives us an efficient (sub-linear) Decrease-Key. Finally, my priority queue operations are:
extractMax :: (Ord k) => Heap k a -> (Info k a, Heap k a)
extractMax (OrdSeq s) = (x, OrdSeq s')
where x :< s' = viewl s
increaseKey :: (Ord k, Eq a) => Info k a -> k -> Heap k a -> Heap k a
increaseKey oldInfo newKey (OrdSeq t) = OrdSeq (l' >< eqs' >< r')
where (l, r) = split (<= measure oldInfo) t
(eqs, r') = split (< measure oldInfo) r
eqs' = foldr (\i t' -> if i == oldInfo then t' else i <| t')
FT.empty eqs
-- newInfo is bigger, so must fit on bigger side of split
(OrdSeq l') = insert newInfo (OrdSeq l)
newInfo = oldInfo{ key = newKey }
These implementations essentially do what I described in the previous section: implement a pointer approximation and integrate efficient searching. (Read the paper for more details.)
So What?
Well, I used finger trees in funsat. They were faster than whatever I was doing before.
