-----------------------------------------------------------------------------
-- |
-- Module      :  ToySolver.SAT.MUS.QuickXplain
-- Copyright   :  (c) Masahiro Sakai 2015
-- License     :  BSD-style
--
-- Maintainer  :  masahiro.sakai@gmail.com
-- Stability   :  provisional
-- Portability :  portable
--
-- Minimal Unsatifiable Subset (MUS) Finder based on QuickXplain algorithm.
--
-- References:
--
-- * Ulrich Junker. QuickXplain: Preferred explanations and relaxations for
--   over-constrained problems. In Proc. of AAAI’04, pages 167-172, 2004.
--   <http://www.aaai.org/Papers/AAAI/2004/AAAI04-027.pdf>
--
-----------------------------------------------------------------------------
module ToySolver.SAT.MUS.QuickXplain
  ( module ToySolver.SAT.MUS.Base
  , Options (..)
  , findMUSAssumptions
  ) where

import Control.Monad
import Data.Default.Class
import Data.List
import qualified Data.IntSet as IS
import qualified ToySolver.SAT as SAT
import ToySolver.SAT.Types
import ToySolver.SAT.MUS.Base

-- | Find a minimal set of assumptions that causes a conflict.
-- Initial set of assumptions is taken from 'SAT.getFailedAssumptions'.
findMUSAssumptions
  :: SAT.Solver
  -> Options
  -> IO MUS
findMUSAssumptions :: Solver -> Options -> IO MUS
findMUSAssumptions Solver
solver Options
opt = do
  String -> IO ()
log String
"computing a minimal unsatisfiable core by QuickXplain"
  MUS
core <- Solver -> IO MUS
SAT.getFailedAssumptions Solver
solver
  String -> IO ()
log (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"initial core = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ MUS -> String
showLits MUS
core
  MUS -> IO ()
update MUS
core
  if MUS -> Bool
IS.null MUS
core then
    MUS -> IO MUS
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return MUS
core
  else
    ((MUS, MUS) -> MUS) -> IO (MUS, MUS) -> IO MUS
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (MUS, MUS) -> MUS
forall a b. (a, b) -> a
fst (IO (MUS, MUS) -> IO MUS) -> IO (MUS, MUS) -> IO MUS
forall a b. (a -> b) -> a -> b
$ MUS -> Bool -> MUS -> IO (MUS, MUS)
f MUS
IS.empty Bool
False MUS
core

  where
    log :: String -> IO ()
    log :: String -> IO ()
log = Options -> String -> IO ()
optLogger Options
opt

    update :: US -> IO ()
    update :: MUS -> IO ()
update = Options -> MUS -> IO ()
optUpdateBest Options
opt

    showLit :: Lit -> String
    showLit :: Int -> String
showLit = Options -> Int -> String
optShowLit Options
opt

    showLits :: IS.IntSet -> String
    showLits :: MUS -> String
showLits MUS
ls = String
"{" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
", " ((Int -> String) -> [Int] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Int -> String
showLit (MUS -> [Int]
IS.toList MUS
ls)) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"}"

    split :: IS.IntSet -> (IS.IntSet, IS.IntSet)
    split :: MUS -> (MUS, MUS)
split MUS
cs = (MUS
cs1, MUS
cs2)
      where
        s :: Int
s = MUS -> Int
IS.size MUS
cs
        cs' :: [Int]
cs' = MUS -> [Int]
IS.toAscList MUS
cs
        cs1 :: MUS
cs1 = [Int] -> MUS
IS.fromAscList ([Int] -> MUS) -> [Int] -> MUS
forall a b. (a -> b) -> a -> b
$ Int -> [Int] -> [Int]
forall a. Int -> [a] -> [a]
take (Int
s Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
2) [Int]
cs'
        cs2 :: MUS
cs2 = [Int] -> MUS
IS.fromAscList ([Int] -> MUS) -> [Int] -> MUS
forall a b. (a -> b) -> a -> b
$ Int -> [Int] -> [Int]
forall a. Int -> [a] -> [a]
drop (Int
s Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
2) [Int]
cs'

    -- Precondition:
    -- * bs∪cs is unsatisfiable
    -- * ¬hasDelta ⇒ bs is satisfiable
    --
    -- Returns:
    -- * minimal subset cs'⊆cs such that bs∪cs' is unsatisfiable
    -- * (not necessarily minimal) subset bs'⊆bs such that bs'∪cs' is unsatisfiable.
    f :: IS.IntSet -> Bool -> IS.IntSet -> IO (IS.IntSet, IS.IntSet)
    f :: MUS -> Bool -> MUS -> IO (MUS, MUS)
f MUS
bs Bool
hasDelta MUS
cs = do
      String -> IO ()
log (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"checking satisfiability of " String -> String -> String
forall a. [a] -> [a] -> [a]
++ MUS -> String
showLits MUS
bs
      Bool
ret <- if Bool -> Bool
not Bool
hasDelta then do
               Bool -> IO Bool
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
             else
               Solver -> [Int] -> IO Bool
SAT.solveWith Solver
solver (MUS -> [Int]
IS.toList MUS
bs)
      if Bool -> Bool
not Bool
ret then do
        String -> IO ()
log (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ MUS -> String
showLits MUS
bs String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" is unsatisfiable"
        MUS
bs' <- Solver -> IO MUS
SAT.getFailedAssumptions Solver
solver
        String -> IO ()
log (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"new core = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ MUS -> String
showLits MUS
bs'
        MUS -> IO ()
update MUS
bs'
        (MUS, MUS) -> IO (MUS, MUS)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (MUS
IS.empty, MUS
bs')
      else do
        String -> IO ()
log (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ MUS -> String
showLits MUS
bs String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" is satisfiable"
        if MUS -> Int
IS.size MUS
cs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1 then do
          (MUS, MUS) -> IO (MUS, MUS)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (MUS
cs, MUS
bs)
        else do
          let (MUS
cs1,MUS
cs2) = MUS -> (MUS, MUS)
split MUS
cs
          String -> IO ()
log (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"splitting " String -> String -> String
forall a. [a] -> [a] -> [a]
++ MUS -> String
showLits MUS
cs String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" into " String -> String -> String
forall a. [a] -> [a] -> [a]
++ MUS -> String
showLits MUS
cs1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" and " String -> String -> String
forall a. [a] -> [a] -> [a]
++ MUS -> String
showLits MUS
cs2
          (MUS
ds2, MUS
es2) <- MUS -> Bool -> MUS -> IO (MUS, MUS)
f (MUS
bs MUS -> MUS -> MUS
`IS.union` MUS
cs1) (Bool -> Bool
not (MUS -> Bool
IS.null MUS
cs1)) MUS
cs2
          let bs' :: MUS
bs'  = MUS
bs MUS -> MUS -> MUS
`IS.intersection` MUS
es2
              cs1' :: MUS
cs1' = MUS
cs1 MUS -> MUS -> MUS
`IS.intersection` MUS
es2
          (MUS
ds1, MUS
es1) <- MUS -> Bool -> MUS -> IO (MUS, MUS)
f (MUS
bs' MUS -> MUS -> MUS
`IS.union` MUS
ds2) (Bool -> Bool
not (MUS -> Bool
IS.null MUS
ds2)) MUS
cs1'
          (MUS, MUS) -> IO (MUS, MUS)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (MUS
ds1 MUS -> MUS -> MUS
`IS.union` MUS
ds2, MUS
bs MUS -> MUS -> MUS
`IS.intersection` (MUS
es1 MUS -> MUS -> MUS
`IS.union` MUS
es2))

{-
Algorithm QUICKXPLAIN(B, C, ≺)
 1. if isConsistent(B ∪ C) return 'no conflict';
 2. else if C = ∅ then return ∅;
 3. else return QUICKXPLAIN'(B, B, C, ≺);

Algorithm QUICKXPLAIN'(B, ∆, C, ≺)
 4. if ∆ ≠ ∅ and not isConsistent(B) then return ∅;
 5. if C = {α} then return {α};
 6. let α_1, …, α_n be an enumeration of C that respects ≺;
 7. let k be split(n) where 1 ≤ k < n;
 8. C1 := {α_1, …, α_k} and C2 := {α_{k+1}, …, α_n};
 9. ∆2 := QUICKXPLAIN'(B ∪ C1, C1, C2, ≺);
10. ∆1 := QUICKXPLAIN'(B ∪ ∆2, ∆2, C1, ≺);
11. return ∆1 ∪ ∆2;
-}