funsat (empty) → 0.4
raw patch · 12 files changed
+2773/−0 lines, 12 filesdep +QuickCheckdep +arraydep +basesetup-changed
Dependencies added: QuickCheck, array, base, bitset, containers, fgl, mtl, parse-dimacs, parsec, pretty, random, time
Files
- Control/Monad/MonadST.hs +51/−0
- DPLL/Monad.hs +82/−0
- Funsat/FastDom.hs +122/−0
- Funsat/Solver.hs +1414/−0
- Funsat/Utils.hs +111/−0
- LICENSE +165/−0
- Main.hs +172/−0
- README +26/−0
- Setup.hs +2/−0
- Text/Tabular.hs +77/−0
- funsat.cabal +63/−0
- tests/Properties.hs +488/−0
+ Control/Monad/MonadST.hs view
@@ -0,0 +1,51 @@+{-# LANGUAGE MultiParamTypeClasses+ ,FunctionalDependencies+ ,FlexibleInstances+ #-}+++{-+ This file is part of funsat.++ funsat is free software: you can redistribute it and/or modify+ it under the terms of the GNU Lesser General Public License as published by+ the Free Software Foundation, either version 3 of the License, or+ (at your option) any later version.++ funsat is distributed in the hope that it will be useful,+ but WITHOUT ANY WARRANTY; without even the implied warranty of+ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the+ GNU Lesser General Public License for more details.++ You should have received a copy of the GNU Lesser General Public License+ along with funsat. If not, see <http://www.gnu.org/licenses/>.++ Copyright 2008 Denis Bueno+-}+++-- | Idea from <http://haskell.org/pipermail/libraries/2003-September/001411.html>+module Control.Monad.MonadST where++import Control.Monad.ST+import Data.STRef++-- | A type class for monads that are able to perform `ST' actions.+class (Monad m) => MonadST s m | m -> s where+ liftST :: ST s a -> m a++instance MonadST s (Control.Monad.ST.ST s) where+ liftST = id++readSTRef :: MonadST s m => STRef s a -> m a+readSTRef = liftST . Data.STRef.readSTRef++writeSTRef :: MonadST s m => STRef s a -> a -> m ()+writeSTRef r x = liftST (Data.STRef.writeSTRef r x)++newSTRef :: MonadST s m => a -> m (STRef s a)+newSTRef = liftST . Data.STRef.newSTRef++modifySTRef :: MonadST s m => STRef s a -> (a -> a) -> m ()+modifySTRef r f = liftST (Data.STRef.modifySTRef r f)+
+ DPLL/Monad.hs view
@@ -0,0 +1,82 @@+{-# LANGUAGE PolymorphicComponents+ ,MultiParamTypeClasses+ ,FunctionalDependencies+ ,FlexibleInstances+ #-}++{-|++The main SAT solver monad. Embeds `ST'. See type `SSTErrMonad', which stands+for ''State ST Error Monad''.++Most of the work done is in the form of `SSTErrMonad' actions. -}+module DPLL.Monad+ ( liftST+ , runSSTErrMonad+ , evalSSTErrMonad+ , SSTErrMonad )+ where+import Control.Monad.Error hiding ((>=>), forM_)+import Control.Monad.ST.Strict+import Control.Monad.State.Lazy hiding ((>=>), forM_)+import Control.Monad.MonadST+++instance MonadST s (SSTErrMonad e st s) where+ liftST = dpllST++-- | Perform an @ST@ action in the DPLL monad.+dpllST :: ST s a -> SSTErrMonad e st s a+{-# INLINE dpllST #-}+dpllST st = SSTErrMonad (\k s -> st >>= \x -> k x s)++-- | @runSSTErrMonad m s@ executes a `SSTErrMonad' action with initial state @s@+-- until an error occurs or a result is returned.+runSSTErrMonad :: (Error e) => SSTErrMonad e st s a -> (st -> ST s (Either e a, st))+runSSTErrMonad m = unSSTErrMonad m (\x s -> return (return x, s))++evalSSTErrMonad :: (Error e) => SSTErrMonad e st s a -> st -> ST s (Either e a)+evalSSTErrMonad m s = do (result, _) <- runSSTErrMonad m s+ return result++-- | @SSTErrMonad e st s a@: the error type @e@, state type @st@, @ST@ thread+-- @s@ and result type @a@.+--+-- This is a monad embedding @ST@ and supporting error handling and state+-- threading. It uses CPS to avoid checking `Left' and `Right' for every+-- `>>='; instead only checks on `catchError'. Idea adapted from+-- <http://haskell.org/haskellwiki/Performance/Monads>.+newtype SSTErrMonad e st s a =+ SSTErrMonad { unSSTErrMonad :: forall r. (a -> (st -> ST s (Either e r, st)))+ -> (st -> ST s (Either e r, st)) }++instance Monad (SSTErrMonad e st s) where+ return x = SSTErrMonad ($ x)+ (>>=) = bindSSTErrMonad++bindSSTErrMonad :: SSTErrMonad e st s a -> (a -> SSTErrMonad e st s b) -> SSTErrMonad e st s b+{-# INLINE bindSSTErrMonad #-}+bindSSTErrMonad m f =+ {-# SCC "bindSSTErrMonad" #-}+ SSTErrMonad (\k -> unSSTErrMonad m (\a -> unSSTErrMonad (f a) k))++instance MonadState st (SSTErrMonad e st s) where+ get = SSTErrMonad (\k s -> k s s)+ put s' = SSTErrMonad (\k _ -> k () s')++instance (Error e) => MonadError e (SSTErrMonad e st s) where+ throwError err = -- throw away continuation+ SSTErrMonad (\_ s -> return (Left err, s))+ catchError action handler = {-# SCC "catchErrorSSTErrMonad" #-} SSTErrMonad+ (\k s -> do (x, s') <- runSSTErrMonad action s+ case x of+ Left error -> unSSTErrMonad (handler error) k s'+ Right result -> k result s')++instance (Error e) => MonadPlus (SSTErrMonad e st s) where+ mzero = SSTErrMonad (\_ s -> return (Left noMsg, s))+ mplus m n = SSTErrMonad (\k s ->+ do (r, s') <- runSSTErrMonad m s+ case r of+ Left _ -> unSSTErrMonad n k s'+ Right x -> k x s')
+ Funsat/FastDom.hs view
@@ -0,0 +1,122 @@++-- From a patch to the dominators lib on ghc's trac; should be incorporated+-- into fgl in GHC sooner or later.++-- | Find Dominators of a graph.+--+-- Author: Bertram Felgenhauer <int-e@gmx.de>+--+-- Implementation based on+-- Keith D. Cooper, Timothy J. Harvey, Ken Kennedy,+-- ''A Simple, Fast Dominance Algorithm'',+-- (http://citeseer.ist.psu.edu/cooper01simple.html)+module Funsat.FastDom+ ( dom+ , iDom ) where++import Data.Graph.Inductive.Graph+import Data.Graph.Inductive.Query.DFS+import Data.Tree (Tree(..))+import qualified Data.Tree as T+import Data.Array+import Data.IntMap (IntMap)+import qualified Data.IntMap as I++-- | return immediate dominators for each node of a graph, given a root+iDom :: Graph gr => gr a b -> Node -> [(Node,Node)]+iDom g root = let (result, toNode, _) = idomWork g root+ in map (\(a, b) -> (toNode ! a, toNode ! b)) (assocs result)+++-- | return the set of dominators of the nodes of a graph, given a root+dom :: Graph gr => gr a b -> Node -> [(Node,[Node])]+dom g root = let+ (iDom, toNode, fromNode) = idomWork g root+ dom' = getDom toNode iDom+ nodes' = nodes g+ rest = I.keys (I.filter (-1 ==) fromNode)+ in+ [(toNode ! i, dom' ! i) | i <- range (bounds dom')] +++ [(n, nodes') | n <- rest]++-- internal node type+type Node' = Int+-- array containing the immediate dominator of each node, or an approximation+-- thereof. the dominance set of a node can be found by taking the union of+-- {node} and the dominance set of its immediate dominator.+type IDom = Array Node' Node'+-- array containing the list of predecessors of each node+type Preds = Array Node' [Node']+-- arrays for translating internal nodes back to graph nodes and back+type ToNode = Array Node' Node+type FromNode = IntMap Node'++idomWork :: Graph gr => gr a b -> Node -> (IDom, ToNode, FromNode)+idomWork g root = let+ -- use depth first tree from root do build the first approximation+ trees@(~[tree]) = dff [root] g+ -- relabel the tree so that paths from the root have increasing nodes+ (s, ntree) = numberTree 0 tree+ -- the approximation iDom0 just maps each node to its parent+ iDom0 = array (1, s-1) (tail $ treeEdges (-1) ntree)+ -- fromNode translates graph nodes to relabeled (internal) nodes+ fromNode = I.unionWith const (I.fromList (zip (T.flatten tree) (T.flatten ntree))) (I.fromList (zip (nodes g) (repeat (-1))))+ -- toNode translates internal nodes to graph nodes+ toNode = array (0, s-1) (zip (T.flatten ntree) (T.flatten tree))+ preds = array (1, s-1) [(i, filter (/= -1) (map (fromNode I.!)+ (pre g (toNode ! i)))) | i <- [1..s-1]]+ -- iteratively improve the approximation to find iDom.+ iDom = fixEq (refineIDom preds) iDom0+ in+ if null trees then error "Dominators.idomWork: root not in graph"+ else (iDom, toNode, fromNode)+-- for each node in iDom, find the intersection of all its predecessor's+-- dominating sets, and update iDom accordingly.+refineIDom :: Preds -> IDom -> IDom+refineIDom preds iDom = fmap (foldl1 (intersect iDom)) preds++-- find the intersection of the two given dominance sets.+intersect :: IDom -> Node' -> Node' -> Node'+intersect iDom a b = case a `compare` b of+ LT -> intersect iDom a (iDom ! b)+ EQ -> a+ GT -> intersect iDom (iDom ! a) b++-- convert an IDom to dominance sets. we translate to graph nodes here+-- because mapping later would be more expensive and lose sharing.+getDom :: ToNode -> IDom -> Array Node' [Node]+getDom toNode iDom = let+ res = array (0, snd (bounds iDom)) ((0, [toNode ! 0]) :+ [(i, toNode ! i : res ! (iDom ! i)) | i <- range (bounds iDom)])+ in+ res+-- relabel tree, labeling vertices with consecutive numbers in depth first order+numberTree :: Node' -> Tree a -> (Node', Tree Node')+numberTree n (Node _ ts) = let (n', ts') = numberForest (n+1) ts+ in (n', Node n ts')++-- same as numberTree, for forests.+numberForest :: Node' -> [Tree a] -> (Node', [Tree Node'])+numberForest n [] = (n, [])+numberForest n (t:ts) = let (n', t') = numberTree n t+ (n'', ts') = numberForest n' ts+ in (n'', t':ts')++-- return the edges of the tree, with an added dummy root node.+treeEdges :: a -> Tree a -> [(a,a)]+treeEdges a (Node b ts) = (b,a) : concatMap (treeEdges b) ts++-- find a fixed point of f, iteratively+fixEq :: Eq a => (a -> a) -> a -> a+fixEq f v | v' == v = v+ | otherwise = fixEq f v'+ where v' = f v++{-+:m +Data.Graph.Inductive+let g0 = mkGraph [(i,()) | i <- [0..4]] [(a,b,()) | (a,b) <- [(0,1),(1,2),(0,3),(3,2),(4,0)]] :: Gr () ()+let g1 = mkGraph [(i,()) | i <- [0..4]] [(a,b,()) | (a,b) <- [(0,1),(1,2),(2,3),(1,3),(3,4)]] :: Gr () ()+let g2,g3,g4 :: Int -> Gr () (); g2 n = mkGraph [(i,()) | i <- [0..n-1]] ([(a,a+1,()) | a <- [0..n-2]] ++ [(a,a+2,()) | a <- [0..n-3]]); g3 n =mkGraph [(i,()) | i <- [0..n-1]] ([(a,a+2,()) | a <- [0..n-3]] ++ [(a,a+1,()) | a <- [0..n-2]]); g4 n =mkGraph [(i,()) | i <- [0..n-1]] ([(a+2,a,()) | a <- [0..n-3]] ++ [(a+1,a,()) | a <- [0..n-2]])+:m -Data.Graph.Inductive+-}+
+ Funsat/Solver.hs view
@@ -0,0 +1,1414 @@+{-# LANGUAGE PatternSignatures+ ,MultiParamTypeClasses+ ,FunctionalDependencies+ ,FlexibleInstances+ ,FlexibleContexts+ ,GeneralizedNewtypeDeriving+ ,TypeSynonymInstances+ ,TypeOperators+ ,ParallelListComp+ ,BangPatterns+ #-}+{-# OPTIONS -cpp #-}+++++++{-|++Goal: A reasonably efficient, easy-to-understand modern sat solver. I want it+as architecturally simple as the description in /Abstract DPLL and Abstract+DPLL Modulo Theories/ is conceptually, while retaining some efficient+optimisations.++ Current state: decision heuristic\/code cleanup\/tests.++* 24 Apr 2008 16:47:56++After some investigating, mad coding, and cursing, First UIP clause learning+has been implemented. For conceptual clarity, though, it is implemented in+terms of an explicit conflict graph, explicit dominator calculation, and+explicit cuts. Profiling shows that for conflict-heavy problems,+conflict-clause generation is no more a bottleneck than boolean constraint+propagation.++This can and will be improved later.++* 15 Dec 2007 22:46:11++backJump appears to work now. I used to have both Just and Nothing cases+there, but there was no reason why, since either you always reverse some past+decision (maybe the most recent one). Well, the problem had to do with+DecisionMap. Basically instead of keeping around the implications of a+decision literal (those as a result of unit propagation *and* reversed+decisions of higher decision levels), I was throwing them away. This was bad+for backJump.++Anyway, now it appears to work properly.++* 08 Dec 2007 22:15:44++IT IS ALIVE++I do need the /bad/ variables to be kept around, but I should only update the+list after I'm forced to backtrack *all the way to decision level 0*. Only+then is a variable bad. The Chaff paper makes you think you mark it as /tried+both ways/ the *first* time you see that, no matter the decision level.++On the other hand, why do I need a bad variable list at all? The DPLL paper+doesn't imply that I should. Hmm.++* 08 Dec 2007 20:16:17++For some reason, the /unsat/ (or /fail/ condition, in the DPLL paper) was not+sufficient: I was trying out all possible assignments but in the end I didn't+get a conflict, just no more options. So I added an or to test for that case+in `unsat'. Still getting assignments under which some clauses are undefined;+though, it appears they can always be extended to proper, satisfying+assignments. But why does it stop before then?++* 20 Nov 2007 14:52:51++Any time I've spent coding on this I've spent trying to figure out why some+inputs cause divergence. I finally figured out how (easily) to print out the+assignment after each step, and indeed the same decisions were being made+over, and over, and over again. So I decided to keep a /bad/ list of literals+which have been tried both ways, without success, so that decLit never decides+based on one of those literals. Now it terminates, but the models are (at+least) non-total, and (possibly) simply incorrect. This leads me to believ+that either (1) the DPLL paper is wrong about not having to keep track of+whether you've tried a particular variable both ways, or (2) I misread the+paper or (3) I implemented incorrectly what is in the paper. Hopefully before+I die I will know which of the three is the case.++* 17 Nov 2007 11:58:59:++Profiling reveals instance Model Lit Assignment accounts for 74% of time, and+instance Model Lit Clause Assignment accounts for 12% of time. These occur in+the call graph under unitPropLit. So clearly I need a *better way of+searching for the next unit literal*.++* Bibliography++''Abstract DPLL and DPLL Modulo Theories''++''Chaff: Engineering an Efficient SAT solver''++''An Extensible SAT-solver'' by Niklas Een, Niklas Sorensson++''Efficient Conflict Driven Learning in a Boolean Satisfiability Solver'' by+Zhang, Madigan, Moskewicz, Malik++''SAT-MICRO: petit mais costaud!'' by Conchon, Kanig, and Lescuyer++-}+module Funsat.Solver+#ifndef TESTING+ ( solve+ , solve1+ , DPLLConfig(..)+ , Solution(..)+ , IAssignment+ , litAssignment+ , litSign+ , Stats(..)+ , CNF+ , GenCNF(..)+ , Clause+ , Lit(..)+ , Var(..)+ , var+ , NonStupidString(..)+ , statTable+ , verify+ )+#endif+ where++{-+ This file is part of funsat.++ funsat is free software: you can redistribute it and/or modify+ it under the terms of the GNU Lesser General Public License as published by+ the Free Software Foundation, either version 3 of the License, or+ (at your option) any later version.++ funsat is distributed in the hope that it will be useful,+ but WITHOUT ANY WARRANTY; without even the implied warranty of+ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the+ GNU Lesser General Public License for more details.++ You should have received a copy of the GNU Lesser General Public License+ along with funsat. If not, see <http://www.gnu.org/licenses/>.++ Copyright 2008 Denis Bueno+-}+++import Control.Arrow ((&&&))+import Control.Exception (assert)+import Control.Monad.Error hiding ((>=>), forM_, runErrorT)+import Control.Monad.MonadST( MonadST(..) )+import Control.Monad.ST.Strict+import Control.Monad.State.Lazy hiding ((>=>), forM_)+import Data.Array.ST+import Data.Array.Unboxed+import Data.BitSet (BitSet)+import Data.Foldable hiding (sequence_)+import Data.Graph.Inductive.Graph( DynGraph, Graph )+import Data.Graph.Inductive.Graphviz+import Data.Graph.Inductive.Tree( Gr )+import Data.Int (Int64)+import Data.List (intercalate, nub, tails, sortBy, intersect, sort)+import Data.Map (Map)+import Data.Maybe+import Data.Ord (comparing)+import Data.STRef+import Data.Sequence (Seq)+import Data.Set (Set)+import Debug.Trace (trace)+import Prelude hiding (sum, concatMap, elem, foldr, foldl, any, maximum)+import Text.Printf( printf )+import Funsat.Utils+import DPLL.Monad+import qualified Data.BitSet as BitSet+import qualified Data.Graph.Inductive.Graph as Graph+import qualified Data.Graph.Inductive.Query.BFS as BFS+import qualified Data.Graph.Inductive.Query.DFS as DFS+import qualified Data.Foldable as Fl+import qualified Data.List as List+import qualified Data.Map as Map+import qualified Data.Sequence as Seq+import qualified Data.Set as Set+import qualified Funsat.FastDom as Dom+import qualified Text.Tabular as Tabular++-- * Interface++-- | Run the DPLL-based SAT solver on the given CNF instance.+solve :: DPLLConfig -> CNF -> (Solution, Stats)+solve cfg fIn =+ -- To solve, we simply take baby steps toward the solution using solveStep,+ -- starting with an initial assignment.+-- trace ("input " ++ show f) $+ either (error "no solution") id $+ runST $+ evalSSTErrMonad+ (do sol <- stepToSolution $ do+ initialAssignment <- liftST $ newSTUArray (V 1, V (numVars f)) 0+ isUnsat <- initialState initialAssignment+ if isUnsat then return (Right Unsat)+ else solveStep initialAssignment+ stats <- extractStats+ return (sol, stats))+ SC{ cnf=f{clauses = Set.empty}, dl=[]+ , watches=undefined, learnt=undefined, propQ=Seq.empty+ , trail=[], numConfl=0, level=undefined, numConflTotal=0+ , numDecisions=0, numImpl=0+ , reason=Map.empty, varOrder=undefined+ , dpllConfig=cfg }+ where+ f = preprocessCNF fIn+ -- If returns True, then problem is unsat.+ initialState :: MAssignment s -> DPLLMonad s Bool+ initialState m = do+ initialLevel <- liftST $ newSTUArray (V 1, V (numVars f)) noLevel+ modify $ \s -> s{level = initialLevel}+ initialWatches <- liftST $ newSTArray (L (- (numVars f)), L (numVars f)) []+ modify $ \s -> s{ watches = initialWatches }+ initialLearnts <- liftST $ newSTArray (L (- (numVars f)), L (numVars f)) []+ modify $ \s -> s{ learnt = initialLearnts }+ initialVarOrder <- liftST $ newSTUArray (V 1, V (numVars f)) initialActivity+ modify $ \s -> s{ varOrder = VarOrder initialVarOrder }++ (`catchError` (const $ return True)) $ do+ forM_ (clauses f)+ (\c -> do isConsistent <- watchClause m c False+ when (not isConsistent)+ -- conflict data is ignored here, so safe to fake+ (throwError (L 0, [])))+ return False+++-- | Solve with a default configuration `defaultConfig' (for debugging).+solve1 :: CNF -> (Solution, Stats)+solve1 f = solve (defaultConfig f) f++-- | Configuration parameters for the solver.+data DPLLConfig = Cfg+ { configRestart :: !Int64 -- ^ Number of conflicts before a restart.+ , configRestartBump :: !Double -- ^ `configRestart' is altered after each+ -- restart by multiplying it by this value.+ , configUseVSIDS :: !Bool -- ^ If true, use dynamic variable ordering.+ , configUseWatchedLiterals :: !Bool -- ^ If true, use watched literals+ -- scheme.+ , configUseRestarts :: !Bool+ , configUseLearning :: !Bool }+ deriving Show++-- | A default configuration based on the formula to solve.+defaultConfig :: CNF -> DPLLConfig+defaultConfig f = Cfg { configRestart = 100 -- fromIntegral $ max (numVars f `div` 10) 100+ , configRestartBump = 1.5+ , configUseVSIDS = True+ , configUseWatchedLiterals = True+ , configUseRestarts = True+ , configUseLearning = True }++-- * Preprocessing++-- | Some kind of preprocessing.+--+-- * remove duplicates+preprocessCNF :: CNF -> CNF+preprocessCNF f = f{clauses = simpClauses (clauses f)}+ where simpClauses = Set.map nub -- rm dups++-- | Simplify the clause database. Eventually should supersede, probably,+-- `preprocessCNF'.+--+-- Precondition: no decisions.+simplifyDB :: IAssignment -> DPLLMonad s ()+simplifyDB mFr = do+ -- For each clause in the database, remove it if satisfied; if it contains a+ -- literal whose negation is assigned, delete that literal.+ n <- numVars `liftM` gets cnf+ s <- get+ liftST . forM_ [V 1 .. V n] $ \i -> when (mFr!i /= 0) $ do+ let l = L (mFr!i)+ filterL _i = map (\(p, c) -> (p, filter (/= negate l) c))+ -- Remove unsat literal `negate l' from clauses.+ modifyArray (watches s) l filterL+ modifyArray (learnt s) l filterL+ -- Clauses containing `l' are Sat.+ writeArray (watches s) (negate l) []+ writeArray (learnt s) (negate l) []++-- * Internals++-- | The DPLL procedure is modeled as a state transition system. This+-- function takes one step in that transition system. Given an unsatisfactory+-- assignment, perform one state transition, producing a new assignment and a+-- new state.+solveStep :: MAssignment s -> DPLLMonad s (Step s)+solveStep m = do+ unsafeFreezeAss m >>= solveStepInvariants+ conf <- gets dpllConfig+ let selector = if configUseVSIDS conf then select else selectStatic+ let bcper = if configUseWatchedLiterals conf then bcp else bcpDumb+ maybeConfl <- bcper m+ mFr <- unsafeFreezeAss m+ s <- get+ voFr <- FrozenVarOrder `liftM` liftST (unsafeFreeze . varOrderArr . varOrder $ s)+ newState $ + -- Check if unsat.+ unsat maybeConfl s ==> return Nothing+ -- Unit propagation may reveal conflicts; check.+ >< maybeConfl >=> backJump m+ -- No conflicts. Decide.+ >< selector mFr voFr >=> decide m+ where+ -- Take the step chosen by the transition guards above.+ newState stepMaybe =+ case stepMaybe of+ -- No step to do => satisfying assignment. (p. 6)+ Nothing -> unsafeFreezeAss m >>= return . Right . Sat+ -- A step to do => do it, then see what it says.+ Just step -> step >>= return . maybe (Right Unsat) Left++-- | Check data structure invariants. Unless @-fno-ignore-asserts@ is passed,+-- this should be optimised away to nothing.+solveStepInvariants :: IAssignment -> DPLLMonad s ()+{-# INLINE solveStepInvariants #-}+solveStepInvariants _m = assert True $ do+ s <- get+ -- no dups in decision list or trail+ assert ((length . dl) s == (length . nub . dl) s) $+ assert ((length . trail) s == (length . nub . trail) s) $+ return ()+++-- | A state transition, or /step/, produces either an intermediate assignment+-- (using `Left') or a solution to the instance.+type Step s = Either (MAssignment s) Solution+ +-- | The solution to a SAT problem is either an assignment or unsatisfiable.+data Solution = Sat IAssignment | Unsat deriving (Eq)++-- | This function applies `solveStep' recursively until SAT instance is+-- solved. It also implements the conflict-based restarting (see+-- `DPLLConfig').+stepToSolution :: DPLLMonad s (Step s) -> DPLLMonad s Solution+stepToSolution stepAction = do+ step <- stepAction+ useRestarts <- gets (configUseRestarts . dpllConfig)+ restart <- uncurry ((>=)) `liftM`+ gets (numConfl &&& (configRestart . dpllConfig))+ case step of+ Left m -> do when (useRestarts && restart)+ (do stats <- extractStats+-- trace ("Restarting...") $+-- trace (statSummary stats) $+ resetState m)+ stepToSolution (solveStep m)+ Right s -> return s+ where+ resetState m = do+ modify $ \s -> s{ numConfl = 0 }+ -- Require more conflicts before next restart.+ modifySlot dpllConfig $ \s c ->+ s{ dpllConfig = c{ configRestart = ceiling (configRestartBump c+ * fromIntegral (configRestart c))+ } }+ lvl :: FrozenLevelArray <- gets level >>= liftST . unsafeFreeze+ undoneLits <- takeWhile (\l -> lvl ! (var l) > 0) `liftM` gets trail+ forM_ undoneLits $ const (undoOne m)+ modify $ \s -> s{ dl = [], propQ = Seq.empty }+ compactDB+ unsafeFreezeAss m >>= simplifyDB++instance Show Solution where+ show (Sat a) = "satisfiable: " ++ showAssignment a+ show Unsat = "unsatisfiable"+++-- ** Star Data Types++newtype Var = V {unVar :: Int} deriving (Eq, Ord, Enum, Ix)++instance Show Var where+ show (V i) = show i ++ "v"++instance Num Var where+ _ + _ = error "+ doesn't make sense for variables"+ _ - _ = error "- doesn't make sense for variables"+ _ * _ = error "* doesn't make sense for variables"+ signum _ = error "signum doesn't make sense for variables"+ negate = error "negate doesn't make sense for variables"+ abs = id+ fromInteger l | l <= 0 = error $ show l ++ " is not a variable"+ | otherwise = V $ fromInteger l++newtype Lit = L {unLit :: Int} deriving (Eq, Ord, Enum, Ix)+inLit f = L . f . unLit++-- | The polarity of the literal. Negative literals are false; positive+-- literals are true.+litSign :: Lit -> Bool+litSign (L x) | x < 0 = False+ | x > 0 = True++instance Show Lit where+ show l = show ul+ where ul = unLit l+instance Read Lit where+ readsPrec i s = map (\(i,s) -> (L i, s)) (readsPrec i s :: [(Int, String)])++-- | The variable for the given literal.+var :: Lit -> Var+var = V . abs . unLit++instance Num Lit where+ _ + _ = error "+ doesn't make sense for literals"+ _ - _ = error "- doesn't make sense for literals"+ _ * _ = error "* doesn't make sense for literals"+ signum _ = error "signum doesn't make sense for literals"+ negate = inLit negate+ abs = inLit abs+ fromInteger l | l == 0 = error "0 is not a literal"+ | otherwise = L $ fromInteger l++type Clause = [Lit]++-- | ''Generic'' conjunctive normal form. It's ''generic'' because the+-- elements of the clause set are polymorphic. And they are polymorphic so+-- that I can get a `Foldable' instance.+data GenCNF a = CNF {+ numVars :: Int,+ numClauses :: Int,+ clauses :: Set a+ }+ deriving (Show, Read, Eq)++type CNF = GenCNF Clause++instance Foldable GenCNF where+ -- TODO it might be easy to make this instance more efficient.+ foldMap toM cnf = foldMap toM (clauses cnf)+++-- | There are a bunch of things in the state which are essentially used as+-- ''set-like'' objects. I've distilled their interface into three methods.+-- These methods are used extensively in the implementation of the solver.+class Ord a => Setlike t a where+ -- | The set-like object with an element removed.+ without :: t -> a -> t+ -- | The set-like object with an element included.+ with :: t -> a -> t+ -- | Whether the set-like object contains a certain element.+ contains :: t -> a -> Bool++instance Ord a => Setlike (Set a) a where+ without = flip Set.delete+ with = flip Set.insert+ contains = flip Set.member++instance Ord a => Setlike [a] a where+ without = flip List.delete+ with = flip (:)+ contains = flip List.elem++instance Setlike IAssignment Lit where+ without a l = a // [(var l, 0)]+ with a l = a // [(var l, unLit l)]+ contains a l = unLit l == a ! (var l)++instance (Ord k, Ord a) => Setlike (Map k a) (k, a) where+ with m (k,v) = Map.insert k v m+ without m (k,_) = Map.delete k m+ contains = error "no contains for Setlike (Map k a) (k, a)"++instance (Ord a, BitSet.Hash a) => Setlike (BitSet a) a where+ with = flip BitSet.insert+ without = flip BitSet.delete+ contains = flip BitSet.member+++instance (BitSet.Hash Lit) where+ hash l = if li > 0 then 2 * vi else (2 * vi) + 1+ where li = unLit l+ vi = abs li++instance (BitSet.Hash Var) where+ hash = unVar+++-- | An ''immutable assignment''. Stores the current assignment according to+-- the following convention. A literal @L i@ is in the assignment if in+-- location @(abs i)@ in the array, @i@ is present. Literal @L i@ is absent+-- if in location @(abs i)@ there is 0. It is an error if the location @(abs+-- i)@ is any value other than @0@ or @i@ or @negate i@.+--+-- Note that the `Model' instance for `Lit' and `IAssignment' takes constant+-- time to execute because of this representation for assignments. Also+-- updating an assignment with newly-assigned literals takes constant time,+-- and can be done destructively, but safely.+type IAssignment = UArray Var Int++-- | Mutable array corresponding to the `IAssignment' representation.+type MAssignment s = STUArray s Var Int++-- | Same as @freeze@, but at the right type so GHC doesn't yell at me.+freezeAss :: MAssignment s -> ST s IAssignment+freezeAss = freeze+-- | See `freezeAss'.+unsafeFreezeAss :: MAssignment s -> DPLLMonad s IAssignment+unsafeFreezeAss = liftST . unsafeFreeze++thawAss :: IAssignment -> ST s (MAssignment s)+thawAss = thaw+unsafeThawAss :: IAssignment -> ST s (MAssignment s)+unsafeThawAss = unsafeThaw++-- | Destructively update the assignment with the given literal.+assign :: MAssignment s -> Lit -> ST s (MAssignment s)+assign a l = writeArray a (var l) (unLit l) >> return a++-- | Destructively undo the assignment to the given literal.+unassign :: MAssignment s -> Lit -> ST s (MAssignment s)+unassign a l = writeArray a (var l) 0 >> return a+++-- | An instance of this class is able to answer the question, Is a+-- truth-functional object @x@ true under the model @m@? Or is @m@ a model+-- for @x@? There are three possible answers for this question: `True' (''the+-- object is true under @m@''), `False' (''the object is false under @m@''),+-- and undefined, meaning its status is uncertain or unknown (as is the case+-- with a partial assignment).+--+-- The only method in this class is so named so it reads well when used infix.+-- Also see: `isTrueUnder', `isFalseUnder', `isUndefUnder'.+class Model a m where+ -- | @x ``statusUnder`` m@ should use @Right@ if the status of @x@ is+ -- defined, and @Left@ otherwise.+ statusUnder :: a -> m -> Either () Bool++-- /O(1)/.+instance Model Lit IAssignment where+ statusUnder l a | a `contains` l = Right True+ | a `contains` negate l = Right False+ | otherwise = Left ()+instance Model Var IAssignment where+ statusUnder v a | a `contains` pos = Right True+ | a `contains` neg = Right False+ | otherwise = Left ()+ where pos = L (unVar v)+ neg = negate pos+instance Model Clause IAssignment where+ statusUnder c m+ -- true if c intersect m is not null == a member of c in m+ | Fl.any (\e -> m `contains` e) c = Right True+ -- false if all its literals are false under m.+ | Fl.all (`isFalseUnder` m) c = Right False+ | otherwise = Left ()++++-- | `True' if and only if the object is undefined in the model.+isUndefUnder :: Model a m => a -> m -> Bool+isUndefUnder x m = isUndef $ x `statusUnder` m+ where isUndef (Left ()) = True+ isUndef _ = False++-- | `True' if and only if the object is true in the model.+isTrueUnder :: Model a m => a -> m -> Bool+isTrueUnder x m = isTrue $ x `statusUnder` m+ where isTrue (Right True) = True+ isTrue _ = False++-- | `True' if and only if the object is false in the model.+isFalseUnder :: Model a m => a -> m -> Bool+isFalseUnder x m = isFalse $ x `statusUnder` m+ where isFalse (Right False) = True+ isFalse _ = False++-- isUnitUnder c m | trace ("isUnitUnder " ++ show c ++ " " ++ showAssignment m) $ False = undefined+isUnitUnder c m = isSingle (filter (not . (`isFalseUnder` m)) c)+ && not (Fl.any (`isTrueUnder` m) c)++-- Precondition: clause is unit.+-- getUnit :: (Model a m, Show a, Show m) => [a] -> m -> a+-- getUnit c m | trace ("getUnit " ++ show c ++ " " ++ showAssignment m) $ False = undefined+getUnit c m = case filter (not . (`isFalseUnder` m)) c of+ [u] -> u+ xs -> error $ "getUnit: not unit: " ++ show xs++type Level = Int++-- | A /level array/ maintains a record of the decision level of each variable+-- in the solver. If @level@ is such an array, then @level[i] == j@ means the+-- decision level for var number @i@ is @j@. @j@ must be non-negative when+-- the level is defined, and `noLevel' otherwise.+--+-- Whenever an assignment of variable @v@ is made at decision level @i@,+-- @level[unVar v]@ is set to @i@.+type LevelArray s = STUArray s Var Level+-- | Immutable version.+type FrozenLevelArray = UArray Var Level++-- | Value of the `level' array if corresponding variable unassigned. Had+-- better be less that 0.+noLevel :: Level+noLevel = -1++-- | The VSIDS-like dynamic variable ordering.+newtype VarOrder s = VarOrder { varOrderArr :: STUArray s Var Double }+ deriving Show+newtype FrozenVarOrder = FrozenVarOrder (UArray Var Double)+ deriving Show++-- | Each pair of watched literals is paired with its clause.+type WatchedPair s = (STRef s (Lit, Lit), Clause)+type WatchArray s = STArray s Lit [WatchedPair s]++-- ** DPLL State and Phases++data DPLLStateContents s = SC+ { cnf :: CNF -- ^ The problem.+ , dl :: [Lit]+ -- ^ The decision level (last decided literal on front).+ , watches :: WatchArray s+ -- ^ Invariant: if @l@ maps to @((x, y), c)@, then @x == l || y == l@.+ , learnt :: WatchArray s+ -- ^ Same invariant as `watches', but only contains learned conflict+ -- clauses.+ , propQ :: Seq Lit+ -- ^ A FIFO queue of literals to propagate. This should not be+ -- manipulated directly; see `enqueue' and `dequeue'.+ , level :: LevelArray s+ , trail :: [Lit]+ -- ^ Chronological trail of assignments, last-assignment-at-head.+ , reason :: Map Var Clause+ -- ^ For each variable, the clause that (was unit and) implied its value.+ , numConfl :: !Int64+ -- ^ The number of conflicts that have occurred since the last restart.+ , numConflTotal :: !Int64+ -- ^ The total number of conflicts.+ , numDecisions :: !Int64+ -- ^ The total number of decisions.+ , numImpl :: !Int64+ -- ^ The total number of implications (propagations).+ , varOrder :: VarOrder s+ , dpllConfig :: DPLLConfig+ }+ deriving Show++instance Show (STRef s a) where+ show = const "<STRef>"+instance Show (STUArray s Var Int) where+ show = const "<STUArray Var Int>"+instance Show (STUArray s Var Double) where+ show = const "<STUArray Var Double>"+instance Show (STArray s a b) where+ show = const "<STArray>"++-- | Our star monad, the DPLL State monad. We use @ST@ for mutable arrays and+-- references, when necessary. Most of the state, however, is kept in+-- `DPLLStateContents' and is not mutable.+type DPLLMonad' s = StateT (DPLLStateContents s) (ST s)+instance Control.Monad.MonadST.MonadST s (DPLLMonad' s) where+ liftST = lift+++type DPLLMonad s = SSTErrMonad (Lit, Clause) (DPLLStateContents s) s+++-- *** Boolean constraint propagation++-- | Assign a new literal, and enqueue any implied assignments. If a conflict+-- is detected, return @Just (impliedLit, conflictingClause)@; otherwise+-- return @Nothing@. The @impliedLit@ is implied by the clause, but conflicts+-- with the assignment.+--+-- If no new clauses are unit (i.e. no implied assignments), simply update+-- watched literals.+bcpLit :: MAssignment s+ -> Lit -- ^ Assigned literal which might propagate.+ -> DPLLMonad s (Maybe (Lit, Clause))+bcpLit m l = do+ ws <- gets watches ; ls <- gets learnt+ clauses <- liftST $ readArray ws l+ learnts <- liftST $ readArray ls l+ liftST $ do writeArray ws l [] ; writeArray ls l []++ -- Update wather lists for normal & learnt clauses; if conflict is found,+ -- return that and don't update anything else.+ (`catchError` return . Just) $ do+ {-# SCC "bcpWatches" #-} forM_ (tails clauses) (updateWatches+ (\ f l -> liftST $ modifyArray ws l (const f)))+ {-# SCC "bcpLearnts" #-} forM_ (tails learnts) (updateWatches+ (\ f l -> liftST $ modifyArray ls l (const f)))+ return Nothing -- no conflict+ where+ -- updateWatches: `l' has been assigned, so we look at the clauses in+ -- which contain @negate l@, namely the watcher list for l. For each+ -- annotated clause, find the status of its watched literals. If a+ -- conflict is found, the at-fault clause is returned through Left, and+ -- the unprocessed clauses are placed back into the appropriate watcher+ -- list.+ {-# INLINE updateWatches #-}+ updateWatches _ [] = return ()+ updateWatches alter (annCl@(watchRef, c) : restClauses) = do+ mFr <- unsafeFreezeAss m+ q <- liftST $ do (x, y) <- readSTRef watchRef+ return $ if x == l then y else x+ -- l,q are the (negated) literals being watched for clause c.+ if negate q `isTrueUnder` mFr -- if other true, clause already sat+ then alter (annCl:) l+ else+ case find (\x -> x /= negate q && x /= negate l+ && not (x `isFalseUnder` mFr)) c of+ Just l' -> do -- found unassigned literal, negate l', to watch+ liftST $ writeSTRef watchRef (q, negate l')+ alter (annCl:) (negate l')++ Nothing -> do -- all other lits false, clause is unit+ modify $ \s -> s{ numImpl = numImpl s + 1 }+ alter (annCl:) l+ isConsistent <- enqueue m (negate q) (Just c)+ when (not isConsistent) $ do -- unit literal is conflicting+ alter (restClauses ++) l+ clearQueue+ throwError (negate q, c)++-- | Boolean constraint propagation of all literals in `propQ'. If a conflict+-- is found it is returned exactly as described for `bcpLit'.+bcp :: MAssignment s -> DPLLMonad s (Maybe (Lit, Clause))+bcp m = do+ q <- gets propQ+ if Seq.null q then return Nothing+ else do+ p <- dequeue+ bcpLit m p >>= maybe (bcp m) (return . Just)++bcpDumb :: MAssignment s -> DPLLMonad s (Maybe (Lit, Clause))+bcpDumb m = do+ mFr <- liftST $ freezeAss m+ s <- get+ let candidates = Set.filter (not . (`isTrueUnder` mFr)) (clauses . cnf $ s)+ case find (`isFalseUnder` mFr) candidates of+ Just fClause -> return $ Just (head fClause, fClause)+ Nothing ->+ case find (`isUnitUnder` mFr) candidates of+ Nothing -> return Nothing+ Just clause -> do+ let unitLit = getUnit clause mFr+ modify $ \s -> s{ numImpl = numImpl s + 1 }+ isConsistent <- assert (unitLit `isUndefUnder` mFr) $+ enqueue m unitLit (Just clause)+ clearQueue+ if not isConsistent+ then return $ Just (unitLit, clause)+ else bcpDumb m+++-- *** Decisions++-- | Find and return a decision variable. A /decision variable/ must be (1)+-- undefined under the assignment and (2) it or its negation occur in the+-- formula.+--+-- Select a decision variable, if possible, and return it and the adjusted+-- `VarOrder'.+select :: IAssignment -> FrozenVarOrder -> Maybe Var+{-# INLINE select #-}+select = varOrderGet++selectStatic :: IAssignment -> a -> Maybe Var+{-# INLINE selectStatic #-}+selectStatic m _ = find (`isUndefUnder` m) (range . bounds $ m)++-- | Assign given decision variable. Records the current assignment before+-- deciding on the decision variable indexing the assignment.+decide :: MAssignment s -> Var -> DPLLMonad s (Maybe (MAssignment s))+decide m v = do+ let ld = L (unVar v)+ (SC{dl=dl}) <- get+-- trace ("decide " ++ show ld) $ return ()+ modify $ \s -> s{ dl = ld:dl+ , numDecisions = numDecisions s + 1 }+ enqueue m ld Nothing+ return $ Just m++++-- *** Backtracking++-- | Non-chronological backtracking. The current returns the learned clause+-- implied by the first unique implication point cut of the conflict graph.+backJump :: MAssignment s+ -> (Lit, Clause)+ -- ^ @(l, c)@, where attempting to assign @l@ conflicted with+ -- clause @c@.+ -> DPLLMonad s (Maybe (MAssignment s))+backJump m c@(_, _conflict) = get >>= \(SC{dl=dl, reason=_reason}) -> do+ _theTrail <- gets trail+-- trace ("********** conflict = " ++ show c) $ return ()+-- trace ("trail = " ++ show _theTrail) $ return ()+-- trace ("dlits (" ++ show (length dl) ++ ") = " ++ show dl) $ return ()+-- ++ "reason: " ++ Map.showTree _reason+-- ) (+ modify $ \s -> s{ numConfl = numConfl s + 1+ , numConflTotal = numConflTotal s + 1 }+ levelArr :: FrozenLevelArray <- do s <- get+ liftST $ unsafeFreeze (level s)+ (learntCl, newLevel) <-+ do mFr <- unsafeFreezeAss m+ useLearning <- configUseLearning `liftM` gets dpllConfig+ if useLearning then analyse mFr levelArr dl c+ else analyseDecision mFr levelArr dl c+ s <- get+ let numDecisionsToUndo = length dl - newLevel+ dl' = drop numDecisionsToUndo dl+ undoneLits = takeWhile (\lit -> levelArr ! (var lit) > newLevel) (trail s) + forM_ undoneLits $ const (undoOne m) -- backtrack+ mFr <- unsafeFreezeAss m+ assert (numDecisionsToUndo > 0) $+ assert (not (null learntCl)) $+ assert (learntCl `isUnitUnder` mFr) $+ modify $ \s -> s{ dl = dl' } -- undo decisions+ mFr <- unsafeFreezeAss m+-- trace ("new mFr: " ++ showAssignment mFr) $ return ()+ -- TODO once I'm sure this works I don't need getUnit, I can just use the+ -- uip of the cut.+ enqueue m (getUnit learntCl mFr) (Just learntCl) -- learntCl is asserting+ watchClause m learntCl True+ return $ Just m++++-- Use the Decision first UIP clause, i.e, the crappiest one.+analyseDecision :: IAssignment -> FrozenLevelArray -> [Lit] -> (Lit, Clause)+ -> DPLLMonad s (Clause, Int)+analyseDecision mFr levelArr dlits c@(cLit, _cClause) = do+ st <- get+ let decisionCut = uipCut dlits levelArr conflGraph (unLit cLit)+ (decisionUIP conflGraph)+ conflGraph = mkConflGraph mFr levelArr (reason st) dlits c+ :: Gr CGNodeAnnot ()+ return $ cutLearn mFr levelArr decisionCut+ where+ decisionUIP :: (Graph gr) => gr CGNodeAnnot () -> Graph.Node+ decisionUIP _ = abs . unLit $ head dlits++-- | @doWhile cmd test@ first runs @cmd@, then loops testing @test@ and+-- executing @cmd@. The traditional @do-while@ semantics, in other words.+doWhile :: (Monad m) => m () -> m Bool -> m ()+doWhile body test = do+ body+ shouldContinue <- test+ when shouldContinue $ doWhile body test++-- | Analyse a the conflict graph and produce a learned clause. We use the+-- First UIP cut of the conflict graph.+--+-- May undo part of the trail, but not past the current decision level.+analyse :: IAssignment -> FrozenLevelArray -> [Lit] -> (Lit, Clause)+ -> DPLLMonad s (Clause, Int) -- ^ learned clause and new decision+ -- level+analyse mFr levelArr dlits (cLit, cClause) = do+ st <- get+-- trace ("mFr: " ++ showAssignment mFr) $ assert True (return ())+-- let (learntCl, newLevel) = cutLearn mFr levelArr firstUIPCut+-- firstUIPCut = uipCut dlits levelArr conflGraph (unLit cLit)+-- (firstUIP conflGraph)+-- conflGraph = mkConflGraph mFr levelArr (reason st) dlits c+-- :: Gr CGNodeAnnot ()+-- trace ("graphviz graph:\n" ++ graphviz' conflGraph) $ return ()+-- trace ("cut: " ++ show firstUIPCut) $ return ()+-- trace ("topSort: " ++ show topSortNodes) $ return ()+-- trace ("dlits (" ++ show (length dlits) ++ "): " ++ show dlits) $ return ()+-- trace ("learnt: " ++ show (map (\l -> (l, levelArr!(var l))) learntCl, newLevel)) $ return ()+-- outputConflict "conflict.dot" (graphviz' conflGraph) $ return ()+-- return $ (learntCl, newLevel)+ m <- liftST $ unsafeThawAss mFr+ a <- firstUIPBFS m (numVars . cnf $ st) (reason st)+-- trace ("firstUIPBFS learned: " ++ show a) $ return ()+ return a+ where+ -- BFS by undoing the trail backward. From Minisat paper.+ firstUIPBFS :: MAssignment s -> Int -> Map Var Clause -> DPLLMonad s (Clause, Int)+ firstUIPBFS m nVars reasonMap = do+ -- Literals we should process.+ seenArr <- liftST $ newSTUArray (V 1, V nVars) False+ counterR <- liftST $ newSTRef 0 -- Number of unprocessed current-level+ -- lits we know about.+ pR <- liftST $ newSTRef cLit -- Invariant: literal from current dec. lev.+ out_learnedR <- liftST $ newSTRef []+ out_btlevelR <- liftST $ newSTRef 0+ let reasonL l = (if l == cLit then cClause+ else Map.findWithDefault [] (var l) reasonMap+ `without` l)++ (`doWhile` (liftST (readSTRef counterR) >>= return . (> 0))) $+ do p <- liftST $ readSTRef pR+ forM_ (reasonL p) (bump . var)+ -- For each unseen reason,+ -- > from the current level, bump counter+ -- > from lower level, put in learned clause+ liftST . forM_ (reasonL p) $ \q -> do+ seenq <- readArray seenArr (var q)+ when (not seenq) $+ do writeArray seenArr (var q) True+ if levelL q == currentLevel+ then modifySTRef counterR (+ 1)+ else if levelL q > 0+ then do modifySTRef out_learnedR (q:)+ modifySTRef out_btlevelR $ max (levelL q)+ else return ()+ -- Select next literal to look at:+ (`doWhile` (liftST (readSTRef pR >>= readArray seenArr . var)+ >>= return . not)) $ do+ p <- head `liftM` gets trail -- a dec. var. only if the counter =+ -- 1, i.e., loop terminates now+ liftST $ writeSTRef pR p+ undoOne m+ -- Invariant states p is from current level, so when we're done+ -- with it, we've thrown away one lit. from counting toward+ -- counter.+ liftST $ modifySTRef counterR (\c -> c - 1)+ p <- liftST $ readSTRef pR+ liftST $ modifySTRef out_learnedR (negate p:)+ bump . var $ p+ out_learned <- liftST $ readSTRef out_learnedR+ out_btlevel <- liftST $ readSTRef out_btlevelR+ return (out_learned, out_btlevel)++ firstUIP conflGraph = -- trace ("--> uips = " ++ show uips) $+-- trace ("--> dom " ++ show conflNode+-- ++ " = " ++ show domConfl) $+-- trace ("--> dom " ++ show (negate conflNode)+-- ++ " = " ++ show domAssigned) $+ argminimum distanceFromConfl uips :: Graph.Node+ where+ uips = domConfl `intersect` domAssigned :: [Graph.Node]+ -- `domConfl' never gives us vacuous dominators since there is by+ -- construction a path on the current decision level to the implied,+ -- conflicting node. OTOH, there might be no path from dec. var. to+ -- the assigned literal which is conflicting (negate conflNode).+ domConfl = filter (\i -> levelN i == currentLevel && i /= conflNode) $+ fromJust $ lookup conflNode domFromLastd+ domAssigned =+ -- if assigned conflict node is not implied by the current-level+ -- dec var, then the only dominator we should list of it should+ -- be the dec var.+ if negate conflNode `elem` DFS.reachable (abs $ unLit lastd) conflGraph+ then + filter (\i -> levelN i == currentLevel && i /= conflNode) $+ fromJust $ lookup (negate conflNode) domFromLastd+ else [(abs $ unLit lastd)]+ domFromLastd = Dom.dom conflGraph (abs $ unLit lastd)+ distanceFromConfl x = length $ BFS.esp x conflNode conflGraph++ -- helpers+ lastd = head dlits+ conflNode = unLit cLit+ currentLevel = length dlits+ levelL l = levelArr!(var l)+ levelN i = if i == unLit cLit then currentLevel else ((levelArr!) . V . abs) i++-- | The union of the reason side and the conflict side are all the nodes in+-- the `cutGraph' (excepting, perhaps, the nodes on the reason side at+-- decision level 0, which should never be present in a learned clause).+data Cut f gr a b =+ Cut { reasonSide :: f Graph.Node+ -- ^ The reason side contains at least the decision variables.+ , conflictSide :: f Graph.Node+ -- ^ The conflict side contains the conflicting literal.+ , cutUIP :: Graph.Node+ , cutGraph :: gr a b }+instance (Show (f Graph.Node), Show (gr a b)) => Show (Cut f gr a b) where+ show (Cut { conflictSide = c, cutUIP = uip }) =+ "Cut (uip=" ++ show uip ++ ", cSide=" ++ show c ++ ")"++-- | Generate a cut using the given UIP node. The cut generated contains+-- exactly the (transitively) implied nodes starting with (but not including)+-- the UIP on the conflict side, with the rest of the nodes on the reason+-- side.+uipCut :: (Graph gr) =>+ [Lit] -- ^ decision literals+ -> FrozenLevelArray+ -> gr a b -- ^ conflict graph+ -> Graph.Node -- ^ unassigned, implied conflicting node+ -> Graph.Node -- ^ a UIP in the conflict graph+ -> Cut Set gr a b+uipCut dlits levelArr conflGraph conflNode uip =+ Cut { reasonSide = Set.filter (\i -> levelArr!(V $ abs i) > 0) $+ allNodes Set.\\ impliedByUIP+ , conflictSide = impliedByUIP+ , cutUIP = uip+ , cutGraph = conflGraph }+ where+ -- Transitively implied, and not including the UIP. + impliedByUIP = Set.insert extraNode $+ Set.fromList $ tail $ DFS.reachable uip conflGraph+ -- The UIP may not imply the assigned conflict variable which needs to+ -- be on the conflict side, unless it's a decision variable or the UIP+ -- itself.+ extraNode = if L (negate conflNode) `elem` dlits || negate conflNode == uip+ then conflNode -- idempotent addition+ else negate conflNode+ allNodes = Set.fromList $ Graph.nodes conflGraph+++-- | Generate a learned clause from a cut of the graph. Returns a pair of the+-- learned clause and the decision level to which to backtrack.+cutLearn :: (Graph gr, Foldable f) => IAssignment -> FrozenLevelArray+ -> Cut f gr a b -> (Clause, Int)+cutLearn a levelArr cut =+ ( clause+ -- The new decision level is the max level of all variables in the+ -- clause, excluding the uip (which is always at the current decision+ -- level).+ , maximum0 (map (levelArr!) . (`without` V (abs $ cutUIP cut)) . map var $ clause) )+ where+ -- The clause is composed of the variables on the reason side which have+ -- at least one successor on the conflict side. The value of the variable+ -- is the negation of its value under the current assignment.+ clause =+ foldl' (\ls i ->+ if any (`elem` conflictSide cut) (Graph.suc (cutGraph cut) i)+ then L (negate $ a!(V $ abs i)):ls+ else ls)+ [] (reasonSide cut)+ maximum0 [] = 0 -- maximum0 has 0 as its max for the empty list+ maximum0 xs = maximum xs+++-- | Annotate each variable in the conflict graph with literal (indicating its+-- assignment) and decision level. The only reason we make a new datatype for+-- this is for its `Show' instance.+data CGNodeAnnot = CGNA Lit Level+instance Show CGNodeAnnot where+ show (CGNA (L 0) _) = "lambda"+ show (CGNA l lev) = show l ++ " (" ++ show lev ++ ")"++-- | Creates the conflict graph, where each node is labeled by its literal and+-- level.+--+-- Useful for getting pretty graphviz output of a conflict.+mkConflGraph :: DynGraph gr =>+ IAssignment+ -> FrozenLevelArray+ -> Map Var Clause+ -> [Lit] -- ^ decision lits, in rev. chron. order+ -> (Lit, Clause) -- ^ conflict info+ -> gr CGNodeAnnot ()+mkConflGraph mFr lev reasonMap _dlits (cLit, confl) =+ Graph.mkGraph nodes' edges'+ where+ -- we pick out all the variables from the conflict graph, specially adding+ -- both literals of the conflict variable, so that that variable has two+ -- nodes in the graph.+ nodes' =+ ((0, CGNA (L 0) (-1)) :) $ -- lambda node+ ((unLit cLit, CGNA cLit (-1)) :) $+ ((negate (unLit cLit), CGNA (negate cLit) (lev!(var cLit))) :) $+ -- annotate each node with its literal and level+ map (\v -> (unVar v, CGNA (varToLit v) (lev!v))) $+ filter (\v -> v /= var cLit) $+ toList nodeSet'+ + -- node set includes all variables reachable from conflict. This node set+ -- construction needs a `seen' set because it might infinite loop+ -- otherwise.+ (nodeSet', edges') =+ mkGr Set.empty (Set.empty, [ (unLit cLit, 0, ())+ , ((negate . unLit) cLit, 0, ()) ])+ [negate cLit, cLit]+ varToLit v = (if v `isTrueUnder` mFr then id else negate) $ L (unVar v)++ -- seed with both conflicting literals+ mkGr _ ne [] = ne+ mkGr (seen :: Set Graph.Node) ne@(nodes, edges) (lit:lits) =+ if haveSeen+ then mkGr seen ne lits+ else newNodes `seq` newEdges `seq`+ mkGr seen' (newNodes, newEdges) (lits ++ pred)+ where+ haveSeen = seen `contains` litNode lit+ newNodes = var lit `Set.insert` nodes+ newEdges = [ ( litNode (negate x) -- unimplied lits from reasons are+ -- complemented+ , litNode lit, () )+ | x <- pred ] ++ edges+ pred = filterReason $+ if lit == cLit then confl else+ Map.findWithDefault [] (var lit) reasonMap `without` lit+ filterReason = filter ( ((var lit /=) . var) .&&.+ ((<= litLevel lit) . litLevel) )+ seen' = seen `with` litNode lit+ litLevel l = if l == cLit then length _dlits else lev!(var l)+ litNode l = -- lit to node+ if var l == var cLit -- preserve sign of conflicting lit+ then unLit l+ else (abs . unLit) l+++-- | Delete the assignment to last-assigned literal. Undoes the trail, the+-- assignment, sets `noLevel', undoes reason.+--+-- Does /not/ touch `dl'.+undoOne :: MAssignment s -> DPLLMonad s ()+{-# INLINE undoOne #-}+undoOne m = do+ trl <- gets trail+ lvl <- gets level+ case trl of+ [] -> error "undoOne of empty trail"+ (l:trl') -> do+ liftST $ m `unassign` l+ liftST $ writeArray lvl (var l) noLevel+ modify $ \s ->+ s{ trail = trl'+ , reason = Map.delete (var l) (reason s) }++-- | Increase the recorded activity of given variable.+bump :: Var -> DPLLMonad s ()+{-# INLINE bump #-}+bump v = varOrderMod v (+ varInc)++varInc :: Double+varInc = 1.0+ +++-- *** Impossible to satisfy++-- | /O(1)/. Test for unsatisfiability.+--+-- The DPLL paper says, ''A problem is unsatisfiable if there is a conflicting+-- clause and there are no decision literals in @m@.'' But we were deciding+-- on all literals *without* creating a conflicting clause. So now we also+-- test whether we've made all possible decisions, too.+unsat :: Maybe a -> DPLLStateContents s -> Bool+{-# INLINE unsat #-}+unsat maybeConflict (SC{dl=dl}) = isUnsat+ where isUnsat = (null dl && isJust maybeConflict)+ -- or BitSet.size bad == numVars cnf++++-- ** Helpers++-- *** Clause compaction++-- | Keep the smaller half of the learned clauses.+compactDB :: DPLLMonad s ()+compactDB = do+ n <- numVars `liftM` gets cnf+ lArr <- gets learnt+ clauses <- liftST $ (nub . Fl.concat) `liftM`+ forM [L (- n) .. L n]+ (\v -> do val <- readArray lArr v ; writeArray lArr v []+ return val)+ let clauses' = take (length clauses `div` 2)+ $ sortBy (comparing (length . snd)) clauses+ liftST $ forM_ clauses'+ (\ wCl@(r, _) -> do+ (x, y) <- readSTRef r+ modifyArray lArr x $ const (wCl:)+ modifyArray lArr y $ const (wCl:))++-- *** Unit propagation++-- | Add clause to the watcher lists, unless clause is a singleton; if clause+-- is a singleton, `enqueue's fact and returns `False' if fact is in conflict,+-- `True' otherwise. This function should be called exactly once per clause,+-- per run. It should not be called to reconstruct the watcher list when+-- propagating.+--+-- Currently the watched literals in each clause are the first two.+watchClause :: MAssignment s+ -> Clause+ -> Bool -- ^ Is this clause learned?+ -> DPLLMonad s Bool+{-# INLINE watchClause #-}+watchClause m c isLearnt = do+ conf <- gets dpllConfig+ case c of+ [] -> return True+ [l] -> do result <- enqueue m l (Just c)+ levelArr <- gets level+ liftST $ writeArray levelArr (var l) 0+ return result+ _ -> if configUseWatchedLiterals conf then+ do let p = (negate (c !! 0), negate (c !! 1))+ insert annCl@(_, cl) list -- avoid watching dup clauses+ | any (\(_, c) -> cl == c) list = list+ | otherwise = annCl:list+ r <- liftST $ newSTRef p+ let annCl = (r, c)+ addCl arr = do modifyArray arr (fst p) $ const (annCl:)+ modifyArray arr (snd p) $ const (annCl:)+ get >>= liftST . addCl . (if isLearnt then learnt else watches)+ return True+ else do modify $ \s ->+ let cs = c `Set.insert` (clauses . cnf) s+ in s{ cnf = (cnf s){ clauses = cs+ , numClauses = Set.size cs } }+ return True++-- | Enqueue literal in the `propQ' and place it in the current assignment.+-- If this conflicts with an existing assignment, returns @False@; otherwise+-- returns @True@. In case there is a conflict, the assignment is /not/+-- altered.+--+-- Also records decision level, modifies trail, and records reason for+-- assignment.+enqueue :: MAssignment s+ -> Lit -- ^ The literal that has been assigned true.+ -> Maybe Clause -- ^ The reason for enqueuing the literal. Including+ -- a non-@Nothing@ value here adjusts the `reason'+ -- map.+ -> DPLLMonad s Bool+{-# INLINE enqueue #-}+-- enqueue _m l _r | trace ("enqueue " ++ show l) $ False = undefined+enqueue m l r = do+ mFr <- unsafeFreezeAss m+ case l `statusUnder` mFr of+ Right b -> return b -- conflict/already assigned+ Left () -> do+ liftST $ m `assign` l+ -- assign decision level for literal+ gets (level &&& (length . dl)) >>= \(levelArr, dlInt) ->+ liftST (writeArray levelArr (var l) dlInt)+ modify $ \s -> s{ trail = l : (trail s)+ , propQ = propQ s Seq.|> l } + when (isJust r) $+ modifySlot reason $ \s m -> s{reason = Map.insert (var l) (fromJust r) m}+ return True++-- | Pop the `propQ'. Error (crash) if it is empty.+dequeue :: DPLLMonad s Lit+{-# INLINE dequeue #-}+dequeue = do+ q <- gets propQ+ case Seq.viewl q of+ Seq.EmptyL -> error "dequeue of empty propQ"+ top Seq.:< q' -> do+ modify $ \s -> s{propQ = q'}+ return top++-- | Clear the `propQ'.+clearQueue :: DPLLMonad s ()+{-# INLINE clearQueue #-}+clearQueue = modify $ \s -> s{propQ = Seq.empty}++-- *** Dynamic variable ordering++-- | Modify priority of variable; takes care of @Double@ overflow.+varOrderMod :: Var -> (Double -> Double) -> DPLLMonad s ()+varOrderMod v f = do+ vo <- varOrderArr `liftM` gets varOrder+ vActivity <- liftST $ readArray vo v+ when (f vActivity > 1e100) $ rescaleActivities vo+ liftST $ writeArray vo v (f vActivity)+ where+ rescaleActivities vo = liftST $ do+ indices <- range `liftM` getBounds vo+ forM_ indices (\i -> modifyArray vo i $ const (* 1e-100))+++-- | Retrieve the maximum-priority variable from the variable order.+varOrderGet :: IAssignment -> FrozenVarOrder -> Maybe Var+{-# INLINE varOrderGet #-}+varOrderGet mFr (FrozenVarOrder voFr) =+ -- find highest var undef under mFr, then find one with highest activity+ (`fmap` goUndef highestIndex) $ \start -> goActivity start start+ where+ highestIndex = snd . bounds $ voFr+ maxActivity v v' = if voFr!v > voFr!v' then v else v'++ -- @goActivity current highest@ returns highest-activity var+ goActivity !(V 0) !h = h+ goActivity !v@(V n) !h = if v `isUndefUnder` mFr+ then goActivity (V $! n-1) (v `maxActivity` h)+ else goActivity (V $! n-1) h++ -- returns highest var that is undef under mFr+ goUndef !(V 0) = Nothing+ goUndef !v@(V n) | v `isUndefUnder` mFr = Just v+ | otherwise = goUndef (V $! n-1)+++-- *** Generic state transition notation++-- | Guard a transition action. If the boolean is true, return the action+-- given as an argument. Otherwise, return `Nothing'.+(==>) :: (Monad m) => Bool -> m a -> Maybe (m a)+(==>) b amb = guard b >> return amb++infixr 6 ==>++-- | @flip fmap@.+(>=>) :: (Monad m) => Maybe a -> (a -> m b) -> Maybe (m b)+{-# INLINE (>=>) #-}+(>=>) = flip fmap++infixr 6 >=>+++-- | Choice of state transitions. Choose the leftmost action that isn't+-- @Nothing@, or return @Nothing@ otherwise.+(><) :: (Monad m) => Maybe (m a) -> Maybe (m a) -> Maybe (m a)+a1 >< a2 =+ case (a1, a2) of+ (Nothing, Nothing) -> Nothing+ (Just _, _) -> a1+ _ -> a2++infixl 5 ><++-- *** Misc++showAssignment a = intercalate " " ([show (a!i) | i <- range . bounds $ a,+ (a!i) /= 0])++initialActivity :: Double+initialActivity = 1.0++instance Error (Lit, Clause) where+ noMsg = (L 0, [])++instance Error () where+ noMsg = ()+++data Stats = Stats+ { statsNumConfl :: Int64+ , statsNumConflTotal :: Int64+ , statsNumLearnt :: Int64+ , statsAvgLearntLen :: Double+ , statsNumDecisions :: Int64+ , statsNumImpl :: Int64 }++-- the show instance uses the wrapped string.+newtype NonStupidString = Stupid { stupefy :: String }+instance Show NonStupidString where+ show = stupefy++instance Show Stats where+ show = show . statTable++statTable :: Stats -> Tabular.T NonStupidString+statTable s =+ Tabular.mkTable+ [ [Stupid "Num. Conflicts"+ ,Stupid $ show (statsNumConflTotal s)]+ , [Stupid "Num. Learned Clauses"+ ,Stupid $ show (statsNumLearnt s)]+ , [Stupid " --> Avg. Lits/Clause"+ ,Stupid $ show (statsAvgLearntLen s)]+ , [Stupid "Num. Decisions"+ ,Stupid $ show (statsNumDecisions s)]+ , [Stupid "Num. Propagations"+ ,Stupid $ show (statsNumImpl s)] ]++statSummary :: Stats -> String+statSummary s =+ show (Tabular.mkTable+ [[Stupid $ show (statsNumConflTotal s) ++ " Conflicts"+ ,Stupid $ "| " ++ show (statsNumLearnt s) ++ " Learned Clauses"+ ++ " (avg " ++ printf "%.2f" (statsAvgLearntLen s)+ ++ " lits/clause)"]])+++extractStats :: DPLLMonad s Stats+extractStats = do+ s <- get+ learntArr <- liftST $ unsafeFreezeWatchArray (learnt s)+ let learnts = (nub . Fl.concat)+ [ map (sort . snd) (learntArr!i)+ | i <- (range . bounds) learntArr ] :: [Clause]+ stats =+ Stats { statsNumConfl = numConfl s+ , statsNumConflTotal = numConflTotal s+ , statsNumLearnt = fromIntegral $ length learnts+ , statsAvgLearntLen =+ fromIntegral (foldl' (+) 0 (map length learnts))+ / fromIntegral (statsNumLearnt stats)+ , statsNumDecisions = numDecisions s+ , statsNumImpl = numImpl s }+ return stats++unsafeFreezeWatchArray :: WatchArray s -> ST s (Array Lit [WatchedPair s])+unsafeFreezeWatchArray = freeze++-- | The assignment as a list of signed literals.+litAssignment :: IAssignment -> [Lit]+litAssignment mFr = map (L . (mFr!)) (range . bounds $ mFr)++---------- TESTING ----------+++-- | Verify the assigment is well-formed and satisfies the CNF problem. This+-- function is run after a solution is discovered, just to be safe.+--+-- Makes sure each slot in the assignment is either 0 or contains its+-- (possibly negated) corresponding literal, and verifies that each clause is+-- made true by the assignment.+verify :: IAssignment -> CNF -> Maybe [(Clause, Either () Bool)]+verify m cnf =+ -- m is well-formed+-- Fl.all (\l -> m!(V l) == l || m!(V l) == negate l || m!(V l) == 0) [1..numVars cnf]+ let unsatClauses = toList $+ Set.filter (not . isTrue . snd) $+ Set.map (\c -> (c, c `statusUnder` m)) (clauses cnf)+ in if null unsatClauses+ then Nothing+ else Just unsatClauses+ where isTrue (Right True) = True+ isTrue _ = False
+ Funsat/Utils.hs view
@@ -0,0 +1,111 @@+{-# LANGUAGE PatternSignatures+ ,MultiParamTypeClasses+ ,FunctionalDependencies+ ,FlexibleInstances+ ,FlexibleContexts #-}++{-+ This file is part of funsat.++ funsat is free software: you can redistribute it and/or modify+ it under the terms of the GNU Lesser General Public License as published by+ the Free Software Foundation, either version 3 of the License, or+ (at your option) any later version.++ funsat is distributed in the hope that it will be useful,+ but WITHOUT ANY WARRANTY; without even the implied warranty of+ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the+ GNU Lesser General Public License for more details.++ You should have received a copy of the GNU Lesser General Public License+ along with funsat. If not, see <http://www.gnu.org/licenses/>.++ Copyright 2008 Denis Bueno+-}+++{-|++Generic utilities that happen to be used in the SAT solver. In pretty much+every case, these functions will be useful for any number of manipulations,+and are not SAT-solver specific.++-}+module Funsat.Utils where++import Control.Monad.ST.Strict+import Control.Monad.State.Lazy hiding ((>=>), forM_)+import Data.Array.ST+import Data.Array.Unboxed+import Data.Foldable hiding (sequence_)+import Data.List (foldl1')+import Debug.Trace (trace)+import Prelude hiding (sum, concatMap, elem, foldr, foldl, any, maximum)+import System.IO.Unsafe (unsafePerformIO)+import System.IO (hPutStr, stderr)+import qualified Data.Foldable as Fl+import qualified Data.List as List+++{-# INLINE mytrace #-}+mytrace msg expr = unsafePerformIO $ do+ hPutStr stderr msg+ return expr++outputConflict fn g x = unsafePerformIO $ do writeFile fn g+ return x+++-- | /O(1)/ Whether a list contains a single element.+isSingle :: [a] -> Bool+{-# INLINE isSingle #-}+isSingle [_] = True+isSingle _ = False++-- | Modify a value inside the state.+modifySlot :: (MonadState s m) => (s -> a) -> (s -> a -> s) -> m ()+{-# INLINE modifySlot #-}+modifySlot slot f = modify $ \s -> f s (slot s)++-- | @modifyArray arr i f@ applies the function @f@ to the index @i@ and the+-- current value of the array at index @i@, then writes the result into @i@ in+-- the array.+modifyArray :: (Monad m, MArray a e m, Ix i) => a i e -> i -> (i -> e -> e) -> m ()+{-# INLINE modifyArray #-}+modifyArray arr i f = readArray arr i >>= writeArray arr i . (f i)++-- | Same as @newArray@, but helping along the type checker.+newSTUArray :: (MArray (STUArray s) e (ST s), Ix i)+ => (i, i) -> e -> ST s (STUArray s i e)+newSTUArray = newArray++newSTArray :: (MArray (STArray s) e (ST s), Ix i)+ => (i, i) -> e -> ST s (STArray s i e)+newSTArray = newArray+++-- | Count the number of elements in the list that satisfy the predicate.+count :: (a -> Bool) -> [a] -> Int+count p = foldl' f 0+ where f x y = x + (if p y then 1 else 0)++-- | /O(1)/ @argmin f x y@ is the argument whose image is least under @f@; if+-- the images are equal, returns the first.+argmin :: Ord b => (a -> b) -> a -> a -> a+argmin f x y = if f x <= f y then x else y++-- | /O(length xs)/ @argminimum f xs@ returns the value in @xs@ whose image+-- is least under @f@; if @xs@ is empty, throws an error.+argminimum :: Ord b => (a -> b) -> [a] -> a+argminimum f = foldl1' (argmin f)+++-- | Show the value with trace, then return it. Useful because you can wrap+-- it around any subexpression to print it when it is forced.+tracing :: (Show a) => a -> a+tracing x = trace (show x) x++-- | Returns a predicate which holds exactly when both of the given predicates+-- hold.+p .&&. q = \x -> p x && q x+
+ LICENSE view
@@ -0,0 +1,165 @@+ GNU LESSER GENERAL PUBLIC LICENSE+ Version 3, 29 June 2007++ Copyright (C) 2007 Free Software Foundation, Inc. <http://fsf.org/>+ Everyone is permitted to copy and distribute verbatim copies+ of this license document, but changing it is not allowed.+++ This version of the GNU Lesser General Public License incorporates+the terms and conditions of version 3 of the GNU General Public+License, supplemented by the additional permissions listed below.++ 0. Additional Definitions. ++ As used herein, "this License" refers to version 3 of the GNU Lesser+General Public License, and the "GNU GPL" refers to version 3 of the GNU+General Public License.++ "The Library" refers to a covered work governed by this License,+other than an Application or a Combined Work as defined below.++ An "Application" is any work that makes use of an interface provided+by the Library, but which is not otherwise based on the Library.+Defining a subclass of a class defined by the Library is deemed a mode+of using an interface provided by the Library.++ A "Combined Work" is a work produced by combining or linking an+Application with the Library. The particular version of the Library+with which the Combined Work was made is also called the "Linked+Version".++ The "Minimal Corresponding Source" for a Combined Work means the+Corresponding Source for the Combined Work, excluding any source code+for portions of the Combined Work that, considered in isolation, are+based on the Application, and not on the Linked Version.++ The "Corresponding Application Code" for a Combined Work means the+object code and/or source code for the Application, including any data+and utility programs needed for reproducing the Combined Work from the+Application, but excluding the System Libraries of the Combined Work.++ 1. Exception to Section 3 of the GNU GPL.++ You may convey a covered work under sections 3 and 4 of this License+without being bound by section 3 of the GNU GPL.++ 2. Conveying Modified Versions.++ If you modify a copy of the Library, and, in your modifications, a+facility refers to a function or data to be supplied by an Application+that uses the facility (other than as an argument passed when the+facility is invoked), then you may convey a copy of the modified+version:++ a) under this License, provided that you make a good faith effort to+ ensure that, in the event an Application does not supply the+ function or data, the facility still operates, and performs+ whatever part of its purpose remains meaningful, or++ b) under the GNU GPL, with none of the additional permissions of+ this License applicable to that copy.++ 3. Object Code Incorporating Material from Library Header Files.++ The object code form of an Application may incorporate material from+a header file that is part of the Library. You may convey such object+code under terms of your choice, provided that, if the incorporated+material is not limited to numerical parameters, data structure+layouts and accessors, or small macros, inline functions and templates+(ten or fewer lines in length), you do both of the following:++ a) Give prominent notice with each copy of the object code that the+ Library is used in it and that the Library and its use are+ covered by this License.++ b) Accompany the object code with a copy of the GNU GPL and this license+ document.++ 4. Combined Works.++ You may convey a Combined Work under terms of your choice that,+taken together, effectively do not restrict modification of the+portions of the Library contained in the Combined Work and reverse+engineering for debugging such modifications, if you also do each of+the following:++ a) Give prominent notice with each copy of the Combined Work that+ the Library is used in it and that the Library and its use are+ covered by this License.++ b) Accompany the Combined Work with a copy of the GNU GPL and this license+ document.++ c) For a Combined Work that displays copyright notices during+ execution, include the copyright notice for the Library among+ these notices, as well as a reference directing the user to the+ copies of the GNU GPL and this license document.++ d) Do one of the following:++ 0) Convey the Minimal Corresponding Source under the terms of this+ License, and the Corresponding Application Code in a form+ suitable for, and under terms that permit, the user to+ recombine or relink the Application with a modified version of+ the Linked Version to produce a modified Combined Work, in the+ manner specified by section 6 of the GNU GPL for conveying+ Corresponding Source.++ 1) Use a suitable shared library mechanism for linking with the+ Library. A suitable mechanism is one that (a) uses at run time+ a copy of the Library already present on the user's computer+ system, and (b) will operate properly with a modified version+ of the Library that is interface-compatible with the Linked+ Version. ++ e) Provide Installation Information, but only if you would otherwise+ be required to provide such information under section 6 of the+ GNU GPL, and only to the extent that such information is+ necessary to install and execute a modified version of the+ Combined Work produced by recombining or relinking the+ Application with a modified version of the Linked Version. (If+ you use option 4d0, the Installation Information must accompany+ the Minimal Corresponding Source and Corresponding Application+ Code. If you use option 4d1, you must provide the Installation+ Information in the manner specified by section 6 of the GNU GPL+ for conveying Corresponding Source.)++ 5. Combined Libraries.++ You may place library facilities that are a work based on the+Library side by side in a single library together with other library+facilities that are not Applications and are not covered by this+License, and convey such a combined library under terms of your+choice, if you do both of the following:++ a) Accompany the combined library with a copy of the same work based+ on the Library, uncombined with any other library facilities,+ conveyed under the terms of this License.++ b) Give prominent notice with the combined library that part of it+ is a work based on the Library, and explaining where to find the+ accompanying uncombined form of the same work.++ 6. Revised Versions of the GNU Lesser General Public License.++ The Free Software Foundation may publish revised and/or new versions+of the GNU Lesser General Public License from time to time. Such new+versions will be similar in spirit to the present version, but may+differ in detail to address new problems or concerns.++ Each version is given a distinguishing version number. If the+Library as you received it specifies that a certain numbered version+of the GNU Lesser General Public License "or any later version"+applies to it, you have the option of following the terms and+conditions either of that published version or of any later version+published by the Free Software Foundation. If the Library as you+received it does not specify a version number of the GNU Lesser+General Public License, you may choose any version of the GNU Lesser+General Public License ever published by the Free Software Foundation.++ If the Library as you received it specifies that a proxy can decide+whether future versions of the GNU Lesser General Public License shall+apply, that proxy's public statement of acceptance of any version is+permanent authorization for you to choose that version for the+Library.
+ Main.hs view
@@ -0,0 +1,172 @@+{-# OPTIONS -cpp #-}++module Main where++{-+ This file is part of funsat.++ funsat is free software: you can redistribute it and/or modify+ it under the terms of the GNU Lesser General Public License as published by+ the Free Software Foundation, either version 3 of the License, or+ (at your option) any later version.++ funsat is distributed in the hope that it will be useful,+ but WITHOUT ANY WARRANTY; without even the implied warranty of+ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the+ GNU Lesser General Public License for more details.++ You should have received a copy of the GNU Lesser General Public License+ along with funsat. If not, see <http://www.gnu.org/licenses/>.++ Copyright 2008 Denis Bueno+-}++import Control.Monad ( when, forM_ )+import Data.Foldable ( fold, toList, elem )+import Data.List ( intercalate )+import Data.Monoid+import Data.Set ( Set )+import Funsat.Solver+ ( solve+ , DPLLConfig(..)+ , defaultConfig+ , CNF+ , GenCNF(..)+ , Solution(..)+ , verify+ , NonStupidString(..)+ , statTable )+import Prelude hiding ( elem )+import System.Console.GetOpt+import System.Environment ( getArgs )+import System.Exit ( ExitCode(..), exitWith )+import Data.Time.Clock+import qualified Data.Set as Set+import qualified Language.CNF.Parse.ParseDIMACS as ParseCNF+import qualified Text.Tabular as Tabular+++#ifdef TESTING+import qualified Properties+#endif++data Feature = WatchedLiterals+ | ClauseLearning+ | Restarts+ | VSIDS+ deriving (Eq, Ord)+instance Show Feature where+ show WatchedLiterals = "watched literals"+ show ClauseLearning = "conflict clause learning"+ show Restarts = "restarts"+ show VSIDS = "dynamic variable ordering"++allFeatures :: Set Feature+allFeatures = Set.fromList [WatchedLiterals, ClauseLearning, Restarts, VSIDS]+++validOptions :: [OptDescr RunOptions]+validOptions =+-- [ Option [] ["no-clause-learning"] (NoArg $ disableF ClauseLearning)+-- "Use naivest clause learning."+-- , Option [] ["no-watched-literals"] (NoArg $ disableF WatchedLiterals)+-- "Just traverse the formula to find unit clauses."+-- , Option [] ["no-vsids"] (NoArg $ disableF VSIDS)+-- "Use static variable ordering."+ [ Option [] ["no-restarts"] (NoArg $ disableF Restarts)+ "Never restart."+ , Option [] ["verify"] (NoArg RunTests)+ "Run quickcheck properties and unit tests."+ , Option [] ["print-features"] (NoArg (PrintFeatures Set.empty))+ "Print the optimisations the SAT solver supports." ]++disableF :: Feature -> RunOptions+disableF = Disable . Set.singleton++data RunOptions = Disable (Set Feature) -- disable certain features+ | RunTests -- run unit tests+ | PrintFeatures (Set Feature) -- disable certain features+-- Combines features, choosing only RunTests and PrintFeatures if present,+-- otherwise combining sets of features to disable.+instance Monoid RunOptions where+ mempty = Disable Set.empty+ mappend (PrintFeatures f) (PrintFeatures f') = PrintFeatures (f `Set.union` f')+ mappend (PrintFeatures f) (Disable f') = PrintFeatures (f `Set.union` f')+ mappend o@(PrintFeatures _) _ = o+ mappend o@RunTests _ = o+ mappend (Disable s) (Disable s') = Disable (s `Set.union` s')+ mappend (Disable _) o = o -- non-feature selection options override++parseOptions :: [String] -> IO (RunOptions, [FilePath])+parseOptions args = do+ let (runoptionss, filepaths, errors) = getOpt RequireOrder validOptions args+ when (not (null errors)) $ do { mapM_ putStr errors ;+ putStrLn (usageInfo usageHeader validOptions) ;+ exitWith (ExitFailure 1) }+ return $ (fold runoptionss, filepaths)++main :: IO ()+main = do+ (opts, files) <- getArgs >>= parseOptions+ case opts of+#ifdef TESTING+ RunTests -> Properties.main+#endif+ PrintFeatures disabled ->+ putStrLn $ intercalate ", " $ map show $+ toList (allFeatures Set.\\ disabled)+ Disable features -> do+ putStr "Enabled features: "+ putStrLn $ intercalate ", " $ map show $+ toList (allFeatures Set.\\ features)+ forM_ files $ \path -> readFile path >>= parseAndSolve path+ where+ parseAndSolve path contents = do+ let cnf = asCNF $ ParseCNF.parseCNF path contents+ putStrLn $ show (numVars cnf) ++ " variables, "+ ++ show (numClauses cnf) ++ " clauses"+ Set.map seqList (clauses cnf)+ `seq` putStrLn ("Solving " ++ path ++ "...")+ startingTime <- getCurrentTime+ let cfg =+ (defaultConfig cnf)+ { configUseVSIDS = not $ VSIDS `elem` features+ , configUseWatchedLiterals = not $ WatchedLiterals `elem` features+ , configUseRestarts = not $ Restarts `elem` features+ , configUseLearning = not $ ClauseLearning `elem` features }+ (solution, stats) = solve cfg cnf+ endingTime <- solution `seq` getCurrentTime+ print solution+ print $ statTable stats `Tabular.combine`+ Tabular.mkTable+ [[ Stupid "Real time "+ , Stupid $ show (diffUTCTime endingTime startingTime)]]+ case solution of+ Sat m -> do+ putStrLn "Verifying..."+ case verify m cnf of+ Just problemClauses ->+ do putStrLn "VERIFICATION ERROR!"+ print problemClauses+ Nothing -> return ()+#ifdef TESTING+-- putStrLn $+-- "Minimal erroneous CNF:\n"+-- ++ show (Properties.minimalError cnf)+#endif TESTING+ Unsat -> return ()+++usageHeader = "Usage: funsat [options] <cnf-filename> ... <cnf-filename>"++seqList l@[] = l+seqList l@(x:xs) = x `seq` seqList xs `seq` l+++-- | Convert parsed CNF to internal representation.+asCNF :: ParseCNF.CNF -> CNF+asCNF (ParseCNF.CNF v c is) =+ CNF { numVars = v+ , numClauses = c+ , clauses = Set.fromList . map (map fromIntegral) $ is }+
+ README view
@@ -0,0 +1,26 @@+-*- mode: outline -*-++* A DPLL-style SAT solver in pure Haskell+Install using the typical Cabal procedure:++$ ./Setup.lhs configure+$ ./Setup.lhs build++This will produce a binary called funsat at ./dist/build/funsat/funsat and a+standalone library interface for the solver. If you feel like profiling the+code, uncomment the profiling executable in funsat.cabal, and a profiling+binary will automatically be built in ./dist/build/funsat-prof/funsat-prof.++** Dependencies+All the dependences are cabal-ised and available from hackage. URLs below.++They're also available in subdirectories.++*** parse-dimacs [cnf]+A haskell CNF file parser.++http://hackage.haskell.org/cgi-bin/hackage-scripts/package/parse-dimacs++*** bitset [bitset]+http://hackage.haskell.org/cgi-bin/hackage-scripts/package/bitset+
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ Text/Tabular.hs view
@@ -0,0 +1,77 @@+{-+ This file is part of funsat.++ funsat is free software: you can redistribute it and/or modify+ it under the terms of the GNU Lesser General Public License as published by+ the Free Software Foundation, either version 3 of the License, or+ (at your option) any later version.++ funsat is distributed in the hope that it will be useful,+ but WITHOUT ANY WARRANTY; without even the implied warranty of+ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the+ GNU Lesser General Public License for more details.++ You should have received a copy of the GNU Lesser General Public License+ along with funsat. If not, see <http://www.gnu.org/licenses/>.++ Copyright 2008 Denis Bueno+-}++{-|++Tabular output.++Converting any matrix of showable data types into a tabular form for which the+layout is automatically done properly. Currently there is no maximum row+width, just a dynamically-calculated column width.++If the input matrix is mal-formed, the largest well-formed submatrix is+chosen. That is, elements along too-long dimensions are chopped off.++-}+module Text.Tabular( T(..), mkTable, combine, unTable ) where++import Data.List( intercalate )++newtype T a = T [Row a] -- table is a list of rows+newtype Row a = Row [Cell a]+data Cell a = Cell { cellWidth :: !Int+ -- the width of a cell is the max of the widths of the+ -- string representations of all the elements in the column+ -- in which this cell occurs+ , cellData :: !a } -- element printed in box of colWidth++mkTable :: (Show a) => [[a]] -> T a+mkTable rows = T $ mkRows rows+ where+ widths = colWidths rows+ mkRows rows = [ Row (map mkCell (zip widths row)) | row <- rows ]+ mkCell = uncurry Cell++unTable :: T a -> [[a]]+unTable (T rows) = [ map cellData r | (Row r) <- rows ]++combine :: (Show a) => T a -> T a -> T a+-- slow impl but works+combine t t' = mkTable (unTable t ++ unTable t')++-- returns a list of the widths of each column+colWidths :: (Show a) => [[a]] -> [Int]+colWidths = map (maximum . map (length . show)) . zipn++-- Pretty, columnar output.+instance (Show a) => Show (T a) where+ show (T rows) = intercalate "\n" $ map showRow rows + where+ showRow (Row cols) = intercalate " " $ colStrings+ where+ colStrings = [ padString (cellWidth c) (show d)+ | c@(Cell {cellData=d}) <- cols ]++padString maxWidth str = str ++ replicate padLen ' '+ where padLen = maxWidth - length str++zipn xss | any null xss = []+zipn xss = map head xss : zipn (map tail xss)++
+ funsat.cabal view
@@ -0,0 +1,63 @@+Name: funsat+Version: 0.4+Cabal-Version: >= 1.2+Description:++ Funsat is a native Haskell SAT solver that uses modern techniques for+ solving SAT instances. Current features include two-watched literals,+ conflict-directed learning, non-chronological backtracking, a VSIDS-like+ dynamic variable ordering, and restarts. It is possible to use funsat+ both as a library and as a standalone executable.++Synopsis: A modern DPLL-style SAT solver+Category: Algorithms+Stability: alpha+License: LGPL+License-file: LICENSE+Author: Denis Bueno+Maintainer: Denis Bueno <dbueno@gmail.com>+Build-type: Simple+Extra-source-files: README+++Executable funsat+ Main-is: Main.hs+ Ghc-options: -W+ Extensions: CPP+ CPP-options: -DTESTING+ Hs-source-dirs: . tests+ Other-modules:+ Funsat.Solver+ Funsat.FastDom+ Funsat.Utils+ Text.Tabular+ DPLL.Monad+ Control.Monad.MonadST+ Properties++ Build-Depends: base, parsec, containers, pretty, mtl+ , array, QuickCheck, parse-dimacs, bitset+ , fgl, time++-- Executable funsat-prof+-- Main-is: Main.hs+-- Ghc-options: -W -prof -auto-all+-- Extensions: CPP+-- CPP-options: -DTESTING+-- Hs-source-dirs: . tests+-- Other-modules: DPLLSat Properties FastDom Utils Text.Tabular DPLL.Monad+-- Control.Monad.MonadST+-- Build-Depends: base, parsec, containers, pretty, mtl+-- , random, array, QuickCheck, parse-dimacs, bitset+-- , fgl, time+++Library+ Exposed-modules: Funsat.Solver DPLL.Monad Control.Monad.MonadST Text.Tabular+ Other-modules: Funsat.FastDom Funsat.Utils+ Ghc-options: -W -funbox-strict-fields+ Extensions: CPP+ Hs-source-dirs: . tests+ Build-Depends: base, parsec, containers, pretty, mtl+ , random, array, QuickCheck, parse-dimacs, bitset+ , fgl
+ tests/Properties.hs view
@@ -0,0 +1,488 @@+{-# OPTIONS_GHC -fglasgow-exts #-}+module Properties where++{-+ This file is part of DPLLSat.++ DPLLSat is free software: you can redistribute it and/or modify+ it under the terms of the GNU Lesser General Public License as published by+ the Free Software Foundation, either version 3 of the License, or+ (at your option) any later version.++ DPLLSat is distributed in the hope that it will be useful,+ but WITHOUT ANY WARRANTY; without even the implied warranty of+ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the+ GNU Lesser General Public License for more details.++ You should have received a copy of the GNU Lesser General Public License+ along with DPLLSat. If not, see <http://www.gnu.org/licenses/>.++ Copyright 2008 Denis Bueno+-}++import Funsat.Solver hiding ( (==>) )++import Control.Monad (replicateM)+import Data.Array.Unboxed+import Data.BitSet (hash)+import Data.Bits+import Data.Foldable hiding (sequence_)+import Data.List (nub, splitAt, unfoldr, delete, sort, sortBy)+import Data.Maybe+import Data.Ord( comparing )+import Debug.Trace+import Language.CNF.Parse.ParseDIMACS( parseCNF )+import Prelude hiding ( or, and, all, any, elem, minimum, foldr, splitAt, concatMap+ , sum, concat )+import System.Random+import Test.QuickCheck hiding (defaultConfig)+import Funsat.Utils( count, argmin )+import qualified Data.Foldable as Foldable+import qualified Data.List as List+import qualified Data.Set as Set+import qualified Test.QuickCheck as QC+import qualified Language.CNF.Parse.ParseDIMACS as ParseCNF+++main :: IO ()+main = do+-- let s = solve1 prob1+-- case s of+-- Unsat -> return ()+-- Sat m -> if not (verifyBool m prob1)+-- then putStrLn (show (find (`isFalseUnder` m) prob1))+-- else return ()++ --setStdGen (mkStdGen 42)+ check config prop_randAssign+ check config prop_allIsTrueUnderA+ check config prop_noneIsFalseUnderA+ check config prop_noneIsUndefUnderA+ check config prop_negIsFalseUnder+ check config prop_negNotUndefUnder+ check config prop_outsideUndefUnder+ check config prop_clauseStatusUnderA+ check config prop_negDefNotUndefUnder+ check config prop_undefUnderImpliesNegUndef+ check config prop_litHash+ check config prop_varHash+ check config prop_count++ -- Add more tests above here. Setting the rng keeps the SAT instances+ -- the same even if more tests are added above. Reproducible results+ -- are important.+ setStdGen (mkStdGen 42)+ check solveConfig prop_solveCorrect++config = QC.defaultConfig { configMaxTest = 1000 }++-- Special configuration for the "solve this random instance" tests.+solveConfig = QC.defaultConfig { configMaxTest = 2000 }++myConfigEvery testnum args = show testnum ++ ": " ++ show args ++ "\n\n"++-- * Tests+prop_solveCorrect (cnf :: CNF) =+ label "prop_solveCorrect" $+ trivial (numClauses cnf < 2 || numVars cnf < 2) $+ classify (numClauses cnf > 15 || numVars cnf > 10) "c>15, v>10" $+ classify (numClauses cnf > 30 || numVars cnf > 20) "c>30, v>20" $+ classify (numVars cnf > 20) "c>30, v>30" $+ case solve (defaultConfig cnf) cnf of+ (Sat m,_) -> label "SAT" $ verifyBool m cnf+ (Unsat,_) -> label "UNSAT-unverified" $ True+++prop_allIsTrueUnderA (m :: IAssignment) =+ label "prop_allIsTrueUnderA"$+ allA (\i -> if i /= 0 then L i `isTrueUnder` m else True) m++prop_noneIsFalseUnderA (m :: IAssignment) =+ label "prop_noneIsFalseUnderA"$+ not $ anyA (\i -> if i /= 0 then L i `isFalseUnder` m else False) m++prop_noneIsUndefUnderA (m :: IAssignment) =+ label "prop_noneIsUndefUnderA"$+ not $ anyA (\i -> if i /= 0 then L i `isUndefUnder` m else False) m++prop_negIsFalseUnder (m :: IAssignment) =+ label "prop_negIsFalseUnder"$+ allA (\l -> if l /= 0 then negate (L l) `isFalseUnder` m else True) m++prop_negNotUndefUnder (m :: IAssignment) =+ label "prop_negNotUndefUnder"$+ allA (\l -> if l /= 0 then not (negate (L l) `isUndefUnder` m) else True) m++prop_outsideUndefUnder (l :: Lit) (m :: IAssignment) =+ label "prop_outsideUndefUnder"$+ trivial ((unVar . var) l > rangeSize (bounds m)) $+ inRange (bounds m) (var l) ==>+ trivial (m `contains` l || m `contains` negate l) $+ not (m `contains` l) && not (m `contains` (negate l)) ==>+ l `isUndefUnder` m++prop_negDefNotUndefUnder (l :: Lit) (m :: IAssignment) =+ label "prop_negDefNotUndefUnder" $+ inRange (bounds m) (var l) ==>+ m `contains` l || m `contains` (negate l) ==>+ l `isTrueUnder` m || negate l `isTrueUnder` m++prop_undefUnderImpliesNegUndef (l :: Lit) (m :: IAssignment) =+ label "prop_undefUnderImpliesNegUndef" $+ inRange (bounds m) (var l) ==>+ trivial (m `contains` l) $+ l `isUndefUnder` m ==> negate l `isUndefUnder` m+ ++prop_clauseStatusUnderA (c :: Clause) (m :: IAssignment) =+ label "prop_clauseStatusUnderA" $+ classify expectTrueTest "expectTrue"$+ classify expectFalseTest "expectFalseTest"$+ classify expectUndefTest "expectUndefTest"$+ if expectTrueTest then c `isTrueUnder` m+ else if expectFalseTest then c `isFalseUnder` m+ else c `isUndefUnder` m+ where+ expectTrueTest = not . null $ c `List.intersect` (map L $ elems m)+ expectFalseTest = all (`isFalseUnder` m) c+ expectUndefTest = not expectTrueTest && not expectFalseTest++-- Verify assignments generated are sane, i.e. no assignment contains an+-- element and its negation.+prop_randAssign (a :: IAssignment) =+ label "randAssign"$+ not $ anyA (\l -> if l /= 0 then a `contains` (negate $ L l) else False) a++-- unitPropFar should stop only if it can't propagate anymore.+-- prop_unitPropFarthest (m :: Assignment) (cnf :: CNF) =+-- label "prop_unitPropFarthest"$+-- case unitPropFar m cnf of+-- Nothing -> label "no propagation" True+-- Just m' -> label "propagated" $ not (anyUnit m' cnf)++-- Unit propagation may only add to the given assignment.+-- prop_unitPropOnlyAdds (m :: Assignment) (cnf :: CNF) =+-- label "prop_unitPropOnlyAdds"$+-- case unitPropFar m cnf of+-- Nothing -> label "no propagation" True+-- Just m' -> label "propagated" $ all (\l -> elem l m') m++-- Make sure the bit set will work.++prop_litHash (k :: Lit) (l :: Lit) =+ label "prop_litHash" $+ hash k == hash l <==> k == l++prop_varHash (k :: Var) l =+ label "prop_varHash" $+ hash k == hash l <==> k == l+++(<==>) = iff+infixl 3 <==>+++-- newtype WPTest s = WPTest (WatchedPair s)++-- instance Arbitrary (WPTest s) where+-- arbitrary = sized sizedWPTest+-- where sizedWPTest n = do+-- [lit1, lit2] <- 2 `uniqElts` 1+-- clause :: Clause <- arbitrary+-- return $ runST $+-- do r <- newSTRef (lit1, lit2)+-- return (r, lit1 : lit2 : clause)++newtype Nat = Nat { unNat :: Int }+ deriving (Eq, Ord)+instance Show Nat where+ show (Nat i) = "Nat " ++ show i+instance Num Nat where+ (Nat x) + (Nat y) = Nat (x + y)+ (Nat x) - (Nat y) | x >= y = Nat (x - y)+ | x < y = error "Nat: subtraction out of range"+ (Nat x) * (Nat y) = Nat (x * y)+ abs = id+ signum (Nat n) | n == 0 = 0+ | n > 0 = 1+ | n < 0 = error "Nat: signum of negative number"+ fromInteger n | n >= 0 = Nat (fromInteger n)+ | n < 0 = error "Negative natural literal found"++instance Arbitrary Nat where+ arbitrary = sized $ \n -> do i <- choose (0, n)+ return (fromIntegral i)+++-- sanity checking for Arbitrary Nat instance.+prop_nat (xs :: [Nat]) = trivial (null xs) $ sum xs >= 0+prop_nat1 (xs :: [Nat]) = trivial (null xs) $ unNat (sum xs) == sum (map unNat xs)++prop_count p xs =+ label "prop_count" $+ count p xs == length (filter p xs)+ where _types = xs :: [Int]++prop_argmin f x y =+ label "prop_argmin" $+ f x /= f y ==>+ argmin f x y == m+ where m = if f x < f y then x else y++instance Show (a -> b) where+ show = const "<fcn>"+++++-- * Helpers++++allA :: (IArray a e, Ix i) => (e -> Bool) -> a i e -> Bool+allA p a = all (p . (a !)) (range . bounds $ a)++anyA :: (IArray a e, Ix i) => (e -> Bool) -> a i e -> Bool+anyA p a = any (p . (a !)) (range . bounds $ a)++_findA :: (IArray a e, Ix i) => (e -> Bool) -> a i e -> Maybe e+_findA p a = (a !) `fmap` find (p . (a !)) (range . bounds $ a)+++-- Generate exactly n distinct, random things from given enum, starting at+-- element given. Obviously only really works for infinite enumerations.+uniqElts :: (Enum a) => Int -> a -> Gen [a]+uniqElts n x =+ do is <- return [x..]+ choices <-+ sequence $ map+ (\i -> do {b <- oneof [return True, return False];+ return $ if b then Just i else Nothing})+ is+ return $ take n $ catMaybes choices++-- Send this as a patch for quickcheck, maybe.+iff :: Bool -> Bool -> Property+first `iff` second =+ classify first "first" $+ classify (not first) "not first" $+ classify second "second" $+ classify (not second) "not second" $+ if first then second+ else not second+ && if second then first+ else not first+++fromRight (Right x) = x+fromRight (Left _) = error "fromRight: Left"+++_intAssignment :: Int -> Integer -> [Lit]+_intAssignment n i = map nthBitLit [0..n-1]+ -- nth bit of i as a literal+ where nthBitLit n = toLit (n + 1) $ i `testBit` n+ toLit n True = L n+ toLit n False = negate $ L n+ +++_powerset :: [a] -> [[a]]+_powerset [] = [[]]+_powerset (x:xs) = xss /\/ map (x:) xss+ where+ xss = _powerset xs++ (/\/) :: [a] -> [a] -> [a]+ [] /\/ ys = ys+ (x:xs) /\/ ys = x : (ys /\/ xs)+++-- * Generators++instance Arbitrary Var where+ arbitrary = sized $ \n -> V `fmap` choose (1, n)+instance Arbitrary Lit where+ arbitrary = sized $ sizedLit++-- Generates assignment that never has a subset {l, -l}.+instance Arbitrary IAssignment where+ arbitrary = sized $ assign'+ where + assign' n = do lits :: [Lit] <- vector n+ return $ array (V 1, V n) $ map (\i -> (var i, unLit i))+ (nub lits)++instance Arbitrary CNF where+ arbitrary = sized genRandom3SAT++sizedLit n = do+ v <- choose (1, n)+ t <- oneof [return id, return negate]+ return $ L (t v)++genRandom3SAT :: Int -> Gen CNF+genRandom3SAT n =+ do let clausesPerVar = 3.0+ nClauses = ceiling (fromIntegral nVars * clausesPerVar)+ clauseList <- replicateM nClauses arbClause+ return $ CNF { numVars = nVars+ , numClauses = nClauses+ , clauses = Set.fromList clauseList }+ where + nVars = n `div` 3+ arbClause :: Gen Clause+ arbClause = do+ a <- sizedLit nVars+ b <- sizedLit nVars+ c <- sizedLit nVars+ return [a,b,c]+++genCNF2 n = gen (fromIntegral n)+ where+ gen n =+ let _g = n `div` 4+ lits :: [Lit] = map L [1..n]+ genClause1 [a,b,c,d] =+ map (map negate) [[a,b,c], [a,b,d], [a,c,d], [b,c,d]]+ genClause1 _ = error "genClause1: bad arg"+ genClause2 [a,b,c,d] = [[a,b,c], [a,b,d], [a,c,d], [b,c,c]]+ genClause2 _ = error "genClause2: bad arg"+ _genUnsat [a,b,c,d,e] =+ map (map negate)+ [[a,b,c,d]+ ,[a,b,c,e]+ ,[a,b,d,e]+ ,[a,c,d, negate e]+ ,[b,c,d, negate e]]+ _genUnsat _ = error "genUnsat: bad arg"+ in do groups1 <- return $ concatMap genClause1 $ windows 4 lits+ lits' <- permute lits+ groups2 <- return $ concatMap genClause2 $ windows 4 lits'+ return $+ CNF {numVars = n+ ,numClauses = length groups1 + length groups1+ ,clauses = Set.fromList $ groups1 ++ groups2}++windows :: Int -> [a] -> [[a]]+windows n xs = if length xs < n+ then []+ else take n xs : windows n (drop n xs)++permute :: [a] -> Gen [a]+permute [] = return []+permute xs = choose (0, length xs - 1) >>= \idx ->+ case splitAt idx xs of+ (pfx, x:xs') -> do perm <- permute $ pfx ++ xs'+ return $ x : perm+ _ -> error "permute: bug"+++-- ** Simplification++class WellFoundedSimplifier a where+ -- | If the argument can be made simpler, a list of one-step simpler+ -- objects. Only in cases where there are multiple "dimensions" to+ -- simplify should the returned list have length more than 1. Otherwise+ -- returns the empty list.+ simplify :: a -> [a]++instance WellFoundedSimplifier a => WellFoundedSimplifier [a] where+ simplify [] = []+ simplify (x:xs) = case simplify x of+ [] -> [xs]+ x's-> map (:xs) x's++instance WellFoundedSimplifier () where+ simplify () = []++instance WellFoundedSimplifier Bool where+ simplify True = [False]+ simplify False = []++instance WellFoundedSimplifier Int where+ simplify i | i == 0 = []+ | i > 0 = [i-1]+ | i < 0 = [i+1]++-- Assign the highest variable and reduce the number of variables.+instance WellFoundedSimplifier CNF where+ simplify f+ | numVars f <= 1 = []+ | numVars f > 1 = [ f{ numVars = numVars f - 1+ , clauses = clauses'+ , numClauses = Set.size clauses' }+-- , f{ clauses = Set.deleteMax (clauses f)+-- , numClauses = numClauses f - 1 }+ ]+ where+ clauses' = foldl' assignVar Set.empty (clauses f)+ pos = L (numVars f)+ neg = negate pos+ assignVar outClauses clause =+ let clause' = neg `delete` clause+ in if pos `elem` clause || null clause' then outClauses+ else clause' `Set.insert` outClauses+++simplifications :: WellFoundedSimplifier a => a -> [a]+simplifications a = concat $ unfoldr (\ xs -> let r = concatMap simplify xs+ in if null r then Nothing+ else Just (r, r))+ [a]++-- Returns smallest CNF simplification that also gives erroneous output.+minimalError :: CNF -> CNF+minimalError f = lastST f satAndWrong (simplifications f)+ where satAndWrong f_inner =+ trace (show (numVars f_inner) ++ "/" ++ show (numClauses f_inner)) $+ case solve1 f_inner of+ (Unsat,_) -> False+ (Sat assignment,_) -> not (verifyBool assignment f_inner)++-- last (takeWhile p xs) in the common case.+-- mnemonic: "last Such That"+lastST def _ [] = def+lastST def p (x:xs) = if p x then lastST x p xs else def++prop_lastST (x :: Int) =+ if not (null xs) && xa > 3 then+ classify True "nontrivial" $+ last (takeWhile p xs) == lastST undefined p xs+ else True `trivial` True+ where p = (> xa `div` 2)+ xs = simplifications xa+ xa = abs x+++getCNF :: Int -> IO CNF+getCNF maxVars = do g <- newStdGen+ return (generate (maxVars * 3) g arbitrary)++prob :: IO ParseCNF.CNF+prob = do let file = "./tests/problems/uf20/uf20-0119.cnf"+ s <- readFile file+ return $ parseCNF file s+++-- | Convert parsed CNF to internal representation.+asCNF :: ParseCNF.CNF -> CNF+asCNF (ParseCNF.CNF v c is) =+ CNF {numVars = v+ ,numClauses = c+ ,clauses = Set.fromList . map (map fromIntegral) $ is}+++-- import qualified Data.ByteString.Char8 as B++-- hStrictGetContents :: Handle -> IO String+-- hStrictGetContents h = do+-- bs <- B.hGetContents h+-- hClose h -- not sure if this is required; ByteString documentation isn't clear.+-- return $ B.unpack bs -- lazy unpack into String+++verifyBool :: IAssignment -> CNF -> Bool+verifyBool m problem = isNothing $ verify m problem+