Improve rule description
[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 = concatMap (\l -> [a, l])
115
116
117 parseConj :: BS.ByteString -> Conj
118 parseConj = atoms2Conj . filter (/=0) . map int . BS.words
119                     
120 parseCNF :: BS.ByteString -> CNF
121 parseCNF bs = 
122     V.fromList . map parseConj . dropWhile (\l -> BS.null l || BS.head l `elem` "cp") . BS.lines $
123     bs
124
125 runPicosat :: SATProb -> IO (Either (CNF) [Int])
126 runPicosat sp | isPMAXSAT sp = error "runPicosat cannot handle PMAXSAT problem"
127 runPicosat sp = do
128     let cnfString = formatCNF sp
129
130     (coreInFd, coreOutFd) <- createPipe
131     coreIn <- fdToHandle coreInFd
132
133     let picoProc = proc "picosat.trace" ["-c", "/proc/self/fd/" ++ show coreOutFd]
134
135     (Just hint, Just hout, _, procHandle) <- createProcess $ picoProc
136         { std_in = CreatePipe
137         , std_out = CreatePipe
138         }
139
140     closeFd coreOutFd
141     L.hPut hint cnfString
142     hClose hint
143     
144     result <- fix $ \next -> do
145         line <- hGetLine hout
146         if null line || head line == 'c' then next else return line
147     case result of
148         "s UNSATISFIABLE" -> do
149             hClose hout
150             musString <- BS.hGetContents coreIn
151             ensureSuccess [10,20] picoProc procHandle
152             let mus = parseCNF musString
153             --let annotatedMus = findConj mus cnf
154             return (Left mus)
155         "s SATISFIABLE" -> do
156             hClose coreIn
157             satvarsS <- BS.hGetContents hout
158             let ls = mapMaybe (\l ->
159                         if BS.null l then Nothing
160                         else if BS.head l == 'c' then Nothing
161                         else if BS.head l == 'v' then Just (BS.drop 2 l)
162                         else error $ "Cannot parse picosat SAT output: " ++ BS.unpack l
163                     ) $ BS.lines satvarsS
164             let vars = case concatMap BS.words ls of 
165                  ints@(_:_) | last ints == BS.pack "0" -> int <$> init ints
166                  _ -> error $ "Cannot parse picosat SAT output: " ++ BS.unpack satvarsS
167             ensureSuccess [10,20] picoProc procHandle
168             return (Right vars)
169         s -> do
170             error $ "Cannot parse picostat status output: " ++ s
171
172 {-
173 findConj :: CNF -> CNF -> CNF
174 findConj (mus,_) = first (V.filter (`S.member` set))
175   where set = S.fromList (V.toList mus)
176 -}
177
178 -- Takes a CNF and removes clauses until it becomes satisfiable.
179 -- The first argument gives the CNFs to relax
180 -- If successful, the first CNF returned contains the non-removed clauses,
181 -- while the second element in the tuple contains the removed clauses.
182 relaxer :: SATProb -> IO (Either CNF (CNF,CNF))
183 relaxer sp@(SATProb {..}) = do
184     ret <- runPMAXSolver sp
185     case ret of
186         Nothing -> do
187             ret <- runPicosat sp
188             case ret of
189                 Left mus -> do
190                     hPutStrLn stderr $ "Non-relaxable clauses are not satisfiable"
191                     return (Left mus)
192                 Right _ -> do
193                     error $ "The MAX-SAT solver found the problem to be unsatisfiable, " ++
194                             "yet the SAT solver found a solution. Possible bug in the solvers?"
195         Just vars -> do
196             let (satisfied, remove) = partitionSatClauses maxAtom desired vars
197             {- Code to check the PMAX-SAT solver if we do not trust it: 
198             let s = S.fromList remove
199             let (removed,leftOver) = partition (`S.member`s) relaxable
200
201             ret <- runPicosat (cnf ++ leftOver) 
202             case ret of 
203                 Left _ -> do
204                     hPutStrLn stderr $ "Relaxed CNF still unsatisfiable after removing " ++
205                         show (length removed) ++ " clauses, retrying..."
206                     fmap (removed ++) <$> relaxer leftOver cnf
207                 Right _ -> return (Right remove)
208             -}
209             return $ Right (satisfied,remove)
210
211
212 -- Takes a CNF and a list of desired atoms (positive or negative), and it finds
213 -- a solution that is set-inclusion maximal with regard to these atoms.
214 runPicosatPMAX :: [Int] -> SATProb -> IO (Either CNF [Int])
215 runPicosatPMAX _ sp | isPMAXSAT sp = error "runPicosatPMAX must not be passed a PMAXSAT instance"
216 runPicosatPMAX [] sp = runPicosat sp
217 runPicosatPMAX desiredAtoms sp = do
218     ret <- runPMAXSolver (sp { desired })
219     case ret of
220         Nothing -> do
221             ret <- runPicosat (sp { desired = V.empty })
222             case ret of
223                 Left mus ->
224                     return $ Left mus
225                 Right _ -> do
226                     error $ "The MAX-SAT solver found the problem to be unsatisfiable, " ++
227                             "yet the SAT solver found a problem. Possible bug in the solvers?"
228         Just solution -> return (Right solution)
229     where desired = V.fromList (map atom2Conj desiredAtoms)
230
231 -- Takes a CNF and a list of desired atoms (positive or negative), and it finds
232 -- a solution that is set-inclusion minimal with regard to these atoms, but
233 -- includes at least one.
234 runPicosatPMIN1 :: [Int] -> SATProb -> IO (Maybe [Int])
235 runPicosatPMIN1 _ sp | isPMAXSAT sp = error "runPicosatPMIN1 must not be passed a PMAXSAT instance"
236 runPicosatPMIN1 [] _ = error $ "Cannot call runPicosatPMIN1 with an empty set of desired clauses"
237 runPicosatPMIN1 desiredAtoms sp = runPMAXSolver (sp { desired })
238     where desired = V.fromList (disj : map atom2Conj desiredAtoms)
239           disj = atoms2Conj desiredAtoms
240
241 -- Takes a CNF and a list of desired atoms (positive or negative), and it finds
242 -- a set-inclusion minimal solutions that covers the set-inclusion maximal
243 -- solution, both are returned.
244 runPicosatPMINMAX :: [Int] -> SATProb -> IO (Either (CNF) ([Int],[[Int]]))
245 runPicosatPMINMAX _ sp | isPMAXSAT sp = error "runPicosatPMINMAX must not be passed a PMAXSAT instance"
246 runPicosatPMINMAX [] sp = do 
247     ret <- runPicosat sp
248     case ret of
249         Left mus -> return (Left mus)
250         Right solution -> return (Right (solution, [solution]))
251 runPicosatPMINMAX desired sp = do
252     ret <- if isJust sret
253            then runPMAXSolver (ssp { desired = V.fromList (map atom2Conj desired) })
254            else return Nothing
255     case ret of 
256         Nothing -> do
257             ret <- runPicosat sp
258             case ret of
259                 Left mus ->
260                     return $ Left mus
261                 Right _ -> do
262                     error $ "The MAX-SAT solver found the problem to be unsatisfiable, " ++
263                             "yet the SAT solver found a problem. Possible bug in the solvers?"
264         Just maxSol -> do
265             Right . (maxSol,) <$> step 0 (filter (`IS.member` desiredS) maxSol)
266   where sret@(~(Just ssp)) = simplifyCNF sp
267         desiredS    = IS.fromList desired
268         step 5 todo = do
269             hPutStrLn stderr $ show (length todo) ++ " clauses left, but stopping here nevertheless..."
270             return []
271         step n []   = return []
272         step n todo = do
273             hPutStrLn stderr $ show (length todo) ++ " clauses left while finding next small solution..."
274             aMinSol <- either (\_ -> error "Solvable problem turned unsolveable") id <$>
275                 runPicosatPMAX (map negate desired) (sp { required = atoms2Conj todo `V.cons` required sp })
276             let aMinSolS = IS.fromList aMinSol
277                 todo' = filter (`IS.notMember` aMinSolS) todo
278             when (length todo == length todo') $
279                 hPutStr stderr $ "Solution does not contain any variable."
280             (aMinSol :) <$> step (succ n) todo'
281
282 partitionSatClauses :: Int -> CNF -> [Int] -> (CNF,CNF)
283 partitionSatClauses maxVar conjs vars =  V.unstablePartition check conjs
284   where --array = listBitArray (1,maxVar) $ map (>0) vars
285         array = array' (1,maxVar) [ (i, True) | i <- vars, i > 0]
286         check = Z.any (\i -> (i > 0) == unsafeAt' array (abs (fromIntegral i)))
287
288
289 runPMAXSolver :: SATProb -> IO (Maybe [Int])
290 runPMAXSolver sp = do
291     -- hPrint stderr (length (fst cnf), length (fst desired), length (fst cnf'), length (fst desired'))
292     case simplifyCNF sp of
293         Just sp' -> fmap (applyMaskMB (knownAtoms sp')) <$> runSat4j sp'
294         Nothing -> return Nothing
295
296 runMSUnCore :: SATProb -> IO (Maybe [Int])
297 runMSUnCore = runAPMAXSolver $ \filename ->  proc "./solvers/msuncore-2011606-linux64" ["-v","0",filename]
298
299 runMiniMaxSat :: SATProb -> IO (Maybe [Int])
300 runMiniMaxSat = runAPMAXSolver $ \filename ->  proc "./minimaxsat" ["-F=2",filename]
301
302 runSat4j :: SATProb -> IO (Maybe [Int])
303 runSat4j = runAPMAXSolver $  \filename -> proc "java" ["-jar","solvers/sat4j-maxsat.jar",filename]
304
305 runClasp :: SATProb -> IO (Maybe [Int])
306 runClasp = runAPMAXSolver (\filename ->  proc "clasp" $ ["--quiet=1,2",filename])
307
308 runAPMAXSolver :: (FilePath -> CreateProcess) -> SATProb -> IO (Maybe [Int])
309 runAPMAXSolver cmd sp =
310     if isEmptyProblem sp then return (Just [1..maxAtom sp]) else do
311     getTemporaryDirectory  >>= \tmpdir -> do
312     withTempFile tmpdir "sat-britney-.wcnf" $ \tmpfile handle -> do
313     let cnfString = formatCNFPMAX sp
314
315     L.hPut handle cnfString
316     hClose handle
317
318     let proc = cmd tmpfile
319     (_, Just hout, _, procHandle) <- createProcess $ proc { std_out = CreatePipe }
320     
321     lines <- filter (not . BS.null) . BS.lines <$> BS.hGetContents hout
322     let (slines,(vlines,rest)) =
323             second (partition ((=='v') . BS.head)) .
324             partition ((=='s') . BS.head) $
325             lines
326     case slines of 
327         []      -> do
328             ensureSuccess [] proc procHandle
329             error $ "PMAX-SAT solver returned no \"s\"-line."
330         (_:_:_) -> do
331             error $ "PMAX-SAT solver returned more than one \"s\"-line." ++ 
332                     BS.unpack (BS.unlines slines)
333         [sline] | sline == "s UNSATISFIABLE" -> do
334             hClose hout
335             ensureSuccess [] proc procHandle
336             return Nothing
337                 | sline == "s OPTIMUM FOUND" -> do
338             let vars = case concatMap (BS.words . BS.drop 2) vlines of 
339                  ints@(_:_) -> filter (/= 0) . fmap int $ ints
340                  _ -> error $ "Cannot parse pmaxsatsolver assignment output: " ++
341                               BS.unpack (BS.unlines slines)
342             ensureSuccess [] proc procHandle
343             return (Just vars)
344                 | otherwise -> do
345             error $ "Cannot parse pmaxsatsolver status output: " ++ BS.unpack sline
346   
347 ensureSuccess alsoOk proc procHandle = do
348     ec <- waitForProcess procHandle
349     case ec of
350         ExitSuccess -> return ()
351         ExitFailure c | c `elem` alsoOk -> return ()
352         ExitFailure c -> error $ "Command \"" ++ showCmdSpec (cmdspec proc) ++
353          
354             "\" failed with error code " ++ show c
355
356 showCmdSpec (ShellCommand cmd) = cmd
357 showCmdSpec (RawCommand cmd args) = concat $ intersperse " " (cmd:args)
358
359 -- | This takes hard and soft clauses and propagats constants (e.g. variables
360 -- fixed by a top level clause), removing variables from clauses or clauses
361 -- that are known.
362 {-
363 simplifyCNF' :: CNF -> CNF -> Maybe (CNF, CNF, AssignmentMask)
364 --simplifyCNF (hard,maxVar) (soft,_)  = Just ((hard,maxVar), (soft,maxVar), emptyMask)
365 --  where emptyMask = array' (-maxVar, maxVar) []
366 simplifyCNF' (hard,maxVar) (soft,_)  = go [emptyMask] (hard,maxVar) (soft,maxVar)
367   where go ms (hard,maxVar) (soft,_) = if null singletons
368             then if isValidMask finalMask
369                  then Just ((hard,maxVar), (soft,maxVar), finalMask)
370                  else Nothing
371             else if V.any (U.null) hard'
372                  then Nothing
373                  else go (knownAtomsA:ms) (hard',maxVar) (soft',maxVar)
374           where 
375             singletons = {-# SCC "singletons" #-} V.toList $ V.filter (\c -> U.length c == 1) hard
376             others = hard
377             knownAtomsA = {-# SCC "knownAtomsA" #-}
378                 array' (-maxVar, maxVar)
379                          [ (fromIntegral i, True) | (U.toList -> [i]) <- singletons] 
380             knownTrue i = {-# SCC "knownTrue" #-}
381                 unsafeAt' knownAtomsA (fromIntegral i)
382             surelyTrueConjs = {-# SCC "surelyTrueConjs" #-}
383                 U.any knownTrue
384             knownFalse i = {-# SCC "knownFalse" #-}
385                 unsafeAt' knownAtomsA (fromIntegral (-i))
386             hard' = {-# SCC "hard'" #-}
387                 V.map (U.filter (not . knownFalse)) .
388                 V.filter (not . surelyTrueConjs) $ others 
389             soft' = {-# SCC "soft'" #-}
390                 V.filter (not . U.null) .
391                 V.map (U.filter (not . knownFalse)) .
392                 V.filter (not . surelyTrueConjs) $ soft 
393             finalMask = unionsMask ms
394         emptyMask = array' (-maxVar, maxVar) [] :: AssignmentMask
395 -}
396
397 simplifyCNF :: SATProb -> Maybe SATProb
398 simplifyCNF (SATProb {..}) = 
399     let finalMask = runSTUArray $ do
400             mask <- case knownAtoms of
401                 Just originalMask -> thaw originalMask
402                 Nothing -> newArray (-maxAtom,maxAtom) False
403             fix $ \repeat -> do
404                 currentMask <- freeze mask
405                 let knownFalse i = unsafeAt' currentMask (fromIntegral (-i))
406                     knownTrue i = unsafeAt' currentMask (fromIntegral i)
407                     newSingletons = 
408                         mapMaybe (\c ->
409                             case filter (not . knownFalse) $ Z.toList c of
410                                 [x] | not (knownTrue x) -> Just x
411                                 _   -> Nothing
412                         ) $
413                         V.toList required
414                 if null newSingletons
415                 then return ()
416                 else do
417                     forM_ newSingletons $ \c -> writeArray mask (fromIntegral c) True
418                     repeat
419             return mask
420         knownFalse i = unsafeAt' finalMask (fromIntegral (-i))
421         knownTrue i = unsafeAt' finalMask (fromIntegral i)
422         surelyTrueConjs =
423             Z.any knownTrue
424         required' =
425             V.map (Z.filter (not . knownFalse)) .
426             V.filter (not . surelyTrueConjs) $ required 
427         desired' = 
428             V.filter (not . Z.null) .
429             V.map (Z.filter (not . knownFalse)) .
430             V.filter (not . surelyTrueConjs) $ desired 
431     in  if isValidMask finalMask
432         then Just (SATProb maxAtom required' desired' (Just finalMask))
433         else Nothing
434
435
436 array' :: (Int, Int) -> [(Int, Bool)] -> AssignmentMask
437 array' (l,u) assoc = runSTUArray $ do
438     arr <- newArray (l,u) False
439     mapM_ (uncurry (writeArray arr)) assoc
440     return arr
441
442 unsafeAt' :: AssignmentMask -> Int -> Bool
443 unsafeAt' arr i = unsafeAt arr $ index (bounds arr) i
444 {-# INLINE unsafeAt' #-}
445
446 partitionEithersV :: V.Vector (Either a b) -> (V.Vector a, V.Vector b)
447 partitionEithersV = 
448   (V.map (either id undefined) *** V.map (either undefined id)) . V.unstablePartition (either (const True) (const False))
449
450 isValidMask mask = not $ any (\i -> unsafeAt' mask i && unsafeAt' mask (-i) ) [1..u]
451   where (l,u) = bounds mask
452
453 applyMask :: AssignmentMask -> [Int] -> [Int]
454 applyMask mask = map fixAtom 
455   where fixAtom i | unsafeAt' mask i    = i
456                   | unsafeAt' mask (-i) = -i
457                   | otherwise           = i
458
459 applyMaskMB :: Maybe AssignmentMask -> [Int] -> [Int]
460 applyMaskMB  = maybe id applyMask
461
462 unionsMask [] = error "Cannot union empty set of masks"
463 unionsMask ms@(m1:_) =  array' (l,u) [ (i, True) | i <- [l..u] , any (`unsafeAt'` i) ms ]
464   where (l,u) = bounds m1
465
466 invalidExtra = error "PicoSat.hs: Internally created CNF clause leaked to caller"