toysolver-0.7.0: src/ToySolver/SAT/MUS/Enum.hs

{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_HADDOCK show-extensions #-}
{-# LANGUAGE MultiParamTypeClasses #-}

-----------------------------------------------------------------------------
-- |
-- Module      :  ToySolver.SAT.MUS.Enum
-- Copyright   :  (c) Masahiro Sakai 2012-2016
-- License     :  BSD-style
--
-- Maintainer  :  masahiro.sakai@gmail.com
-- Stability   :  provisional
-- Portability :  non-portable
--
-- In this module, we assume each soft constraint /C_i/ is represented as a literal.
-- If a constraint /C_i/ is not a literal, we can represent it as a fresh variable /v/
-- together with a hard constraint /v ⇒ C_i/.
--
-- References:
--
-- * [CAMUS] M. Liffiton and K. Sakallah, Algorithms for computing minimal
--   unsatisfiable subsets of constraints, Journal of Automated Reasoning,
--   vol. 40, no. 1, pp. 1-33, Jan. 2008.
--   <http://sun.iwu.edu/~mliffito/publications/jar_liffiton_CAMUS.pdf>
--
-- * [HYCAM] A. Gregoire, B. Mazure, and C. Piette, Boosting a complete
--   technique to find MSS and MUS: thanks to a local search oracle, in
--   Proceedings of the 20th international joint conference on Artifical
--   intelligence, ser. IJCAI'07. San Francisco, CA, USA: Morgan Kaufmann
--   Publishers Inc., 2007, pp. 2300-2305.
--   <http://ijcai.org/papers07/Papers/IJCAI07-370.pdf>
--
-- * [DAA] J. Bailey and P. Stuckey, Discovery of minimal unsatisfiable
--   subsets of constraints using hitting set dualization," in Practical
--   Aspects of Declarative Languages, pp. 174-186, 2005.
--   <http://ww2.cs.mu.oz.au/~pjs/papers/padl05.pdf>
--
-----------------------------------------------------------------------------
module ToySolver.SAT.MUS.Enum
  ( module ToySolver.SAT.MUS.Types
  , Method (..)
  , showMethod
  , parseMethod
  , Options (..)
  , allMUSAssumptions
  ) where

import Data.Char
import Data.Default.Class
import qualified Data.IntSet as IntSet
import Data.List (intercalate)
import qualified Data.Set as Set
import qualified ToySolver.Combinatorial.HittingSet.InterestingSets as I
import qualified ToySolver.Combinatorial.HittingSet.DAA as DAA
import qualified ToySolver.Combinatorial.HittingSet.MARCO as MARCO
import qualified ToySolver.Combinatorial.HittingSet.GurvichKhachiyan1999 as GurvichKhachiyan1999
import qualified ToySolver.SAT as SAT
import ToySolver.SAT.Types
import ToySolver.SAT.MUS.Types
import ToySolver.SAT.MUS.Enum.Base
import qualified ToySolver.SAT.MUS.Enum.CAMUS as CAMUS

showMethod :: Method -> String
showMethod m = map toLower (show m)

parseMethod :: String -> Maybe Method
parseMethod s =
  case filter (/='-') $ map toLower s of
    "camus" -> Just CAMUS
    "daa" -> Just DAA
    "marco" -> Just MARCO
    "gurvichkhachiyan1999" -> Just GurvichKhachiyan1999
    _ -> Nothing

allMUSAssumptions :: SAT.Solver -> [Lit] -> Options -> IO ([MUS], [MCS])
allMUSAssumptions solver sels opt =
  case optMethod opt of
    CAMUS -> CAMUS.allMUSAssumptions solver sels opt
    DAA -> do
      (msses, muses) <- DAA.run prob opt2
      return (Set.toList muses, map mss2mcs (Set.toList msses))
    MARCO -> do
      (msses, muses) <- MARCO.run prob opt2
      return (Set.toList muses, map mss2mcs (Set.toList msses))
    GurvichKhachiyan1999 -> do
      (msses, muses) <- GurvichKhachiyan1999.run prob opt2
      return (Set.toList muses, map mss2mcs (Set.toList msses))
  where
    prob = Problem solver selsSet opt

    opt2 :: I.Options IO
    opt2 =
      (def :: I.Options IO)
      { I.optOnMaximalInterestingSetFound = \xs ->
          optOnMCSFound opt (mss2mcs xs)
      , I.optOnMinimalUninterestingSetFound = \xs ->
          optOnMUSFound opt xs
      }

    selsSet :: LitSet
    selsSet = IntSet.fromList sels

    mss2mcs :: LitSet -> LitSet
    mss2mcs = (selsSet `IntSet.difference`)

-- -----------------------------------------------------------------

data Problem = Problem SAT.Solver LitSet Options

instance I.IsProblem Problem IO where
  universe (Problem _ univ _) = univ

  isInteresting' (Problem solver univ opt) xs = do
    b <- SAT.solveWith solver (IntSet.toList xs)
    if b then do
      m <- SAT.getModel solver
      return $ I.InterestingSet $ IntSet.fromList [l | l <- IntSet.toList univ, optEvalConstr opt m l]
    else do
      zs <- SAT.getFailedAssumptions solver
      return $ I.UninterestingSet zs

  grow prob@(Problem _ _ opt) xs = do
    optLogger opt $ show (optMethod opt) ++ ": grow " ++ showLits prob xs
    ys <- I.defaultGrow prob xs
    optLogger opt $ show (optMethod opt) ++ ": grow added " ++ showLits prob (ys `IntSet.difference` xs)
    return ys

  shrink prob@(Problem _ _ opt) xs = do
    optLogger opt $ show (optMethod opt) ++ ": shrink " ++ showLits prob xs
    ys <- I.defaultShrink prob xs
    optLogger opt $ show (optMethod opt) ++ ": shrink deleted " ++ showLits prob (xs `IntSet.difference` ys)
    return ys

showLits :: Problem -> IntSet.IntSet -> String
showLits (Problem _ _ opt) ls =
  "{" ++ intercalate ", " (map (optShowLit opt) (IntSet.toList ls)) ++ "}"

-- -----------------------------------------------------------------