incremental-sat-solver (empty) → 0.1

raw patch · 6 files changed

+355/−0 lines, 6 filesdep +basedep +containersdep +mtlsetup-changed

Dependencies added: base, containers, mtl

Files

Data/Boolean.hs +133/−0
Data/Boolean/SatSolver.hs +141/−0
LICENSE +32/−0
README +13/−0
Setup.hs +4/−0
incremental-sat-solver.cabal +32/−0

+ Data/Boolean.hs view

@@ -0,0 +1,133 @@+{-# OPTIONS -fno-warn-incomplete-patterns #-}+-- |+-- Module      : Data.Boolean+-- Copyright   : Sebastian Fischer+-- License     : BSD3+-- +-- Maintainer  : Sebastian Fischer (sebf@informatik.uni-kiel.de)+-- Stability   : experimental+-- Portability : portable+-- +-- This library provides a representation of boolean formulas that is+-- used by the solver in "Data.Boolean.SatSolver".+-- +-- We also define a function to simplify formulas, a type for+-- conjunctive normalforms, and a function that creates them from+-- boolean formulas.+-- +module Data.Boolean ( ++  Boolean(..), ++  Literal(..), literalVar, invLiteral, isPositiveLiteral, ++  CNF, booleanToCNF++  ) where++-- | Boolean formulas are represented as values of type @Boolean@.+-- +data Boolean+  -- | Variables are labeled with an @Int@,+  = Var Int+  -- | @Yes@ represents /true/,+  | Yes+  -- | @No@ represents /false/,+  | No+  -- | @Not@ constructs negated formulas,+  | Not Boolean+  -- | and finally we provide conjunction+  | Boolean :&&: Boolean+  -- | and disjunction of boolean formulas.+  | Boolean :||: Boolean++-- | Literals are variables that occur either positively or negatively.+-- +data Literal = Pos Int | Neg Int deriving (Eq, Show)++-- | This function returns the name of the variable in a literal.+-- +literalVar :: Literal -> Int+literalVar (Pos n) = n+literalVar (Neg n) = n++-- | This function negates a literal.+-- +invLiteral :: Literal -> Literal+invLiteral (Pos n) = Neg n+invLiteral (Neg n) = Pos n++-- | This predicate checks whether the given literal is positive.+-- +isPositiveLiteral :: Literal -> Bool+isPositiveLiteral (Pos _) = True+isPositiveLiteral _       = False++-- | Conjunctive normalforms are lists of lists of literals.+-- +type CNF     = [Clause]+type Clause  = [Literal]++-- | +-- We convert boolean formulas to conjunctive normal form by pushing+-- negations down to variables and repeatedly applying the+-- distributive laws.+-- +booleanToCNF :: Boolean -> CNF+booleanToCNF+  = map (map literal . flatDisjunction)+  . flatConjunction+  . asLongAsPossible distribute+  . asLongAsPossible pushNots+  . asLongAsPossible elim+ where+  elim (Not Yes)      = Just No+  elim (Not No)       = Just Yes+  elim (No  :&&: _)   = Just No+  elim (Yes :&&: x)   = Just x+  elim (_   :&&: No)  = Just No+  elim (x   :&&: Yes) = Just x +  elim (Yes :||: _)   = Just Yes+  elim (No  :||: x)   = Just x+  elim (_   :||: Yes) = Just Yes+  elim (x   :||: No)  = Just x+  elim _              = Nothing++  pushNots (Not (Not x))  = Just x+  pushNots (Not (x:&&:y)) = Just (Not x :||: Not y)+  pushNots (Not (x:||:y)) = Just (Not x :&&: Not y)+  pushNots _              = Nothing++  distribute (x:||:(y:&&:z)) = Just ((x:||:y):&&:(x:||:z))+  distribute ((x:&&:y):||:z) = Just ((x:||:z):&&:(y:||:z))+  distribute _               = Nothing++  literal (Var x)       = Pos x+  literal (Not (Var x)) = Neg x+++-- private helper functions++flatConjunction :: Boolean -> [Boolean]+flatConjunction b = flat b []+ where flat (x:&&:y) = flat x . flat y+       flat x        = (x:)++flatDisjunction :: Boolean -> [Boolean]+flatDisjunction b = flat b []+ where flat (x:||:y) = flat x . flat y+       flat x        = (x:)++asLongAsPossible :: (Boolean -> Maybe Boolean) -> Boolean -> Boolean+asLongAsPossible f = everywhere g+ where g x = maybe x (everywhere g) (f x)++everywhere :: (Boolean -> Boolean) -> Boolean -> Boolean+everywhere f = f . atChildren (everywhere f)++atChildren :: (Boolean -> Boolean) -> Boolean -> Boolean+atChildren f (Not x)  = Not (f x)+atChildren f (x:&&:y) = f x :&&: f y+atChildren f (x:||:y) = f x :||: f y+atChildren _ x        = x+

+ Data/Boolean/SatSolver.hs view

@@ -0,0 +1,141 @@+-- |+-- Module      : Data.Boolean.SatSolver+-- Copyright   : Sebastian Fischer+-- License     : BSD3+-- +-- Maintainer  : Sebastian Fischer (sebf@informatik.uni-kiel.de)+-- Stability   : experimental+-- Portability : portable+-- +-- This Haskell library provides an implementation of the+-- Davis-Putnam-Logemann-Loveland algorithm+-- (cf. <http://en.wikipedia.org/wiki/DPLL_algorithm>) for the boolean+-- satisfiability problem. It not only allows to solve boolean+-- formulas in one go but also to add constraints and query bindings+-- of variables incrementally.+-- +-- The implementation is not sophisticated at all but uses the basic+-- DPLL algorithm with unit propagation.+-- +module Data.Boolean.SatSolver (++  Boolean(..), SatSolver,++  newSatSolver, isSolved, ++  lookupVar, assertTrue, branchOnVar, satisfy, selectBranchVar++  ) where++import Data.List+import Data.Boolean++import Control.Monad.Writer++import qualified Data.IntMap as IM++-- | A @SatSolver@ can be used to solve boolean formulas.+-- +data SatSolver = SatSolver { clauses :: CNF, bindings :: IM.IntMap Bool }+ deriving Show++-- | A new SAT solver without stored constraints.+-- +newSatSolver :: SatSolver+newSatSolver = SatSolver [] IM.empty++-- | This predicate tells whether all constraints are solved.+-- +isSolved :: SatSolver -> Bool+isSolved = null . clauses++-- |+-- We can lookup the binding of a variable according to the currently+-- stored constraints. If the variable is unbound, the result is+-- @Nothing@.+-- +lookupVar :: Int -> SatSolver -> Maybe Bool+lookupVar name = IM.lookup name . bindings++-- | +-- We can assert boolean formulas to update a @SatSolver@. The+-- assertion may fail if the resulting constraints are unsatisfiable.+-- +assertTrue :: MonadPlus m => Boolean -> SatSolver -> m SatSolver+assertTrue formula solver =+  simplify (solver { clauses = booleanToCNF formula ++ clauses solver })++-- |+-- This function guesses a value for the given variable, if it is+-- currently unbound. As this is a non-deterministic operation, the+-- resulting solvers are returned in an instance of @MonadPlus@.+-- +branchOnVar :: MonadPlus m => Int -> SatSolver -> m SatSolver+branchOnVar name solver =+  maybe (branchOnUnbound name solver)+        (const (return solver))+        (lookupVar name solver)++-- | +-- This function guesses values for variables such that the stored+-- constraints are satisfied. The result may be non-deterministic and+-- is, hence, returned in an instance of @MonadPlus@.+-- +satisfy :: MonadPlus m => SatSolver -> m SatSolver+satisfy solver+  | isSolved solver = return solver+  | otherwise = branchOnUnbound (selectBranchVar solver) solver >>= satisfy++-- |+-- We select a variable from the shortest clause hoping to produce a+-- unit clause.+--+selectBranchVar :: SatSolver -> Int+selectBranchVar = literalVar . head . head . sortBy shorter . clauses+++-- private helper functions++updateSolver :: CNF -> [(Int,Bool)] -> SatSolver -> SatSolver+updateSolver cs bs solver =+  solver { clauses  = cs,+           bindings = foldr (uncurry IM.insert) (bindings solver) bs }++simplify :: MonadPlus m => SatSolver -> m SatSolver+simplify solver = do+  (cs,bs) <- runWriterT . simplifyClauses . clauses $ solver+  return $ updateSolver cs bs solver++simplifyClauses :: MonadPlus m => CNF -> WriterT [(Int,Bool)] m CNF+simplifyClauses [] = return []+simplifyClauses allClauses = do+  let shortestClause = head . sortBy shorter $ allClauses+  guard (not (null shortestClause))+  if null (tail shortestClause)+   then propagate (head shortestClause) allClauses >>= simplifyClauses+   else return allClauses++propagate :: MonadPlus m => Literal -> CNF -> WriterT [(Int,Bool)] m CNF+propagate literal allClauses = do+  tell [(literalVar literal, isPositiveLiteral literal)]+  return (foldr prop [] allClauses)+ where+  prop c cs | literal `elem` c = cs+            | otherwise        = filter (invLiteral literal/=) c : cs++branchOnUnbound :: MonadPlus m => Int -> SatSolver -> m SatSolver+branchOnUnbound name solver =+  guess (Pos name) solver `mplus` guess (Neg name) solver++guess :: MonadPlus m => Literal -> SatSolver -> m SatSolver+guess literal solver = do+  (cs,bs) <- runWriterT (propagate literal (clauses solver) >>= simplifyClauses)+  return $ updateSolver cs bs solver++shorter :: [a] -> [a] -> Ordering+shorter []     []     = EQ+shorter []     _      = LT+shorter _      []     = GT+shorter (_:xs) (_:ys) = shorter xs ys++

+ LICENSE view

@@ -0,0 +1,32 @@+Copyright (c) 2009, Sebastian Fischer++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are+met:++ 1. Redistributions of source code must retain the above copyright+    notice, this list of conditions and the following disclaimer.++ 2. Redistributions in binary form must reproduce the above copyright+    notice, this list of conditions and the following disclaimer in+    the documentation and/or other materials provided with the+    distribution.++ 3. Neither the name of the author nor the names of his contributors+    may be used to endorse or promote products derived from this+    software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+``AS IS'' AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED.  IN NO EVENT SHALL THE AUTHORS OR+CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,+EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,+PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR+PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF+LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING+NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS+SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.+

+ README view

@@ -0,0 +1,13 @@+Simple, Incremental SAT Solving as a Library+============================================++This Haskell library provides an implementation of the+Davis-Putnam-Logemann-Loveland algorithm+(cf. <http://en.wikipedia.org/wiki/DPLL_algorithm>) for the boolean+satisfiability problem. It not only allows to solve boolean formulas+in one go but also to add constraints and query bindings of variables+incrementally.++The implementation is not sophisticated at all but uses the basic DPLL+algorithm with unit propagation.+

+ Setup.hs view

@@ -0,0 +1,4 @@+import Distribution.Simple++main = defaultMain+

+ incremental-sat-solver.cabal view

@@ -0,0 +1,32 @@+Name:          incremental-sat-solver+Version:       0.1+Cabal-Version: >= 1.6+Synopsis:      Simple, Incremental SAT Solving as a Library+Description:   This Haskell library provides an implementation of the+               Davis-Putnam-Logemann-Loveland algorithm+               (cf. <http://en.wikipedia.org/wiki/DPLL_algorithm>) for+               the boolean satisfiability problem. It not only allows+               to solve boolean formulas in one go but also to add+               constraints and query bindings of variables+               incrementally.+Category:      Algorithms+License:       BSD3+License-File:  LICENSE+Author:        Sebastian Fischer+Maintainer:    sebf@informatik.uni-kiel.de+Bug-Reports:   mailto:sebf@informatik.uni-kiel.de+Homepage:      http://github.com/sebfisch/incremental-sat-solver+Build-Type:    Simple+Stability:     experimental++Extra-Source-Files: README++Library+  Build-Depends:    base, containers, mtl+  Exposed-Modules:  Data.Boolean.SatSolver+  Other-Modules:    Data.Boolean+  Ghc-Options:      -Wall++Source-Repository head+  type:     git+  location: git://github.com/sebfisch/incremental-sat-solver.git