{-# OPTIONS_GHC -Wall #-}
{-# LANGUAGE TypeFamilies #-}
module ToySolver.Converter.SAT2MIS
  (
  -- * SAT to independent set problem conversion
    satToIS
  , SAT2ISInfo

  -- * 3-SAT to independent set problem conversion
  , sat3ToIS
  , SAT3ToISInfo

  -- * Maximum independent problem to MaxSAT/PB problem conversion
  , is2pb
  , mis2MaxSAT
  , IS2SATInfo
  ) where

import Control.Monad
import Control.Monad.ST
import Data.Array.IArray
import Data.Array.ST
import Data.Array.Unboxed
import qualified Data.IntMap as IntMap
import qualified Data.IntSet as IntSet
import Data.IntSet (IntSet)
import Data.Maybe
import Data.STRef

import qualified Data.PseudoBoolean as PBFile

import ToySolver.Converter.Base
import ToySolver.Converter.SAT2KSAT
import qualified ToySolver.FileFormat.CNF as CNF
import ToySolver.Graph.Base
import ToySolver.SAT.Store.CNF
import ToySolver.SAT.Store.PB
import qualified ToySolver.SAT.Types as SAT

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

satToIS :: CNF.CNF -> ((Graph, Int), SAT2ISInfo)
satToIS :: CNF -> ((Graph, Int), SAT2ISInfo)
satToIS CNF
x = ((Graph, Int)
x2, (forall a b. a -> b -> ComposedTransformer a b
ComposedTransformer SAT2KSATInfo
info1 SAT3ToISInfo
info2))
  where
    (CNF
x1, SAT2KSATInfo
info1) = Int -> CNF -> (CNF, SAT2KSATInfo)
sat2ksat Int
3 CNF
x
    ((Graph, Int)
x2, SAT3ToISInfo
info2) = CNF -> ((Graph, Int), SAT3ToISInfo)
sat3ToIS CNF
x1

type SAT2ISInfo = ComposedTransformer SAT2KSATInfo SAT3ToISInfo

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

sat3ToIS :: CNF.CNF -> ((Graph, Int), SAT3ToISInfo)
sat3ToIS :: CNF -> ((Graph, Int), SAT3ToISInfo)
sat3ToIS CNF
cnf = forall a. (forall s. ST s a) -> a
runST forall a b. (a -> b) -> a -> b
$ do
  STRef s Int
nRef <- forall a s. a -> ST s (STRef s a)
newSTRef Int
0
  STRef s (IntMap [Int])
litToNodesRef <- forall a s. a -> ST s (STRef s a)
newSTRef forall a. IntMap a
IntMap.empty
  STRef s [Int]
nodeToLitRef <- forall a s. a -> ST s (STRef s a)
newSTRef []
  let newNode :: Int -> ST s Int
newNode Int
lit = do
        Int
n <- forall s a. STRef s a -> ST s a
readSTRef STRef s Int
nRef
        forall s a. STRef s a -> a -> ST s ()
writeSTRef STRef s Int
nRef forall a b. (a -> b) -> a -> b
$! Int
n forall a. Num a => a -> a -> a
+ Int
1
        forall s a. STRef s a -> (a -> a) -> ST s ()
modifySTRef' STRef s (IntMap [Int])
litToNodesRef (forall a. (Maybe a -> Maybe a) -> Int -> IntMap a -> IntMap a
IntMap.alter (forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int
n forall a. a -> [a] -> [a]
:) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Maybe a -> a
fromMaybe []) Int
lit)
        forall s a. STRef s a -> (a -> a) -> ST s ()
modifySTRef STRef s [Int]
nodeToLitRef (Int
lit forall a. a -> [a] -> [a]
:)
        forall (m :: * -> *) a. Monad m => a -> m a
return Int
n

  [[Int]]
clusters <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (CNF -> [PackedClause]
CNF.cnfClauses CNF
cnf) forall a b. (a -> b) -> a -> b
$ \PackedClause
clause -> do
    forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Int -> ST s Int
newNode (PackedClause -> [Int]
SAT.unpackClause PackedClause
clause)

  IntMap [Int]
litToNodes <- forall s a. STRef s a -> ST s a
readSTRef STRef s (IntMap [Int])
litToNodesRef
  let es :: [(Int, Int, ())]
es = forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall a b. (a -> b) -> a -> b
$
        [ [(Int
node1, Int
node2, ()) | (Int
node1, Int
node2) <- forall a. [a] -> [(a, a)]
pairs [Int]
nodes] | [Int]
nodes <- [[Int]]
clusters ] forall a. [a] -> [a] -> [a]
++
        [ [(Int
node1, Int
node2, ()) | Int
node1 <- [Int]
nodes1, Int
node2 <- [Int]
nodes2]
        | (Int
lit, [Int]
nodes1) <- forall a. IntMap a -> [(Int, a)]
IntMap.toList IntMap [Int]
litToNodes
        , let nodes2 :: [Int]
nodes2 = forall a. a -> Int -> IntMap a -> a
IntMap.findWithDefault [] (- Int
lit) IntMap [Int]
litToNodes
        ]

  Int
n <- forall s a. STRef s a -> ST s a
readSTRef STRef s Int
nRef
  let g :: Graph
g = forall a. Int -> [(Int, Int, a)] -> EdgeLabeledGraph a
graphFromUnorderedEdges Int
n [(Int, Int, ())]
es

  [Int]
xs <- forall s a. STRef s a -> ST s a
readSTRef STRef s [Int]
nodeToLitRef
  let nodeToLit :: UArray Int Int
nodeToLit = forall i e. (forall s. ST s (STUArray s i e)) -> UArray i e
runSTUArray forall a b. (a -> b) -> a -> b
$ do
        STUArray s Int Int
a <- forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
(i, i) -> m (a i e)
newArray_ (Int
0,Int
nforall a. Num a => a -> a -> a
-Int
1)
        forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (forall a b. [a] -> [b] -> [(a, b)]
zip [Int
nforall a. Num a => a -> a -> a
-Int
1,Int
nforall a. Num a => a -> a -> a
-Int
2..] [Int]
xs) forall a b. (a -> b) -> a -> b
$ \(Int
i, Int
lit) -> do
          forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
a i e -> i -> e -> m ()
writeArray STUArray s Int Int
a Int
i Int
lit
        forall (m :: * -> *) a. Monad m => a -> m a
return STUArray s Int Int
a

  forall (m :: * -> *) a. Monad m => a -> m a
return ((Graph
g, CNF -> Int
CNF.cnfNumClauses CNF
cnf), Int -> [[Int]] -> UArray Int Int -> SAT3ToISInfo
SAT3ToISInfo (CNF -> Int
CNF.cnfNumVars CNF
cnf) [[Int]]
clusters UArray Int Int
nodeToLit)


data SAT3ToISInfo = SAT3ToISInfo Int [[Int]] (UArray Int SAT.Lit)
  deriving (SAT3ToISInfo -> SAT3ToISInfo -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SAT3ToISInfo -> SAT3ToISInfo -> Bool
$c/= :: SAT3ToISInfo -> SAT3ToISInfo -> Bool
== :: SAT3ToISInfo -> SAT3ToISInfo -> Bool
$c== :: SAT3ToISInfo -> SAT3ToISInfo -> Bool
Eq, Int -> SAT3ToISInfo -> ShowS
[SAT3ToISInfo] -> ShowS
SAT3ToISInfo -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SAT3ToISInfo] -> ShowS
$cshowList :: [SAT3ToISInfo] -> ShowS
show :: SAT3ToISInfo -> String
$cshow :: SAT3ToISInfo -> String
showsPrec :: Int -> SAT3ToISInfo -> ShowS
$cshowsPrec :: Int -> SAT3ToISInfo -> ShowS
Show)
-- Note that array <0.5.4.0 did not provided Read instance of UArray

instance Transformer SAT3ToISInfo where
  type Source SAT3ToISInfo = SAT.Model
  type Target SAT3ToISInfo = IntSet

instance ForwardTransformer SAT3ToISInfo where
  transformForward :: SAT3ToISInfo -> Source SAT3ToISInfo -> Target SAT3ToISInfo
transformForward (SAT3ToISInfo Int
_nv [[Int]]
clusters UArray Int Int
nodeToLit) Source SAT3ToISInfo
m = [Int] -> IntSet
IntSet.fromList forall a b. (a -> b) -> a -> b
$ do
    [Int]
nodes <- [[Int]]
clusters
    let xs :: [Int]
xs = [Int
node | Int
node <- [Int]
nodes, forall m. IModel m => m -> Int -> Bool
SAT.evalLit Source SAT3ToISInfo
m (UArray Int Int
nodeToLit forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> i -> e
! Int
node)]
    if forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Int]
xs then
      forall a. HasCallStack => String -> a
error String
"not a model"
    else
      forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. [a] -> a
head [Int]
xs)

instance BackwardTransformer SAT3ToISInfo where
  transformBackward :: SAT3ToISInfo -> Target SAT3ToISInfo -> Source SAT3ToISInfo
transformBackward (SAT3ToISInfo Int
nv [[Int]]
_clusters UArray Int Int
nodeToLit) Target SAT3ToISInfo
indep_set = forall i e. (forall s. ST s (STUArray s i e)) -> UArray i e
runSTUArray forall a b. (a -> b) -> a -> b
$ do
    STUArray s Int Bool
a <- forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
(i, i) -> e -> m (a i e)
newArray (Int
1, Int
nv) Bool
False
    forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (IntSet -> [Int]
IntSet.toList IntSet
lits) forall a b. (a -> b) -> a -> b
$ \Int
lit -> do
      forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
a i e -> i -> e -> m ()
writeArray STUArray s Int Bool
a (Int -> Int
SAT.litVar Int
lit) (Int -> Bool
SAT.litPolarity Int
lit)
    forall (m :: * -> *) a. Monad m => a -> m a
return STUArray s Int Bool
a
    where
      lits :: IntSet
lits = (Int -> Int) -> IntSet -> IntSet
IntSet.map (UArray Int Int
nodeToLit forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> i -> e
!) Target SAT3ToISInfo
indep_set

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

is2pb :: (Graph, Int) -> (PBFile.Formula, IS2SATInfo)
is2pb :: (Graph, Int) -> (Formula, IS2SATInfo)
is2pb (Graph
g, Int
k) = forall a. (forall s. ST s a) -> a
runST forall a b. (a -> b) -> a -> b
$ do
  let (Int
lb, Int
ub) = forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> (i, i)
bounds Graph
g
  PBStore (ST s)
db <- forall (m :: * -> *). PrimMonad m => m (PBStore m)
newPBStore
  [Int]
vs <- forall (m :: * -> *) a. NewVar m a => a -> Int -> m [Int]
SAT.newVars PBStore (ST s)
db (forall a. Ix a => (a, a) -> Int
rangeSize (forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> (i, i)
bounds Graph
g))
  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (forall a. EdgeLabeledGraph a -> [(Int, Int, a)]
graphToUnorderedEdges Graph
g) forall a b. (a -> b) -> a -> b
$ \(Int
node1, Int
node2, ()
_) -> do
    forall (m :: * -> *) a. AddClause m a => a -> [Int] -> m ()
SAT.addClause PBStore (ST s)
db [- (Int
node1 forall a. Num a => a -> a -> a
- Int
lb forall a. Num a => a -> a -> a
+ Int
1), - (Int
node2 forall a. Num a => a -> a -> a
- Int
lb forall a. Num a => a -> a -> a
+ Int
1)]
  forall (m :: * -> *) a.
AddPBLin m a =>
a -> PBLinSum -> Integer -> m ()
SAT.addPBAtLeast PBStore (ST s)
db [(Integer
1,Int
v) | Int
v <- [Int]
vs] (forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
k)
  Formula
formula <- forall (m :: * -> *). PrimMonad m => PBStore m -> m Formula
getPBFormula PBStore (ST s)
db
  forall (m :: * -> *) a. Monad m => a -> m a
return
    ( Formula
formula
    , (Int, Int) -> IS2SATInfo
IS2SATInfo (Int
lb, Int
ub)
    )

mis2MaxSAT :: Graph -> (CNF.WCNF, IS2SATInfo)
mis2MaxSAT :: Graph -> (WCNF, IS2SATInfo)
mis2MaxSAT Graph
g = forall a. (forall s. ST s a) -> a
runST forall a b. (a -> b) -> a -> b
$ do
  let (Int
lb,Int
ub) = forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> (i, i)
bounds Graph
g
      n :: Int
n = Int
ub forall a. Num a => a -> a -> a
- Int
lb forall a. Num a => a -> a -> a
+ Int
1
  CNFStore (ST s)
db <- forall (m :: * -> *). PrimMonad m => m (CNFStore m)
newCNFStore
  [Int]
vs <- forall (m :: * -> *) a. NewVar m a => a -> Int -> m [Int]
SAT.newVars CNFStore (ST s)
db Int
n
  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (forall a. EdgeLabeledGraph a -> [(Int, Int, a)]
graphToUnorderedEdges Graph
g) forall a b. (a -> b) -> a -> b
$ \(Int
node1, Int
node2, ()
_) -> do
    forall (m :: * -> *) a. AddClause m a => a -> [Int] -> m ()
SAT.addClause CNFStore (ST s)
db [- (Int
node1 forall a. Num a => a -> a -> a
- Int
lb forall a. Num a => a -> a -> a
+ Int
1), - (Int
node2 forall a. Num a => a -> a -> a
- Int
lb forall a. Num a => a -> a -> a
+ Int
1)]
  CNF
cnf <- forall (m :: * -> *). PrimMonad m => CNFStore m -> m CNF
getCNFFormula CNFStore (ST s)
db
  let top :: Integer
top = forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
n forall a. Num a => a -> a -> a
+ Integer
1
  forall (m :: * -> *) a. Monad m => a -> m a
return
    ( CNF.WCNF
      { wcnfNumVars :: Int
CNF.wcnfNumVars = CNF -> Int
CNF.cnfNumVars CNF
cnf
      , wcnfNumClauses :: Int
CNF.wcnfNumClauses = CNF -> Int
CNF.cnfNumClauses CNF
cnf forall a. Num a => a -> a -> a
+ Int
n
      , wcnfTopCost :: Integer
CNF.wcnfTopCost = Integer
top
      , wcnfClauses :: [WeightedClause]
CNF.wcnfClauses =
          [(Integer
top, PackedClause
clause) | PackedClause
clause <- CNF -> [PackedClause]
CNF.cnfClauses CNF
cnf] forall a. [a] -> [a] -> [a]
++
          [(Integer
1, [Int] -> PackedClause
SAT.packClause [Int
v]) | Int
v <- [Int]
vs]
      }
    , (Int, Int) -> IS2SATInfo
IS2SATInfo (Int
lb,Int
ub)
    )

newtype IS2SATInfo = IS2SATInfo (Int, Int)
  deriving (IS2SATInfo -> IS2SATInfo -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: IS2SATInfo -> IS2SATInfo -> Bool
$c/= :: IS2SATInfo -> IS2SATInfo -> Bool
== :: IS2SATInfo -> IS2SATInfo -> Bool
$c== :: IS2SATInfo -> IS2SATInfo -> Bool
Eq, Int -> IS2SATInfo -> ShowS
[IS2SATInfo] -> ShowS
IS2SATInfo -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [IS2SATInfo] -> ShowS
$cshowList :: [IS2SATInfo] -> ShowS
show :: IS2SATInfo -> String
$cshow :: IS2SATInfo -> String
showsPrec :: Int -> IS2SATInfo -> ShowS
$cshowsPrec :: Int -> IS2SATInfo -> ShowS
Show, ReadPrec [IS2SATInfo]
ReadPrec IS2SATInfo
Int -> ReadS IS2SATInfo
ReadS [IS2SATInfo]
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [IS2SATInfo]
$creadListPrec :: ReadPrec [IS2SATInfo]
readPrec :: ReadPrec IS2SATInfo
$creadPrec :: ReadPrec IS2SATInfo
readList :: ReadS [IS2SATInfo]
$creadList :: ReadS [IS2SATInfo]
readsPrec :: Int -> ReadS IS2SATInfo
$creadsPrec :: Int -> ReadS IS2SATInfo
Read)

instance Transformer IS2SATInfo where
  type Source IS2SATInfo = IntSet
  type Target IS2SATInfo = SAT.Model

instance ForwardTransformer IS2SATInfo where
  transformForward :: IS2SATInfo -> Source IS2SATInfo -> Target IS2SATInfo
transformForward (IS2SATInfo (Int
lb, Int
ub)) Source IS2SATInfo
indep_set = forall i e. (forall s. ST s (STUArray s i e)) -> UArray i e
runSTUArray forall a b. (a -> b) -> a -> b
$ do
    let n :: Int
n = Int
ub forall a. Num a => a -> a -> a
- Int
lb forall a. Num a => a -> a -> a
+ Int
1
    STUArray s Int Bool
a <- forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
(i, i) -> e -> m (a i e)
newArray (Int
1, Int
n) Bool
False
    forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (IntSet -> [Int]
IntSet.toList Source IS2SATInfo
indep_set) forall a b. (a -> b) -> a -> b
$ \Int
node -> do
      forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
a i e -> i -> e -> m ()
writeArray STUArray s Int Bool
a (Int
node forall a. Num a => a -> a -> a
- Int
lb forall a. Num a => a -> a -> a
+ Int
1) Bool
True
    forall (m :: * -> *) a. Monad m => a -> m a
return STUArray s Int Bool
a

instance BackwardTransformer IS2SATInfo where
  transformBackward :: IS2SATInfo -> Target IS2SATInfo -> Source IS2SATInfo
transformBackward (IS2SATInfo (Int
lb, Int
ub)) Target IS2SATInfo
m =
    [Int] -> IntSet
IntSet.fromList [Int
node | Int
node <- forall a. Ix a => (a, a) -> [a]
range (Int
lb, Int
ub), forall m. IModel m => m -> Int -> Bool
SAT.evalVar Target IS2SATInfo
m (Int
node forall a. Num a => a -> a -> a
- Int
lb forall a. Num a => a -> a -> a
+ Int
1)]

instance ObjValueTransformer IS2SATInfo where
  type SourceObjValue IS2SATInfo = Int
  type TargetObjValue IS2SATInfo = Integer

instance ObjValueForwardTransformer IS2SATInfo where
  transformObjValueForward :: IS2SATInfo
-> SourceObjValue IS2SATInfo -> TargetObjValue IS2SATInfo
transformObjValueForward (IS2SATInfo (Int
lb, Int
ub)) SourceObjValue IS2SATInfo
k = forall a b. (Integral a, Num b) => a -> b
fromIntegral forall a b. (a -> b) -> a -> b
$ (Int
ub forall a. Num a => a -> a -> a
- Int
lb forall a. Num a => a -> a -> a
+ Int
1) forall a. Num a => a -> a -> a
- SourceObjValue IS2SATInfo
k

instance ObjValueBackwardTransformer IS2SATInfo where
  transformObjValueBackward :: IS2SATInfo
-> TargetObjValue IS2SATInfo -> SourceObjValue IS2SATInfo
transformObjValueBackward (IS2SATInfo (Int
lb, Int
ub)) TargetObjValue IS2SATInfo
k = (Int
ub forall a. Num a => a -> a -> a
- Int
lb forall a. Num a => a -> a -> a
+ Int
1) forall a. Num a => a -> a -> a
- forall a b. (Integral a, Num b) => a -> b
fromIntegral TargetObjValue IS2SATInfo
k

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

pairs :: [a] -> [(a,a)]
pairs :: forall a. [a] -> [(a, a)]
pairs [] = []
pairs (a
x:[a]
xs) = [(a
x,a
x2) | a
x2 <- [a]
xs] forall a. [a] -> [a] -> [a]
++ forall a. [a] -> [(a, a)]
pairs [a]
xs

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