module ToySolver.Combinatorial.HittingSet.MARCO
(
module ToySolver.Combinatorial.HittingSet.InterestingSets
, run
, generateCNFAndDNF
, minimalHittingSets
) where
import Control.Monad
import Data.Default.Class
import Data.IntMap ((!))
import qualified Data.IntMap as IntMap
import Data.IntSet (IntSet)
import qualified Data.IntSet as IntSet
import Data.IORef
import Data.Set (Set)
import qualified Data.Set as Set
import System.IO.Unsafe
import ToySolver.Combinatorial.HittingSet.InterestingSets
import qualified ToySolver.SAT as SAT
run :: forall prob. IsProblem prob IO => prob -> Options IO -> IO (Set IntSet, Set IntSet)
run prob opt = do
solver <- SAT.newSolver
item2var <- liftM IntMap.fromList $ forM (IntSet.toList (universe prob)) $ \item -> do
v <- SAT.newVar solver
return (item,v)
let blockUp xs = SAT.addClause solver [(item2var ! x) | x <- IntSet.toList xs]
blockDown xs = SAT.addClause solver [item2var ! x | x <- IntSet.toList (universe prob `IntSet.difference` xs)]
posRef <- newIORef $ Set.toList $ optMaximalInterestingSets opt
negRef <- newIORef $ Set.toList $ optMinimalUninterestingSets opt
mapM_ blockUp $ Set.toList $ optMinimalUninterestingSets opt
mapM_ blockDown $ Set.toList $ optMaximalInterestingSets opt
let loop = do
ret <- SAT.solve solver
if not ret then
return ()
else do
model <- SAT.getModel solver
let xs = IntMap.keysSet $ IntMap.filter (SAT.evalLit model) item2var
ret2 <- minimalUninterestingSetOrMaximalInterestingSet prob xs
case ret2 of
UninterestingSet ys -> do
blockUp ys
modifyIORef negRef (ys :)
optOnMinimalUninterestingSetFound opt ys
InterestingSet ys -> do
blockDown ys
modifyIORef posRef (ys :)
optOnMaximalInterestingSetFound opt ys
loop
loop
pos <- readIORef posRef
neg <- readIORef negRef
return (Set.fromList pos, Set.fromList neg)
generateCNFAndDNF
:: IntSet
-> (IntSet -> Bool)
-> Set IntSet
-> Set IntSet
-> (Set IntSet, Set IntSet)
generateCNFAndDNF vs f cs ds = unsafeDupablePerformIO $ do
(pos,neg) <- run prob opt
return (Set.map (vs `IntSet.difference`) pos, neg)
where
prob = SimpleProblem vs (not . f)
opt = def
{ optMaximalInterestingSets = Set.map (vs `IntSet.difference`) cs
, optMinimalUninterestingSets = ds
}
minimalHittingSets :: Set IntSet -> Set IntSet
minimalHittingSets xss =
case generateCNFAndDNF (IntSet.unions $ Set.toList xss) (evalDNF xss) Set.empty xss of
(yss, _) -> yss
evalDNF :: Set IntSet -> IntSet -> Bool
evalDNF dnf xs = or [is `IntSet.isSubsetOf` xs | is <- Set.toList dnf]