{-# OPTIONS_GHC -Wall #-} {-# LANGUAGE CPP #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TemplateHaskell #-} module Test.SAT.MUS (satMUSTestGroup) where import Control.Monad import Data.Default.Class import qualified Data.Set as Set import qualified Data.IntSet as IntSet import Test.Tasty import Test.Tasty.HUnit import Test.Tasty.TH import qualified ToySolver.SAT as SAT import qualified ToySolver.SAT.MUS as MUS import qualified ToySolver.SAT.MUS.Enum as MUSEnum ------------------------------------------------------------------------ findMUSAssumptions_case1 :: MUS.Method -> IO () findMUSAssumptions_case1 method = do solver <- SAT.newSolver [x1,x2,x3] <- SAT.newVars solver 3 sels@[y1,y2,y3,y4,y5,y6] <- SAT.newVars solver 6 SAT.addClause solver [-y1, x1] SAT.addClause solver [-y2, -x1] SAT.addClause solver [-y3, -x1, x2] SAT.addClause solver [-y4, -x2] SAT.addClause solver [-y5, -x1, x3] SAT.addClause solver [-y6, -x3] ret <- SAT.solveWith solver sels ret @?= False actual <- MUS.findMUSAssumptions solver def{ MUS.optMethod = method } let actual' = IntSet.map (\x -> x-3) actual expected = map IntSet.fromList [[1, 2], [1, 3, 4], [1, 5, 6]] actual' `elem` expected @?= True case_findMUSAssumptions_Deletion :: Assertion case_findMUSAssumptions_Deletion = findMUSAssumptions_case1 MUS.Deletion case_findMUSAssumptions_Insertion :: Assertion case_findMUSAssumptions_Insertion = findMUSAssumptions_case1 MUS.Insertion case_findMUSAssumptions_QuickXplain :: Assertion case_findMUSAssumptions_QuickXplain = findMUSAssumptions_case1 MUS.QuickXplain ------------------------------------------------------------------------ {- c http://sun.iwu.edu/~mliffito/publications/jar_liffiton_CAMUS.pdf c φ= (x1) ∧ (¬x1) ∧ (¬x1∨x2) ∧ (¬x2) ∧ (¬x1∨x3) ∧ (¬x3) c MUSes(φ) = {{C1, C2}, {C1, C3, C4}, {C1, C5, C6}} c MCSes(φ) = {{C1}, {C2, C3, C5}, {C2, C3, C6}, {C2, C4, C5}, {C2, C4, C6}} p cnf 3 6 1 0 -1 0 -1 2 0 -2 0 -1 3 0 -3 0 -} allMUSAssumptions_case1 :: MUSEnum.Method -> IO () allMUSAssumptions_case1 method = do solver <- SAT.newSolver [x1,x2,x3] <- SAT.newVars solver 3 sels@[y1,y2,y3,y4,y5,y6] <- SAT.newVars solver 6 SAT.addClause solver [-y1, x1] SAT.addClause solver [-y2, -x1] SAT.addClause solver [-y3, -x1, x2] SAT.addClause solver [-y4, -x2] SAT.addClause solver [-y5, -x1, x3] SAT.addClause solver [-y6, -x3] (muses, mcses) <- MUSEnum.allMUSAssumptions solver sels def{ MUSEnum.optMethod = method } Set.fromList muses @?= Set.fromList (map (IntSet.fromList . map (+3)) [[1,2], [1,3,4], [1,5,6]]) Set.fromList mcses @?= Set.fromList (map (IntSet.fromList . map (+3)) [[1], [2,3,5], [2,3,6], [2,4,5], [2,4,6]]) case_allMUSAssumptions_CAMUS :: Assertion case_allMUSAssumptions_CAMUS = allMUSAssumptions_case1 MUSEnum.CAMUS case_allMUSAssumptions_DAA :: Assertion case_allMUSAssumptions_DAA = allMUSAssumptions_case1 MUSEnum.DAA case_allMUSAssumptions_MARCO :: Assertion case_allMUSAssumptions_MARCO = allMUSAssumptions_case1 MUSEnum.MARCO case_allMUSAssumptions_GurvichKhachiyan1999 :: Assertion case_allMUSAssumptions_GurvichKhachiyan1999 = allMUSAssumptions_case1 MUSEnum.GurvichKhachiyan1999 {- Boosting a Complete Technique to Find MSS and MUS thanks to a Local Search Oracle http://www.cril.univ-artois.fr/~piette/IJCAI07_HYCAM.pdf Example 3. C0 : (d) C1 : (b ∨ c) C2 : (a ∨ b) C3 : (a ∨ ¬c) C4 : (¬b ∨ ¬e) C5 : (¬a ∨ ¬b) C6 : (a ∨ e) C7 : (¬a ∨ ¬e) C8 : (b ∨ e) C9 : (¬a ∨ b ∨ ¬c) C10 : (¬a ∨ b ∨ ¬d) C11 : (a ∨ ¬b ∨ c) C12 : (a ∨ ¬b ∨ ¬d) -} allMUSAssumptions_case2 :: MUSEnum.Method -> IO () allMUSAssumptions_case2 method = do solver <- SAT.newSolver [a,b,c,d,e] <- SAT.newVars solver 5 sels@[y0,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12] <- SAT.newVars solver 13 SAT.addClause solver [-y0, d] SAT.addClause solver [-y1, b, c] SAT.addClause solver [-y2, a, b] SAT.addClause solver [-y3, a, -c] SAT.addClause solver [-y4, -b, -e] SAT.addClause solver [-y5, -a, -b] SAT.addClause solver [-y6, a, e] SAT.addClause solver [-y7, -a, -e] SAT.addClause solver [-y8, b, e] SAT.addClause solver [-y9, -a, b, -c] SAT.addClause solver [-y10, -a, b, -d] SAT.addClause solver [-y11, a, -b, c] SAT.addClause solver [-y12, a, -b, -d] -- Only three of the MUSes (marked with asterisks) are on the paper. let cores = [ [y0,y1,y2,y5,y9,y12] , [y0,y1,y3,y4,y5,y6,y10] , [y0,y1,y3,y5,y7,y8,y12] , [y0,y1,y3,y5,y9,y12] , [y0,y1,y3,y5,y10,y11] , [y0,y1,y3,y5,y10,y12] , [y0,y2,y3,y5,y10,y11] , [y0,y2,y4,y5,y6,y10] , [y0,y2,y5,y7,y8,y12] , [y0,y2,y5,y10,y12] -- (*) , [y1,y2,y4,y5,y6,y9] , [y1,y3,y4,y5,y6,y7,y8] , [y1,y3,y4,y5,y6,y9] , [y1,y3,y5,y7,y8,y11] , [y1,y3,y5,y9,y11] -- (*) , [y2,y3,y5,y7,y8,y11] , [y2,y4,y5,y6,y7,y8] -- (*) ] let remove1 :: [a] -> [[a]] remove1 [] = [] remove1 (x:xs) = xs : [x : ys | ys <- remove1 xs] forM_ cores $ \core -> do ret <- SAT.solveWith solver core assertBool (show core ++ " should be a core") (not ret) forM (remove1 core) $ \xs -> do ret <- SAT.solveWith solver xs assertBool (show core ++ " should be satisfiable") ret (actual,_) <- MUSEnum.allMUSAssumptions solver sels def{ MUSEnum.optMethod = method } let actual' = Set.fromList actual expected' = Set.fromList $ map IntSet.fromList $ cores actual' @?= expected' case_allMUSAssumptions_2_CAMUS :: Assertion case_allMUSAssumptions_2_CAMUS = allMUSAssumptions_case2 MUSEnum.CAMUS case_allMUSAssumptions_2_DAA :: Assertion case_allMUSAssumptions_2_DAA = allMUSAssumptions_case2 MUSEnum.DAA case_allMUSAssumptions_2_MARCO :: Assertion case_allMUSAssumptions_2_MARCO = allMUSAssumptions_case2 MUSEnum.MARCO case_allMUSAssumptions_2_GurvichKhachiyan1999 :: Assertion case_allMUSAssumptions_2_GurvichKhachiyan1999 = allMUSAssumptions_case2 MUSEnum.GurvichKhachiyan1999 case_allMUSAssumptions_2_HYCAM :: Assertion case_allMUSAssumptions_2_HYCAM = do solver <- SAT.newSolver [a,b,c,d,e] <- SAT.newVars solver 5 sels@[y0,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12] <- SAT.newVars solver 13 SAT.addClause solver [-y0, d] SAT.addClause solver [-y1, b, c] SAT.addClause solver [-y2, a, b] SAT.addClause solver [-y3, a, -c] SAT.addClause solver [-y4, -b, -e] SAT.addClause solver [-y5, -a, -b] SAT.addClause solver [-y6, a, e] SAT.addClause solver [-y7, -a, -e] SAT.addClause solver [-y8, b, e] SAT.addClause solver [-y9, -a, b, -c] SAT.addClause solver [-y10, -a, b, -d] SAT.addClause solver [-y11, a, -b, c] SAT.addClause solver [-y12, a, -b, -d] -- Only three of the MUSes (marked with asterisks) are on the paper. let cores = [ [y0,y1,y2,y5,y9,y12] , [y0,y1,y3,y4,y5,y6,y10] , [y0,y1,y3,y5,y7,y8,y12] , [y0,y1,y3,y5,y9,y12] , [y0,y1,y3,y5,y10,y11] , [y0,y1,y3,y5,y10,y12] , [y0,y2,y3,y5,y10,y11] , [y0,y2,y4,y5,y6,y10] , [y0,y2,y5,y7,y8,y12] , [y0,y2,y5,y10,y12] -- (*) , [y1,y2,y4,y5,y6,y9] , [y1,y3,y4,y5,y6,y7,y8] , [y1,y3,y4,y5,y6,y9] , [y1,y3,y5,y7,y8,y11] , [y1,y3,y5,y9,y11] -- (*) , [y2,y3,y5,y7,y8,y11] , [y2,y4,y5,y6,y7,y8] -- (*) ] mcses = [ [y0,y1,y7] , [y0,y1,y8] , [y0,y3,y4] , [y0,y3,y6] , [y0,y4,y11] , [y0,y6,y11] , [y0,y7,y9] , [y0,y8,y9] , [y1,y2] , [y1,y7,y10] , [y1,y8,y10] , [y2,y3] , [y3,y4,y12] , [y3,y6,y12] , [y4,y11,y12] , [y5] , [y6,y11,y12] , [y7,y9,y10] , [y8,y9,y10] ] -- HYCAM paper wrongly treated {C3,C8,C10} as a candidate MCS (CoMSS). -- Its complement {C0,C1,C2,C4,C5,C6,C7,C9,C11,C12} is unsatisfiable -- and hence not MSS. ret <- SAT.solveWith solver [y0,y1,y2,y4,y5,y6,y7,y9,y11,y12] assertBool "failed to prove the bug of HYCAM paper" (not ret) let cand = map IntSet.fromList [[y5], [y3,y2], [y0,y1,y2]] (actual,_) <- MUSEnum.allMUSAssumptions solver sels def{ MUSEnum.optMethod = MUSEnum.CAMUS, MUSEnum.optKnownCSes = cand } let actual' = Set.fromList $ actual expected' = Set.fromList $ map IntSet.fromList cores actual' @?= expected' ------------------------------------------------------------------------ satMUSTestGroup :: TestTree satMUSTestGroup = $(testGroupGenerator)