Instantly share code, notes, and snippets.

# gatlin/sat.hs Created Feb 6, 2012

 -- 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 []
 module Main where import AI.Surely main = putStrLn \$ show \$ solve [[1,2],[-1,3],[-3]]
Owner Author

### gatlin commented Feb 7, 2012

 Even better: ``````solve [[-1], [2, 3], [-3], [4, 5, 6], , [-7, 8, 9]] `````` I do think that's a bit more manageable.
Owner Author

### gatlin commented Feb 11, 2012

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

### Peaker commented Feb 11, 2012

 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
Owner Author

### gatlin commented Feb 11, 2012

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

### Confusion commented Feb 12, 2012

 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?
Owner Author

### gatlin commented Feb 12, 2012

 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!