{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_HADDOCK show-extensions #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
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 :: forall prob.
IsProblem prob IO =>
prob -> Options IO -> IO (Set IntSet, Set IntSet)
run prob
prob Options IO
opt = do
Solver
solver <- IO Solver
SAT.newSolver
IntMap Var
item2var <- forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM forall a. [(Var, a)] -> IntMap a
IntMap.fromList forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (IntSet -> [Var]
IntSet.toList (forall prob (m :: * -> *). IsProblem prob m => prob -> IntSet
universe prob
prob)) forall a b. (a -> b) -> a -> b
$ \Var
item -> do
Var
v <- forall (m :: * -> *) a. NewVar m a => a -> m Var
SAT.newVar Solver
solver
forall (m :: * -> *) a. Monad m => a -> m a
return (Var
item,Var
v)
let blockUp :: IntSet -> IO ()
blockUp IntSet
xs = forall (m :: * -> *) a. AddClause m a => a -> [Var] -> m ()
SAT.addClause Solver
solver [-(IntMap Var
item2var forall a. IntMap a -> Var -> a
! Var
x) | Var
x <- IntSet -> [Var]
IntSet.toList IntSet
xs]
blockDown :: IntSet -> IO ()
blockDown IntSet
xs = forall (m :: * -> *) a. AddClause m a => a -> [Var] -> m ()
SAT.addClause Solver
solver [IntMap Var
item2var forall a. IntMap a -> Var -> a
! Var
x | Var
x <- IntSet -> [Var]
IntSet.toList (forall prob (m :: * -> *). IsProblem prob m => prob -> IntSet
universe prob
prob IntSet -> IntSet -> IntSet
`IntSet.difference` IntSet
xs)]
IORef [IntSet]
posRef <- forall a. a -> IO (IORef a)
newIORef forall a b. (a -> b) -> a -> b
$ forall a. Set a -> [a]
Set.toList forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Options m -> Set IntSet
optMaximalInterestingSets Options IO
opt
IORef [IntSet]
negRef <- forall a. a -> IO (IORef a)
newIORef forall a b. (a -> b) -> a -> b
$ forall a. Set a -> [a]
Set.toList forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Options m -> Set IntSet
optMinimalUninterestingSets Options IO
opt
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ IntSet -> IO ()
blockUp forall a b. (a -> b) -> a -> b
$ forall a. Set a -> [a]
Set.toList forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Options m -> Set IntSet
optMinimalUninterestingSets Options IO
opt
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ IntSet -> IO ()
blockDown forall a b. (a -> b) -> a -> b
$ forall a. Set a -> [a]
Set.toList forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Options m -> Set IntSet
optMaximalInterestingSets Options IO
opt
let loop :: IO ()
loop = do
Bool
ret <- Solver -> IO Bool
SAT.solve Solver
solver
if Bool -> Bool
not Bool
ret then
forall (m :: * -> *) a. Monad m => a -> m a
return ()
else do
Model
model <- Solver -> IO Model
SAT.getModel Solver
solver
let xs :: IntSet
xs = forall a. IntMap a -> IntSet
IntMap.keysSet forall a b. (a -> b) -> a -> b
$ forall a. (a -> Bool) -> IntMap a -> IntMap a
IntMap.filter (forall m. IModel m => m -> Var -> Bool
SAT.evalLit Model
model) IntMap Var
item2var
InterestingOrUninterestingSet
ret2 <- forall prob (m :: * -> *).
IsProblem prob m =>
prob -> IntSet -> m InterestingOrUninterestingSet
minimalUninterestingSetOrMaximalInterestingSet prob
prob IntSet
xs
case InterestingOrUninterestingSet
ret2 of
UninterestingSet IntSet
ys -> do
IntSet -> IO ()
blockUp IntSet
ys
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef IORef [IntSet]
negRef (IntSet
ys forall a. a -> [a] -> [a]
:)
forall (m :: * -> *). Options m -> IntSet -> m ()
optOnMinimalUninterestingSetFound Options IO
opt IntSet
ys
InterestingSet IntSet
ys -> do
IntSet -> IO ()
blockDown IntSet
ys
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef IORef [IntSet]
posRef (IntSet
ys forall a. a -> [a] -> [a]
:)
forall (m :: * -> *). Options m -> IntSet -> m ()
optOnMaximalInterestingSetFound Options IO
opt IntSet
ys
IO ()
loop
IO ()
loop
[IntSet]
pos <- forall a. IORef a -> IO a
readIORef IORef [IntSet]
posRef
[IntSet]
neg <- forall a. IORef a -> IO a
readIORef IORef [IntSet]
negRef
forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. Ord a => [a] -> Set a
Set.fromList [IntSet]
pos, forall a. Ord a => [a] -> Set a
Set.fromList [IntSet]
neg)
generateCNFAndDNF
:: IntSet
-> (IntSet -> Bool)
-> Set IntSet
-> Set IntSet
-> (Set IntSet, Set IntSet)
generateCNFAndDNF :: IntSet
-> (IntSet -> Bool)
-> Set IntSet
-> Set IntSet
-> (Set IntSet, Set IntSet)
generateCNFAndDNF IntSet
vs IntSet -> Bool
f Set IntSet
cs Set IntSet
ds = forall a. IO a -> a
unsafeDupablePerformIO forall a b. (a -> b) -> a -> b
$ do
(Set IntSet
pos,Set IntSet
neg) <- forall prob.
IsProblem prob IO =>
prob -> Options IO -> IO (Set IntSet, Set IntSet)
run forall {m :: * -> *}. SimpleProblem m
prob Options IO
opt
forall (m :: * -> *) a. Monad m => a -> m a
return (forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (IntSet
vs IntSet -> IntSet -> IntSet
`IntSet.difference`) Set IntSet
pos, Set IntSet
neg)
where
prob :: SimpleProblem m
prob = forall (m :: * -> *). IntSet -> (IntSet -> Bool) -> SimpleProblem m
SimpleProblem IntSet
vs (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. IntSet -> Bool
f)
opt :: Options IO
opt = forall a. Default a => a
def
{ optMaximalInterestingSets :: Set IntSet
optMaximalInterestingSets = forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (IntSet
vs IntSet -> IntSet -> IntSet
`IntSet.difference`) Set IntSet
cs
, optMinimalUninterestingSets :: Set IntSet
optMinimalUninterestingSets = Set IntSet
ds
}
minimalHittingSets :: Set IntSet -> Set IntSet
minimalHittingSets :: Set IntSet -> Set IntSet
minimalHittingSets Set IntSet
xss =
case IntSet
-> (IntSet -> Bool)
-> Set IntSet
-> Set IntSet
-> (Set IntSet, Set IntSet)
generateCNFAndDNF (forall (f :: * -> *). Foldable f => f IntSet -> IntSet
IntSet.unions forall a b. (a -> b) -> a -> b
$ forall a. Set a -> [a]
Set.toList Set IntSet
xss) (Set IntSet -> IntSet -> Bool
evalDNF Set IntSet
xss) forall a. Set a
Set.empty Set IntSet
xss of
(Set IntSet
yss, Set IntSet
_) -> Set IntSet
yss
evalDNF :: Set IntSet -> IntSet -> Bool
evalDNF :: Set IntSet -> IntSet -> Bool
evalDNF Set IntSet
dnf IntSet
xs = forall (t :: * -> *). Foldable t => t Bool -> Bool
or [IntSet
is IntSet -> IntSet -> Bool
`IntSet.isSubsetOf` IntSet
xs | IntSet
is <- forall a. Set a -> [a]
Set.toList Set IntSet
dnf]