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.