diff --git a/Control/Monad/MonadST.hs b/Control/Monad/MonadST.hs new file mode 100644 --- /dev/null +++ b/Control/Monad/MonadST.hs @@ -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 . + + Copyright 2008 Denis Bueno +-} + + +-- | Idea from +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) + diff --git a/DPLL/Monad.hs b/DPLL/Monad.hs new file mode 100644 --- /dev/null +++ b/DPLL/Monad.hs @@ -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 +-- . +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') diff --git a/Funsat/FastDom.hs b/Funsat/FastDom.hs new file mode 100644 --- /dev/null +++ b/Funsat/FastDom.hs @@ -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 +-- +-- 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 +-} + diff --git a/Funsat/Solver.hs b/Funsat/Solver.hs new file mode 100644 --- /dev/null +++ b/Funsat/Solver.hs @@ -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 . + + 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 "" +instance Show (STUArray s Var Int) where + show = const "" +instance Show (STUArray s Var Double) where + show = const "" +instance Show (STArray s a b) where + show = const "" + +-- | 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 diff --git a/Funsat/Utils.hs b/Funsat/Utils.hs new file mode 100644 --- /dev/null +++ b/Funsat/Utils.hs @@ -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 . + + 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 + diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,165 @@ + GNU LESSER GENERAL PUBLIC LICENSE + Version 3, 29 June 2007 + + Copyright (C) 2007 Free Software Foundation, Inc. + 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. diff --git a/Main.hs b/Main.hs new file mode 100644 --- /dev/null +++ b/Main.hs @@ -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 . + + 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] ... " + +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 } + diff --git a/README b/README new file mode 100644 --- /dev/null +++ b/README @@ -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 + diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/Text/Tabular.hs b/Text/Tabular.hs new file mode 100644 --- /dev/null +++ b/Text/Tabular.hs @@ -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 . + + 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) + + diff --git a/funsat.cabal b/funsat.cabal new file mode 100644 --- /dev/null +++ b/funsat.cabal @@ -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 +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 diff --git a/tests/Properties.hs b/tests/Properties.hs new file mode 100644 --- /dev/null +++ b/tests/Properties.hs @@ -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 . + + 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 "" + + + + +-- * 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 +