diff --git a/Data/Boolean.hs b/Data/Boolean.hs new file mode 100644 --- /dev/null +++ b/Data/Boolean.hs @@ -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 + diff --git a/Data/Boolean/SatSolver.hs b/Data/Boolean/SatSolver.hs new file mode 100644 --- /dev/null +++ b/Data/Boolean/SatSolver.hs @@ -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. ) 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 + + diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -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. + diff --git a/README b/README new file mode 100644 --- /dev/null +++ b/README @@ -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. ) 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. + diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,4 @@ +import Distribution.Simple + +main = defaultMain + diff --git a/incremental-sat-solver.cabal b/incremental-sat-solver.cabal new file mode 100644 --- /dev/null +++ b/incremental-sat-solver.cabal @@ -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. ) 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