SAT Solver in Haskell

sat.hs

-- This is going to be on Hackage soon! https://github.com/gatlin/surely

{-# LANGUAGE BangPatterns #-}

-- |
-- Module           : AI.Surely
-- Copyright        : 2012 Gatlin Johnson
-- License          : LGPL 3.0
-- Maintainer       : rokenrol@gmail.com
-- Stability        : experimental
-- Portability      : GHC
--
-- This module defines a simple SAT solving algorithm exploiting the properties
-- of Maybe. Algorithms are based on the paper available at
-- https://cs.uwaterloo.ca/~david/cl/dpll-abstract.pdf.

module AI.Surely (solve) where
import Data.Maybe
import Control.Monad

type Literal = Integer
type Clause  = [Literal]
type Formula = [Clause]
type Record  = [Literal]

-- | The state of a solver at any given time is a subset of the original
--   formula and a record of assignments; that is, a list of the literals
--   considered to be true.
data SolverState = SolverState { formula :: !Formula
                               , record  :: !Record
                               } deriving (Show)

-- | The core algorithm, a simple back-tracking search with unitpropagation.
dpll :: SolverState -> Maybe Record
dpll s
    | null f = return r
    | otherwise = do
        l  <- chooseLiteral f
        case dpll (SolverState (simplify f l) (l:r)) of
            Just record -> return record
            Nothing -> dpll $! SolverState (simplify f (-l)) ((-l):r)
    where
        s' = unitpropagate s
        {-# INLINE s' #-}
        f = formula s'
        {-# INLINE f  #-}
        r = record s'
        {-# INLINE r  #-}

-- | unitpropagate simplifies the formula for every variable in a unit clause
--   (that is, a clause with only one unit).
unitpropagate :: SolverState -> SolverState
unitpropagate (SolverState f r) =
    case getUnit f of
        Nothing -> SolverState f r
        Just u -> unitpropagate $ SolverState (simplify f u) (u:r)

-- | Returns a `Just Literal` or Nothing if the formula has no literals left.
--   Since the argument was checked to see if it was null in a previous step,
--   failure to find a literal means the formula only contains empty clauses,
--   implying the problem is unsatisfiable and `dpll` will backtrack.
chooseLiteral :: Formula -> Maybe Literal
chooseLiteral !f = listToMaybe . concat $! f

-- | If a unit clause (singleton list) exists in the formula, return the
--   literal inside it, or Nothing.
getUnit :: Formula -> Maybe Literal
getUnit !xs = listToMaybe [ x | [x] <- xs ]

-- | Simplifying a formula `f` wrt a literal `l` means, for every clause in
--   which `-l` is a member remove `-l`, and remove every clause from f which
--   contains `l`.
--
--   Reasoning: a disjunction with a false value does not need to
--   consider that value, and a disjunction with a true value is trivially
--   satisfied.
simplify :: Formula -> Literal -> Formula
simplify !f !l = [ simpClause x l | x <- f, not (elem l x) ]
    where
        simpClause c l = filter (/= -l) c
        {-# INLINE simpClause #-}

-- | The top-level function wrapping `dpll` and hiding the library internals.
--   Accepts a list of lists of Integers, treating the outer list as a
--   conjunction and the inner lists as disjunctions.
solve :: [[Integer]] -> Maybe [Integer]
solve = dpll . flip SolverState []

test.hs

module Main where
import AI.Surely

main = putStrLn $ show $ solve [[1,2],[-1,3],[-3]]

Even better:

solve [[-1], [2, 3], [-3], [4, 5, 6], [7], [-7, 8, 9]]

I do think that's a bit more manageable.

Anyway, many thanks to the helpful people in #haskell for helping me understand Haskell idioms much better.

Use hlint on Haskell code. Here, it would whine about "n <- return $ negate l" vs. "let n = negate l".

I would whine about negate l instead of (-l) :-)

Then, you no longer need a "do" block for the Nothing case.

Also, if null would be better served by a case statement.

chooseLiteral xs = listToMaybe [ x | x:_ <- xs ]

Would probably be more readable as: chooseLiteral = listToMaybe . concat

Thanks for the tips. I'm astounded I got as much positive feedback as I have.

Your code interested me into finally diving into SAT-solvers, but there is one thing I can't seem to find via Google: how does the input, a list of lists of integers, encode a propositional logic formula?

It seems to be: each integer indicates a different (independent) variable, the lists in the 'outer' list are ANDed and the variables within an 'inner' list are ORed, meaning the formula is CNF? This seems to be a pretty 'standard' way, but are there other options? I could puzzle this one together, but nobody seems to describe other encodings of formulas?

Your nailed it: think of "1" as "x1", "2" as "x2", etc. 0 is unused and the polarity of the integer determines if it's negated. A clause is assumed to be a disjunction of these literals and a formula is a conjunction of clauses.

I made this up independently of other implementations but it does seem quite popular. I figure it's because negation is simple and you can probably optimize the hell out of it.

There are SAT techniques that don't use CNF in which case I'm not sure how you'd represent formulae. I assume you'd still use integers but you'd have to have some representation of AND and OR. That's the other reason this is probably used: the logical operators are implicit.

Let me know if you think of a better way!