66872f6bbae5c3e7a8a06e747d214c97bb2022b2
[sat-britney.git] / Picosat.hs
1 {-# LANGUAGE OverloadedStrings, TupleSections, ViewPatterns, DoAndIfThenElse, RecordWildCards, NamedFieldPuns #-}
2 -- |
3 -- Module: Picosat
4 -- Copyright: (c) 2011 Joachim Breitner
5 -- License: GPL-2
6 --
7 module Picosat
8     ( Conj
9     , CNF
10     , SATProb(..)
11     , relaxer 
12     , conjs2SATProb
13     , conjs2PMAXSATProb
14     , atom2Conj
15     , atoms2Conj
16     , combineCNF
17     , formatCNF
18     , runPicosatPMAX
19     , runPicosatPMINMAX
20     )
21     where
22
23 import qualified Data.ByteString.Lazy.Char8 as L
24 import qualified Data.ByteString.Char8 as BS
25 import Data.ByteString.Nums.Careless
26
27 import System.IO
28 import System.Posix.IO
29 import System.Process
30 import System.Exit
31 import Data.Functor
32 import Data.List
33 import Data.Maybe
34 import Data.Function
35 import Data.Either
36 import Data.Int
37 import System.Directory
38 import Distribution.Simple.Utils (withTempFile)
39 import Control.Arrow 
40 import Control.Monad
41 import Data.BitArray
42 import Data.Array.Base (unsafeAt)
43 import Data.Array.Unboxed
44 import Data.Array.ST
45 import qualified Data.Array.MArray as MArray
46 import qualified Data.Vector as V
47 import qualified Data.Vector.Unboxed as U
48 import qualified ZArray as Z
49
50 import qualified Data.IntSet as IS
51 import qualified Data.Set as S
52
53 -- Remember largest variable
54 type CNF = V.Vector Conj
55 -- Conj is guaranteed to be ordered by absolute value
56 type Conj = Z.Array
57
58 -- Known to have rage (-maxVar,maxVar)
59 type AssignmentMask = UArray Int Bool
60
61 data SATProb = SATProb {
62     maxAtom :: Int
63     , required :: CNF
64     , desired :: CNF
65     , knownAtoms :: Maybe AssignmentMask
66     }
67
68 combineCNF :: CNF -> CNF -> CNF
69 combineCNF conj1 conj2 = conj1 V.++ conj2
70 {-# INLINE combineCNF #-}
71
72 atoms2Conj :: [Int] -> Conj
73 atoms2Conj = Z.fromList . map fromIntegral
74
75 conj2Line :: Conj -> BS.ByteString
76 conj2Line ls = BS.pack $ unwords (map show (Z.toList ls)) ++ " 0\n"
77
78 conjs2SATProb :: Int -> V.Vector Conj -> SATProb
79 conjs2SATProb m conjs = m `seq` SATProb m conjs V.empty Nothing
80
81 conjs2PMAXSATProb :: Int -> V.Vector Conj -> V.Vector Conj -> SATProb
82 conjs2PMAXSATProb m required desired = m `seq` SATProb m required desired Nothing
83
84 atom2Conj :: Int -> Conj
85 {-# INLINE atom2Conj #-}
86 atom2Conj i = Z.singleton (fromIntegral i)
87
88 atom2Conj' = atom2Conj invalidExtra
89
90 isPMAXSAT (SATProb {..}) = not (V.null desired)
91 isEmptyProblem (SATProb {..}) = V.null required && V.null desired
92
93 formatCNF :: SATProb -> L.ByteString
94 formatCNF sp | isPMAXSAT sp = error "formatCNF cannot format PMAXSAT problem"
95 formatCNF (SATProb {..}) = L.concat
96     [ L.pack "c LitSat CNF generator\n"
97     , L.pack $ unwords ["p", "cnf", show maxAtom, show (V.length required)] ++ "\n"
98     , L.fromChunks $ map conj2Line $ V.toList required
99     ]
100
101 formatCNFPMAX :: SATProb -> L.ByteString
102 formatCNFPMAX (SATProb {..}) = L.concat $
103     [ L.pack "c LitSat CNF generator\n"
104     , L.pack $ unwords
105         ["p", "wcnf", show maxAtom, show (numClauses + numRelaxable), topN ] ++ "\n"
106     , L.fromChunks $ prependEach top  $ map conj2Line $ V.toList required
107     , L.fromChunks $ prependEach soft $ map conj2Line $ V.toList desired
108     ]
109   where numClauses = V.length required
110         numRelaxable = V.length desired
111         topN = show (numRelaxable + 2)
112         top = BS.pack (topN ++ " ")
113         soft = BS.pack ("1 ")
114         prependEach a [] = []
115         prependEach a l = (a:) . intersperse a $ l
116
117
118 parseConj :: BS.ByteString -> Conj
119 parseConj = atoms2Conj . filter (/=0) . map int . BS.words
120                     
121 parseCNF :: BS.ByteString -> CNF
122 parseCNF bs = 
123     V.fromList . map parseConj . dropWhile (\l -> BS.null l || BS.head l `elem` "cp") . BS.lines $
124     bs
125
126 runPicosat :: SATProb -> IO (Either (CNF) [Int])
127 runPicosat sp | isPMAXSAT sp = error "runPicosat cannot handle PMAXSAT problem"
128 runPicosat sp = do
129     let cnfString = formatCNF sp
130
131     (coreInFd, coreOutFd) <- createPipe
132     coreIn <- fdToHandle coreInFd
133
134     let picoProc = proc "picosat.trace" ["-c", "/proc/self/fd/" ++ show coreOutFd]
135
136     (Just hint, Just hout, _, procHandle) <- createProcess $ picoProc
137         { std_in = CreatePipe
138         , std_out = CreatePipe
139         }
140
141     closeFd coreOutFd
142     L.hPut hint cnfString
143     hClose hint
144     
145     result <- fix $ \next -> do
146         line <- hGetLine hout
147         if null line || head line == 'c' then next else return line
148     case result of
149         "s UNSATISFIABLE" -> do
150             hClose hout
151             musString <- BS.hGetContents coreIn
152             ensureSuccess [10,20] picoProc procHandle
153             let mus = parseCNF musString
154             --let annotatedMus = findConj mus cnf
155             return (Left mus)
156         "s SATISFIABLE" -> do
157             hClose coreIn
158             satvarsS <- BS.hGetContents hout
159             let ls = mapMaybe (\l ->
160                         if BS.null l then Nothing
161                         else if BS.head l == 'c' then Nothing
162                         else if BS.head l == 'v' then Just (BS.drop 2 l)
163                         else error $ "Cannot parse picosat SAT output: " ++ BS.unpack l
164                     ) $ BS.lines satvarsS
165             let vars = case concatMap BS.words ls of 
166                  ints@(_:_) | last ints == BS.pack "0" -> int <$> init ints
167                  _ -> error $ "Cannot parse picosat SAT output: " ++ BS.unpack satvarsS
168             ensureSuccess [10,20] picoProc procHandle
169             return (Right vars)
170         s -> do
171             error $ "Cannot parse picostat status output: " ++ s
172
173 {-
174 findConj :: CNF -> CNF -> CNF
175 findConj (mus,_) = first (V.filter (`S.member` set))
176   where set = S.fromList (V.toList mus)
177 -}
178
179 -- Takes a CNF and removes clauses until it becomes satisfiable.
180 -- The first argument gives the CNFs to relax
181 -- If successful, the first CNF returned contains the non-removed clauses,
182 -- while the second element in the tuple contains the removed clauses.
183 relaxer :: SATProb -> IO (Either CNF (CNF,CNF))
184 relaxer sp@(SATProb {..}) = do
185     ret <- runPMAXSolver sp
186     case ret of
187         Nothing -> do
188             ret <- runPicosat sp
189             case ret of
190                 Left mus -> do
191                     hPutStrLn stderr $ "Non-relaxable clauses are not satisfiable"
192                     return (Left mus)
193                 Right _ -> do
194                     error $ "The MAX-SAT solver found the problem to be unsatisfiable, " ++
195                             "yet the SAT solver found a solution. Possible bug in the solvers?"
196         Just vars -> do
197             let (satisfied, remove) = partitionSatClauses maxAtom desired vars
198             {- Code to check the PMAX-SAT solver if we do not trust it: 
199             let s = S.fromList remove
200             let (removed,leftOver) = partition (`S.member`s) relaxable
201
202             ret <- runPicosat (cnf ++ leftOver) 
203             case ret of 
204                 Left _ -> do
205                     hPutStrLn stderr $ "Relaxed CNF still unsatisfiable after removing " ++
206                         show (length removed) ++ " clauses, retrying..."
207                     fmap (removed ++) <$> relaxer leftOver cnf
208                 Right _ -> return (Right remove)
209             -}
210             return $ Right (satisfied,remove)
211
212
213 -- Takes a CNF and a list of desired atoms (positive or negative), and it finds
214 -- a solution that is set-inclusion maximal with regard to these atoms.
215 runPicosatPMAX :: [Int] -> SATProb -> IO (Either CNF [Int])
216 runPicosatPMAX _ sp | isPMAXSAT sp = error "runPicosatPMAX must not be passed a PMAXSAT instance"
217 runPicosatPMAX [] sp = runPicosat sp
218 runPicosatPMAX desiredAtoms sp = do
219     ret <- runPMAXSolver (sp { desired })
220     case ret of
221         Nothing -> do
222             ret <- runPicosat (sp { desired = V.empty })
223             case ret of
224                 Left mus ->
225                     return $ Left mus
226                 Right _ -> do
227                     error $ "The MAX-SAT solver found the problem to be unsatisfiable, " ++
228                             "yet the SAT solver found a problem. Possible bug in the solvers?"
229         Just solution -> return (Right solution)
230     where desired = V.fromList (map atom2Conj desiredAtoms)
231
232 -- Takes a CNF and a list of desired atoms (positive or negative), and it finds
233 -- a solution that is set-inclusion minimal with regard to these atoms, but
234 -- includes at least one.
235 runPicosatPMIN1 :: [Int] -> SATProb -> IO (Maybe [Int])
236 runPicosatPMIN1 _ sp | isPMAXSAT sp = error "runPicosatPMIN1 must not be passed a PMAXSAT instance"
237 runPicosatPMIN1 [] _ = error $ "Cannot call runPicosatPMIN1 with an empty set of desired clauses"
238 runPicosatPMIN1 desiredAtoms sp = runPMAXSolver (sp { desired })
239     where desired = V.fromList (disj : map atom2Conj desiredAtoms)
240           disj = atoms2Conj desiredAtoms
241
242 -- Takes a CNF and a list of desired atoms (positive or negative), and it finds
243 -- a set-inclusion minimal solutions that covers the set-inclusion maximal
244 -- solution, both are returned.
245 runPicosatPMINMAX :: [Int] -> SATProb -> IO (Either (CNF) ([Int],[[Int]]))
246 runPicosatPMINMAX _ sp | isPMAXSAT sp = error "runPicosatPMINMAX must not be passed a PMAXSAT instance"
247 runPicosatPMINMAX [] sp = do 
248     ret <- runPicosat sp
249     case ret of
250         Left mus -> return (Left mus)
251         Right solution -> return (Right (solution, [solution]))
252 runPicosatPMINMAX desired sp = do
253     ret <- if isJust sret
254            then runPMAXSolver (ssp { desired = V.fromList (map atom2Conj desired) })
255            else return Nothing
256     case ret of 
257         Nothing -> do
258             ret <- runPicosat sp
259             case ret of
260                 Left mus ->
261                     return $ Left mus
262                 Right _ -> do
263                     error $ "The MAX-SAT solver found the problem to be unsatisfiable, " ++
264                             "yet the SAT solver found a problem. Possible bug in the solvers?"
265         Just maxSol -> do
266             Right . (maxSol,) <$> step 0 (filter (`IS.member` desiredS) maxSol)
267   where sret@(~(Just ssp)) = simplifyCNF sp
268         desiredS    = IS.fromList desired
269         step 5 todo = do
270             hPutStrLn stderr $ show (length todo) ++ " clauses left, but stopping here nevertheless..."
271             return []
272         step n []   = return []
273         step n todo = do
274             hPutStrLn stderr $ show (length todo) ++ " clauses left while finding next small solution..."
275             aMinSol <- either (\_ -> error "Solvable problem turned unsolveable") id <$>
276                 runPicosatPMAX (map negate desired) (sp { required = atoms2Conj todo `V.cons` required sp })
277             let aMinSolS = IS.fromList aMinSol
278                 todo' = filter (`IS.notMember` aMinSolS) todo
279             when (length todo == length todo') $
280                 hPutStr stderr $ "Solution does not contain any variable."
281             (aMinSol :) <$> step (succ n) todo'
282
283 partitionSatClauses :: Int -> CNF -> [Int] -> (CNF,CNF)
284 partitionSatClauses maxVar conjs vars =  V.unstablePartition check conjs
285   where --array = listBitArray (1,maxVar) $ map (>0) vars
286         array = array' (1,maxVar) [ (i, True) | i <- vars, i > 0]
287         check = Z.any (\i -> (i > 0) == unsafeAt' array (abs (fromIntegral i)))
288
289
290 runPMAXSolver :: SATProb -> IO (Maybe [Int])
291 runPMAXSolver sp = do
292     -- hPrint stderr (length (fst cnf), length (fst desired), length (fst cnf'), length (fst desired'))
293     case simplifyCNF sp of
294         Just sp' -> fmap (applyMaskMB (knownAtoms sp')) <$> runSat4j sp'
295         Nothing -> return Nothing
296
297 runMSUnCore :: SATProb -> IO (Maybe [Int])
298 runMSUnCore = runAPMAXSolver $ \filename ->  proc "./msuncore" ["-v","0",filename]
299
300 runMiniMaxSat :: SATProb -> IO (Maybe [Int])
301 runMiniMaxSat = runAPMAXSolver $ \filename ->  proc "./minimaxsat" ["-F=2",filename]
302
303 runSat4j :: SATProb -> IO (Maybe [Int])
304 runSat4j = runAPMAXSolver $  \filename -> proc "java" ["-jar","solvers/sat4j-maxsat.jar",filename]
305
306 runClasp :: SATProb -> IO (Maybe [Int])
307 runClasp = runAPMAXSolver (\filename ->  proc "clasp" $ ["--quiet=1,2",filename])
308
309 runAPMAXSolver :: (FilePath -> CreateProcess) -> SATProb -> IO (Maybe [Int])
310 runAPMAXSolver cmd sp =
311     if isEmptyProblem sp then return (Just [1..maxAtom sp]) else do
312     getTemporaryDirectory  >>= \tmpdir -> do
313     withTempFile tmpdir "sat-britney-.wcnf" $ \tmpfile handle -> do
314     let cnfString = formatCNFPMAX sp
315
316     L.hPut handle cnfString
317     hClose handle
318
319     let proc = cmd tmpfile
320     (_, Just hout, _, procHandle) <- createProcess $ proc { std_out = CreatePipe }
321     
322     lines <- filter (not . BS.null) . BS.lines <$> BS.hGetContents hout
323     let (slines,(vlines,rest)) =
324             second (partition ((=='v') . BS.head)) .
325             partition ((=='s') . BS.head) $
326             lines
327     case slines of 
328         []      -> do
329             ensureSuccess [] proc procHandle
330             error $ "PMAX-SAT solver returned no \"s\"-line."
331         (_:_:_) -> do
332             error $ "PMAX-SAT solver returned more than one \"s\"-line." ++ 
333                     BS.unpack (BS.unlines slines)
334         [sline] | sline == "s UNSATISFIABLE" -> do
335             hClose hout
336             ensureSuccess [] proc procHandle
337             return Nothing
338                 | sline == "s OPTIMUM FOUND" -> do
339             let vars = case concatMap (BS.words . BS.drop 2) vlines of 
340                  ints@(_:_) -> filter (/= 0) . fmap int $ ints
341                  _ -> error $ "Cannot parse pmaxsatsolver assignment output: " ++
342                               BS.unpack (BS.unlines slines)
343             ensureSuccess [] proc procHandle
344             return (Just vars)
345                 | otherwise -> do
346             error $ "Cannot parse pmaxsatsolver status output: " ++ BS.unpack sline
347   
348 ensureSuccess alsoOk proc procHandle = do
349     ec <- waitForProcess procHandle
350     case ec of
351         ExitSuccess -> return ()
352         ExitFailure c | c `elem` alsoOk -> return ()
353         ExitFailure c -> error $ "Command \"" ++ showCmdSpec (cmdspec proc) ++
354          
355             "\" failed with error code " ++ show c
356
357 showCmdSpec (ShellCommand cmd) = cmd
358 showCmdSpec (RawCommand cmd args) = concat $ intersperse " " (cmd:args)
359
360 -- | This takes hard and soft clauses and propagats constants (e.g. variables
361 -- fixed by a top level clause), removing variables from clauses or clauses
362 -- that are known.
363 {-
364 simplifyCNF' :: CNF -> CNF -> Maybe (CNF, CNF, AssignmentMask)
365 --simplifyCNF (hard,maxVar) (soft,_)  = Just ((hard,maxVar), (soft,maxVar), emptyMask)
366 --  where emptyMask = array' (-maxVar, maxVar) []
367 simplifyCNF' (hard,maxVar) (soft,_)  = go [emptyMask] (hard,maxVar) (soft,maxVar)
368   where go ms (hard,maxVar) (soft,_) = if null singletons
369             then if isValidMask finalMask
370                  then Just ((hard,maxVar), (soft,maxVar), finalMask)
371                  else Nothing
372             else if V.any (U.null) hard'
373                  then Nothing
374                  else go (knownAtomsA:ms) (hard',maxVar) (soft',maxVar)
375           where 
376             singletons = {-# SCC "singletons" #-} V.toList $ V.filter (\c -> U.length c == 1) hard
377             others = hard
378             knownAtomsA = {-# SCC "knownAtomsA" #-}
379                 array' (-maxVar, maxVar)
380                          [ (fromIntegral i, True) | (U.toList -> [i]) <- singletons] 
381             knownTrue i = {-# SCC "knownTrue" #-}
382                 unsafeAt' knownAtomsA (fromIntegral i)
383             surelyTrueConjs = {-# SCC "surelyTrueConjs" #-}
384                 U.any knownTrue
385             knownFalse i = {-# SCC "knownFalse" #-}
386                 unsafeAt' knownAtomsA (fromIntegral (-i))
387             hard' = {-# SCC "hard'" #-}
388                 V.map (U.filter (not . knownFalse)) .
389                 V.filter (not . surelyTrueConjs) $ others 
390             soft' = {-# SCC "soft'" #-}
391                 V.filter (not . U.null) .
392                 V.map (U.filter (not . knownFalse)) .
393                 V.filter (not . surelyTrueConjs) $ soft 
394             finalMask = unionsMask ms
395         emptyMask = array' (-maxVar, maxVar) [] :: AssignmentMask
396 -}
397
398 simplifyCNF :: SATProb -> Maybe SATProb
399 simplifyCNF (SATProb {..}) = 
400     let finalMask = runSTUArray $ do
401             mask <- case knownAtoms of
402                 Just originalMask -> thaw originalMask
403                 Nothing -> newArray (-maxAtom,maxAtom) False
404             fix $ \repeat -> do
405                 currentMask <- freeze mask
406                 let knownFalse i = unsafeAt' currentMask (fromIntegral (-i))
407                     knownTrue i = unsafeAt' currentMask (fromIntegral i)
408                     newSingletons = 
409                         mapMaybe (\c ->
410                             case filter (not . knownFalse) $ Z.toList c of
411                                 [x] | not (knownTrue x) -> Just x
412                                 _   -> Nothing
413                         ) $
414                         V.toList required
415                 if null newSingletons
416                 then return ()
417                 else do
418                     forM_ newSingletons $ \c -> writeArray mask (fromIntegral c) True
419                     repeat
420             return mask
421         knownFalse i = unsafeAt' finalMask (fromIntegral (-i))
422         knownTrue i = unsafeAt' finalMask (fromIntegral i)
423         surelyTrueConjs =
424             Z.any knownTrue
425         required' =
426             V.map (Z.filter (not . knownFalse)) .
427             V.filter (not . surelyTrueConjs) $ required 
428         desired' = 
429             V.filter (not . Z.null) .
430             V.map (Z.filter (not . knownFalse)) .
431             V.filter (not . surelyTrueConjs) $ desired 
432     in  if isValidMask finalMask
433         then Just (SATProb maxAtom required' desired' (Just finalMask))
434         else Nothing
435
436
437 array' :: (Int, Int) -> [(Int, Bool)] -> AssignmentMask
438 array' (l,u) assoc = runSTUArray $ do
439     arr <- newArray (l,u) False
440     mapM_ (uncurry (writeArray arr)) assoc
441     return arr
442
443 unsafeAt' :: AssignmentMask -> Int -> Bool
444 unsafeAt' arr i = unsafeAt arr $ index (bounds arr) i
445 {-# INLINE unsafeAt' #-}
446
447 partitionEithersV :: V.Vector (Either a b) -> (V.Vector a, V.Vector b)
448 partitionEithersV = 
449   (V.map (either id undefined) *** V.map (either undefined id)) . V.unstablePartition (either (const True) (const False))
450
451 isValidMask mask = not $ any (\i -> unsafeAt' mask i && unsafeAt' mask (-i) ) [1..u]
452   where (l,u) = bounds mask
453
454 applyMask :: AssignmentMask -> [Int] -> [Int]
455 applyMask mask = map fixAtom 
456   where fixAtom i | unsafeAt' mask i    = i
457                   | unsafeAt' mask (-i) = -i
458                   | otherwise           = i
459
460 applyMaskMB :: Maybe AssignmentMask -> [Int] -> [Int]
461 applyMaskMB  = maybe id applyMask
462
463 unionsMask [] = error "Cannot union empty set of masks"
464 unionsMask ms@(m1:_) =  array' (l,u) [ (i, True) | i <- [l..u] , any (`unsafeAt'` i) ms ]
465   where (l,u) = bounds m1
466
467 invalidExtra = error "PicoSat.hs: Internally created CNF clause leaked to caller"