Brute force SAT solver in Haskell

Sometimes people get wrong impressions after a Theory of Computation course. A "hard" problem there is not necessarily hard to solve with a program, just hard to solve well in realistic circumstances. Take SAT, for example, the boolean satisfiability problem for propositional logic. It's a classic example of a NP-complete problem, whose naive solution -- generate all possible combinations of truth-values for each atomic proposition and then calculate the value for the whole formula -- is clearly exponential. But this naive solution is very easy to write. For example, in Haskell we get something like the following:

import Data.List  ( nub )
import Data.Maybe ( fromJust )

data Formula = Var String | And Formula Formula |
              Or Formula Formula | Not Formula

getVarsDup (Var v)     = [v]
getVarsDup (And f1 f2) = (getVarsDup f1) ++ (getVarsDup f2)
getVarsDup (Or f1 f2)  = (getVarsDup f1) ++ (getVarsDup f2)
getVarsDup (Not f)     = getVarsDup f

genValues n = genAux $ [replicate n True]
   where genAux (v:vs)     = if not $ or $ v then v:vs
                             else genAux ((next v) : v : vs)
         next (True : ts)  = (False : ts)
         next (False : ts) = (True : (next ts))

solveFormula (Var v) env     = fromJust $ lookup v env
solveFormula (And f1 f2) env = (solveFormula f1 env) &&
                              (solveFormula f2 env)
solveFormula (Or f1 f2) env  = (solveFormula f1 env) ||
                              (solveFormula f2 env)
solveFormula (Not f) env     = not $ solveFormula f env

allSolutions f = map (solveFormula f) (map (zip vars) vals)
   where vars = nub $ getVarsDup f
         vals = genValues (length vars)

-- solve the SAT problem
sat f = or $ allSolutions f

-- pointfree!
sat2 = or . allSolutions

The idea is the same as creating a truth-table for the formula and then looking for a T in the possible values for it. Function genValues generates all possible values for the atomic propositions, and this is fed into solveFormula. It would be very easy to alter the code to output the complete truth-table; I leave it as an exercise to the reader. Another standard exercise in logic textbooks is to prove that if a formula contains n atomic propositions, the truth-table will have 2^n lines. Thus, generating all combinations is easily seen to be exponential in time.

But the fact that it is hard for the computer to solve doesn't mean that it's hard for someone to write a (naive) program to solve it. In practical applications, like circuit design, we may need to solve SAT for thousands of variables, and the naive algorithm would not work. For this we must use a more clever technique, like Binary Decision Diagrams. They're not that hard to code either; the book Expert F# includes an example of BDDs in F#.

Tumbalalaika

It's probably too late to be hip because of this now, but I have created a tumblelog. It's easier to post there, so it should be updated more often than this blog. I'll probably post a good number of links in common with anarchaia.

Functional programming in the mainstream

Here is a bit from Ted Neward, commenting on the outcome of his predictions for 2007:

THEN: Languages: Interest in functional-object hybrid languages will grow. Scala, Jaskell, F#, and others not-yet-invented will start to capture developers' attention, particularly when they hear the part about functional languages being easier to use in multi-core systems because it encourages immutable objects and discourages side effects (meaning we don't have to worry nearly so much about writing thread-safe code). NOW: It grew, and it continues to grow. New languages in general are being released (see Clojure, Jaskell, dynalang, and others), and lots of them are incorporating functional language concepts. If you've never programmed in Haskell, now's a good time to learn, because those concepts and syntax are fast making their way towards you...

Book review: Expert F#

Expert F#, by Don Syme, Adam Granicz and Antonio Cisternino, Apress

When a new programming language arrives and manages to make an impact, books about it will certainly appear. However, most often the books will be geared to beginners, to people that is either not very experienced in programming or in the programming paradigms embodied by the language. For a experienced programmer, these books stop right when the fun would begin: the advanced stuff, the corners, the details are left out.

Expert F#, as suggested by its title, is not like this: it is aimed at more experienced programmers. The book will not teach you, for instance, what is functional programming or hammer to your head the best ways to use lists, an ubiquitous data structure in functional languages. But it explains how the things work in F#, so that programmers already familiar with other functional languages will have no trouble picking it up. F# also has object-oriented capabilities, which are explained in a chapter, without however going much deep into OO concepts; the book is about the language, not the paradigms.

And it does this well. Roughly half of the book is about the language itself, the other half are examples of applications and how to use some important libraries. As I was already familiar with OCaml and Haskell, I mostly skimmed through chapters 1 to 4, reading more closely from chapters 5 (generic types) and 6 (how objects fit into F#). From chapter 7 (encapsulating and packaging your code) on, the book starts to get really interesting; the next one is about common techniques, and chapter 9 is the best in the first part, explaining language-oriented programming, an area where functional languages really shine.

There are mandatory chapters about Windows Forms (11), Web programming (14) using .NET and data access, including how to use LINQ in F#, but I really liked chapters 12 (working with symbolic representations), and 13 (concurrency and asynchronous workflows). The former includes two cool examples: a symbolic differentiator and a verifier for logic circuits based on BDDs (Binary Decision Diagrams). There are other important and advanced chapters treating topics like interoperation with C and COM, debugging and testing F# programs, and F# library design.

All in all a very good book about the best current functional language to use in the Windows platform. I have two minor quibbles about it, though: the first few chapters about the language really could be made more interesting (although it didn't affect me much, as I only skimmed them) and some of the more exciting new features of F# could be explained in more detail. Specifically, workflows and active patterns. They are quite recent additions to the language, however, and there is some additional material promised to feature in the book's site.

Anyway, I will keep this book nearby when programming in F#. It is this kind of book that you'd want to keep around, even after learning the language.

Do it yourself: Visual F# Express 2008

As noted in this post, if you want Visual Studio just to have an IDE to work with F#, you can get it for free. Now with Visual Studio 2008, Microsoft has released a bare-bones VS, without any language, that can be used with language extensions and plugins, as is the case of F#. This bare-bones VS is called Visual Studio 2008 Shell (integrated mode).

After downloading and installing VS 2008 Shell (it takes a lot of unpacking and installing), you can install F# 1.9.3.7 and voilà, you have a pretty good F# IDE in your box, without having to shell out any cash.

I tested it with F# version 1.9.3.7 in a machine running Windows XP SP2 and no previous version of Visual Studio installed, and it worked. I even compiled and ran some test projects. If it doesn't work at first, take a look at the original post.

Further news on World Domination

Don Syme blogs about taking F# forward, which means, it seems, that F# will leave the confines of MS Research and be fully integrated into Visual Studio, as a product. If this is right, it's a great step for F# as a language and for functional programming in general, as we'll have a first-class IDE, by a major vendor, shipping with a functional programming language.

F# is already a great language to use, so I look forward to it getting still greater. The next step for Microsoft is to embrace Visual Haskell and fully integrate Haskell in Visual Studio too :)

Review: OCaml for Scientists

When we think about what makes a programming book good, what separates a classic from a run-of-the-mill for-dummies-learn-in-X-days book, it's not hard to get to the conclusion that the examples are an important piece of what we perceive as quality. I would say that this is even more so for books on programming languages: K&R had great examples; Practical Common Lisp has great examples that are now being copied by many authors; the list could go on.

So it was not that surprising to discover that one of the reasons of all the praise received by Dr. Jon Harrop's book OCaml for Scientists is its set of examples. There are even two entire chapters devoted to examples, the first for simple and the second for more significative ones. They are really good: well-chosen, interesting and well-written. Most of them have a scientific flavor, in keeping with the book's title, but to me this is a plus. Also, I don't recall seeing wavelet transforms as examples in a programming language book before; originality also counts.

The book's title is accurate: it is a book about OCaml primarily targeted for scientific applications. But most of the topics covered are really useful to anyone wanting to learn the OCaml language. Of all the ten chapters, I would say only one -- Chapter 4, Numerical Analysis -- is mostly directed to scientists. Well, probably game programmers too. And programmers of computer graphics applications, and anyone using floating-point arithmetic. Anyway, the other chapters that have somewhat of a scientific bent are: Chapter 6, Visualization, which is really about how to use OpenGL and GLUT in OCaml, which is quite cool in itself; and Chapter 10, Complete Examples, but each example is well explained and can be (mostly) understood without previous knowledge.

To give some idea about the book's contents, here is a quick tour: Chapter 1 is a quick introduction, covering most important concepts of the core language. Chapter 2 is about how to structure bigger programs, including function nesting, modules, objects, and how to manage dependencies and compilation. Chapter 3 is a very interesting chapter on data structures in OCaml, beginning with a section on algorithmic complexity; it covers the more important containers provided in the library, and also how to implement and work with trees. Chapter 4 is the one about numerical analysis, covering the basics about doing calculations with limited-precision numbers, and how to use more precise forms of arithmetic. Chapter 5 tackles input and output in OCaml, going beyond the call of duty to present the lexer generator (ocamllex) and parser generator (ocamlyacc) in the OCaml toolset. Chapter 6 is about visualization with OpenGL and GLUT, Chapter 7 is a very good one about optimization, and Chapter 8 a very useful one about libraries. The final two chapters have examples, and don't be fooled by the title of Chapter 9, Simple Examples. There is good stuff there. There are also two appendices, about more advanced features and troubleshooting advice respectivelly.

To be fair, the book has some small weaknesses that, in the end, are not that important, if you consider its target audience and what's common OCaml style. One is the treatment of objects: it is very cursory, and one of the examples (about real and complex numbers) could easily be considered a bad case of OO design. Considering most OCaml programmers rarely use objects, this is not so troubling. The other weakness I'd like to cite is more of a wish from my part: I wish there were more about advanced topics, especially functors (only very lightly touched in Appendix A).

But it's really a very good book about OCaml, both for beginners and for people with some previous exposure to it. It has advice on good programming style throughout, great examples (shown in color, properly syntax-highlighted), and distilled practical experience on some important topics (optimization, using libraries) that is hard to get elsewhere. It is remarkable not only in the very restricted universe of OCaml books, but as a programming book, in general: it stands between the best I've seen.