module Jukebox.Sat.Minimise where
import Jukebox.Sat
solveLocalMin :: SatSolver s => s -> [Lit] -> [Lit] -> IO Bool
solveLocalMin :: s -> [Lit] -> [Lit] -> IO Bool
solveLocalMin s
s [Lit]
as [Lit]
ms =
do Bool
b <- s -> [Lit] -> IO Bool
forall s. SatSolver s => s -> [Lit] -> IO Bool
solve s
s [Lit]
as
if Bool
b then do Lit
l <- s -> IO Lit
forall s. SatSolver s => s -> IO Lit
newLit s
s
s -> [Lit] -> Lit -> [Lit] -> IO ()
forall s. SatSolver s => s -> [Lit] -> Lit -> [Lit] -> IO ()
localMin s
s [Lit]
as Lit
l [Lit]
ms
s -> [Lit] -> IO ()
forall s. SatSolver s => s -> [Lit] -> IO ()
addClause s
s [Lit -> Lit
neg Lit
l]
Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
else do Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
localMin :: SatSolver s => s -> [Lit] -> Lit -> [Lit] -> IO ()
localMin :: s -> [Lit] -> Lit -> [Lit] -> IO ()
localMin s
s [Lit]
as Lit
l [Lit]
ms =
do
[Maybe Bool]
bs <- [IO (Maybe Bool)] -> IO [Maybe Bool]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [ s -> Lit -> IO (Maybe Bool)
forall s. SatSolver s => s -> Lit -> IO (Maybe Bool)
modelValue s
s Lit
m | Lit
m <- [Lit]
ms ]
[IO ()] -> IO ()
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
t (m a) -> m ()
sequence_ [ s -> [Lit] -> IO ()
forall s. SatSolver s => s -> [Lit] -> IO ()
addClause s
s [Lit -> Lit
neg Lit
l, Lit -> Lit
neg Lit
m] | (Lit
m,Maybe Bool
b) <- [Lit]
ms [Lit] -> [Maybe Bool] -> [(Lit, Maybe Bool)]
forall a b. [a] -> [b] -> [(a, b)]
`zip` [Maybe Bool]
bs, Maybe Bool
b Maybe Bool -> Maybe Bool -> Bool
forall a. Eq a => a -> a -> Bool
/= Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True ]
let ms1 :: [Lit]
ms1 = [ Lit
m | (Lit
m,Just Bool
True) <- [Lit]
ms [Lit] -> [Maybe Bool] -> [(Lit, Maybe Bool)]
forall a b. [a] -> [b] -> [(a, b)]
`zip` [Maybe Bool]
bs ]
s -> [Lit] -> IO ()
forall s. SatSolver s => s -> [Lit] -> IO ()
addClause s
s (Lit -> Lit
neg Lit
l Lit -> [Lit] -> [Lit]
forall a. a -> [a] -> [a]
: [ Lit -> Lit
neg Lit
m | Lit
m <- [Lit]
ms1 ])
Bool
b <- s -> [Lit] -> IO Bool
forall s. SatSolver s => s -> [Lit] -> IO Bool
solve s
s (Lit
lLit -> [Lit] -> [Lit]
forall a. a -> [a] -> [a]
:[Lit]
as)
if Bool
b then s -> [Lit] -> Lit -> [Lit] -> IO ()
forall s. SatSolver s => s -> [Lit] -> Lit -> [Lit] -> IO ()
localMin s
s [Lit]
as Lit
l [Lit]
ms1
else () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()