{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_HADDOCK show-extensions #-}
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE TypeFamilies #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  ToySolver.Converter.SAT2MaxCut
-- Copyright   :  (c) Masahiro Sakai 2018
-- License     :  BSD-style
--
-- Maintainer  :  masahiro.sakai@gmail.com
-- Stability   :  provisional
-- Portability :  non-portable
--
-- http://www.cs.cornell.edu/courses/cs4820/2014sp/notes/reduction-maxcut.pdf
--
-----------------------------------------------------------------------------
module ToySolver.Converter.SAT2MaxCut
  (
  -- * SAT to MaxCut conversion
    SAT2MaxCutInfo
  , sat2maxcut

  -- * Low-level conversion

  -- ** NAE-SAT to MaxCut
  , NAESAT2MaxCutInfo
  , naesat2maxcut

  -- ** NAE-3-SAT to MaxCut
  , NAE3SAT2MaxCutInfo (..)
  , nae3sat2maxcut
  ) where

import Data.Array.Unboxed
import qualified Data.IntSet as IntSet
import qualified Data.Vector.Generic as VG
import qualified Data.Vector.Unboxed as VU

import qualified ToySolver.FileFormat.CNF as CNF
import ToySolver.Graph.Base
import qualified ToySolver.Graph.MaxCut as MaxCut
import qualified ToySolver.SAT.Types as SAT
import ToySolver.Converter.Base
import ToySolver.Converter.NAESAT (NAESAT)
import qualified ToySolver.Converter.NAESAT as NAESAT

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

type SAT2MaxCutInfo = ComposedTransformer NAESAT.SAT2NAESATInfo NAESAT2MaxCutInfo

sat2maxcut :: CNF.CNF -> ((MaxCut.Problem Integer, Integer), SAT2MaxCutInfo)
sat2maxcut :: CNF -> ((Problem Integer, Integer), SAT2MaxCutInfo)
sat2maxcut CNF
x = ((Problem Integer, Integer)
x2, (SAT2NAESATInfo -> NAESAT2MaxCutInfo -> SAT2MaxCutInfo
forall a b. a -> b -> ComposedTransformer a b
ComposedTransformer SAT2NAESATInfo
info1 NAESAT2MaxCutInfo
info2))
  where
    (NAESAT
x1, SAT2NAESATInfo
info1) = CNF -> (NAESAT, SAT2NAESATInfo)
NAESAT.sat2naesat CNF
x
    ((Problem Integer, Integer)
x2, NAESAT2MaxCutInfo
info2) = NAESAT -> ((Problem Integer, Integer), NAESAT2MaxCutInfo)
naesat2maxcut NAESAT
x1

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

type NAESAT2MaxCutInfo = ComposedTransformer NAESAT.NAESAT2NAEKSATInfo NAE3SAT2MaxCutInfo

naesat2maxcut :: NAESAT -> ((MaxCut.Problem Integer, Integer), NAESAT2MaxCutInfo)
naesat2maxcut :: NAESAT -> ((Problem Integer, Integer), NAESAT2MaxCutInfo)
naesat2maxcut NAESAT
x = ((Problem Integer, Integer)
x2, (NAESAT2NAEKSATInfo -> NAE3SAT2MaxCutInfo -> NAESAT2MaxCutInfo
forall a b. a -> b -> ComposedTransformer a b
ComposedTransformer NAESAT2NAEKSATInfo
info1 NAE3SAT2MaxCutInfo
info2))
  where
    (NAESAT
x1, NAESAT2NAEKSATInfo
info1) = Int -> NAESAT -> (NAESAT, NAESAT2NAEKSATInfo)
NAESAT.naesat2naeksat Int
3 NAESAT
x
    ((Problem Integer, Integer)
x2, NAE3SAT2MaxCutInfo
info2) = NAESAT -> ((Problem Integer, Integer), NAE3SAT2MaxCutInfo)
nae3sat2maxcut NAESAT
x1

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

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

-- Original nae-sat problem is satisfiable iff Max-Cut problem has solution with >=threshold.
nae3sat2maxcut :: NAESAT -> ((MaxCut.Problem Integer, Integer), NAE3SAT2MaxCutInfo)
nae3sat2maxcut :: NAESAT -> ((Problem Integer, Integer), NAE3SAT2MaxCutInfo)
nae3sat2maxcut (Int
n,[NAEClause]
cs)
  | (Vector Int -> Bool) -> [Vector Int] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\Vector Int
c -> Vector Int -> Int
forall (v :: * -> *) a. Vector v a => v a -> Int
VG.length Vector Int
c Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
2) [Vector Int]
cs' =
      ( (Int -> [(Int, Int, Integer)] -> Problem Integer
forall a. Int -> [(Int, Int, a)] -> EdgeLabeledGraph a
graphFromUnorderedEdges (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
*Int
2) [], Integer
1)
      , NAE3SAT2MaxCutInfo
NAE3SAT2MaxCutInfo
      )
  | Bool
otherwise =
      ( ( (Integer -> Integer -> Integer)
-> Int -> [(Int, Int, Integer)] -> Problem Integer
forall a.
(a -> a -> a) -> Int -> [(Int, Int, a)] -> EdgeLabeledGraph a
graphFromUnorderedEdgesWith Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
(+) (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
*Int
2) ([(Int, Int, Integer)]
variableEdges [(Int, Int, Integer)]
-> [(Int, Int, Integer)] -> [(Int, Int, Integer)]
forall a. [a] -> [a] -> [a]
++ [(Int, Int, Integer)]
clauseEdges)
        , Integer
bigM Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
clauseEdgesObjMax
        )
      , NAE3SAT2MaxCutInfo
NAE3SAT2MaxCutInfo
      )
  where
    cs' :: [Vector Int]
cs' = (NAEClause -> Vector Int) -> [NAEClause] -> [Vector Int]
forall a b. (a -> b) -> [a] -> [b]
map ([Int] -> Vector Int
forall (v :: * -> *) a. Vector v a => [a] -> v a
VG.fromList ([Int] -> Vector Int)
-> (NAEClause -> [Int]) -> NAEClause -> Vector Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IntSet -> [Int]
IntSet.toList (IntSet -> [Int]) -> (NAEClause -> IntSet) -> NAEClause -> [Int]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Int] -> IntSet
IntSet.fromList ([Int] -> IntSet) -> (NAEClause -> [Int]) -> NAEClause -> IntSet
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NAEClause -> [Int]
SAT.unpackClause) [NAEClause]
cs

    bigM :: Integer
bigM = Integer
clauseEdgesObjMax Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1

    ([(Int, Int, Integer)]
clauseEdges, Integer
clauseEdgesObjMax) = (([(Int, Int, Integer)], Integer)
 -> Vector Int -> ([(Int, Int, Integer)], Integer))
-> ([(Int, Int, Integer)], Integer)
-> [Vector Int]
-> ([(Int, Int, Integer)], Integer)
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl ([(Int, Int, Integer)], Integer)
-> Vector Int -> ([(Int, Int, Integer)], Integer)
f ([],Integer
0) [Vector Int]
cs'
      where
        f :: ([(Int,Int,Integer)], Integer) -> VU.Vector SAT.Lit -> ([(Int,Int,Integer)], Integer)
        f :: ([(Int, Int, Integer)], Integer)
-> Vector Int -> ([(Int, Int, Integer)], Integer)
f ([(Int, Int, Integer)]
clauseEdges', !Integer
clauseEdgesObjMax') Vector Int
c =
          case (Int -> Int) -> [Int] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map Int -> Int
encodeLit (Vector Int -> [Int]
forall (v :: * -> *) a. Vector v a => v a -> [a]
VG.toList Vector Int
c) of
            []  -> String -> ([(Int, Int, Integer)], Integer)
forall a. HasCallStack => String -> a
error String
"nae3sat2maxcut: should not happen"
            [Int
_] -> String -> ([(Int, Int, Integer)], Integer)
forall a. HasCallStack => String -> a
error String
"nae3sat2maxcut: should not happen"
            [Int
v0,Int
v1]    -> ([(Int
v0, Int
v1, Integer
1)] [(Int, Int, Integer)]
-> [(Int, Int, Integer)] -> [(Int, Int, Integer)]
forall a. [a] -> [a] -> [a]
++ [(Int, Int, Integer)]
clauseEdges', Integer
clauseEdgesObjMax' Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1)
            [Int
v0,Int
v1,Int
v2] -> ([(Int
v0, Int
v1, Integer
1), (Int
v1, Int
v2, Integer
1), (Int
v2, Int
v0, Integer
1)] [(Int, Int, Integer)]
-> [(Int, Int, Integer)] -> [(Int, Int, Integer)]
forall a. [a] -> [a] -> [a]
++ [(Int, Int, Integer)]
clauseEdges', Integer
clauseEdgesObjMax' Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
2)
            [Int]
_ -> String -> ([(Int, Int, Integer)], Integer)
forall a. HasCallStack => String -> a
error String
"nae3sat2maxcut: cannot handle nae-clause of size >3"

    variableEdges :: [(Int, Int, Integer)]
variableEdges = [(Int -> Int
encodeLit Int
v, Int -> Int
encodeLit (-Int
v), Integer
bigM) | Int
v <- [Int
1..Int
n]]

instance Transformer NAE3SAT2MaxCutInfo where
  type Source NAE3SAT2MaxCutInfo = SAT.Model
  type Target NAE3SAT2MaxCutInfo = MaxCut.Solution

instance ForwardTransformer NAE3SAT2MaxCutInfo where
  transformForward :: NAE3SAT2MaxCutInfo
-> Source NAE3SAT2MaxCutInfo -> Target NAE3SAT2MaxCutInfo
transformForward NAE3SAT2MaxCutInfo
_ Source NAE3SAT2MaxCutInfo
m = (Int, Int) -> [(Int, Bool)] -> UArray Int Bool
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
(i, i) -> [(i, e)] -> a i e
array (Int
0,Int
2Int -> Int -> Int
forall a. Num a => a -> a -> a
*Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) ([(Int, Bool)] -> UArray Int Bool)
-> [(Int, Bool)] -> UArray Int Bool
forall a b. (a -> b) -> a -> b
$ do
    Int
v <- [Int
1..Int
n]
    let val :: Bool
val = UArray Int Bool -> Int -> Bool
forall a. IModel a => a -> Int -> Bool
SAT.evalVar UArray Int Bool
Source NAE3SAT2MaxCutInfo
m Int
v
    [(Int -> Int
encodeLit Int
v, Bool
val), (Int -> Int
encodeLit (-Int
v), Bool -> Bool
not Bool
val)]
    where
      (Int
_,Int
n) = UArray Int Bool -> (Int, Int)
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> (i, i)
bounds UArray Int Bool
Source NAE3SAT2MaxCutInfo
m

instance BackwardTransformer NAE3SAT2MaxCutInfo where
  transformBackward :: NAE3SAT2MaxCutInfo
-> Target NAE3SAT2MaxCutInfo -> Source NAE3SAT2MaxCutInfo
transformBackward NAE3SAT2MaxCutInfo
_ Target NAE3SAT2MaxCutInfo
sol = (Int, Int) -> [(Int, Bool)] -> UArray Int Bool
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
(i, i) -> [(i, e)] -> a i e
array (Int
1,Int
n) [(Int
v, UArray Int Bool
Target NAE3SAT2MaxCutInfo
sol UArray Int Bool -> Int -> Bool
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> i -> e
! Int -> Int
encodeLit Int
v) | Int
v <- [Int
1..Int
n]]
    where
      (Int
_,Int
n') = UArray Int Bool -> (Int, Int)
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> (i, i)
bounds UArray Int Bool
Target NAE3SAT2MaxCutInfo
sol
      n :: Int
n = (Int
n'Int -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
2

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

encodeLit :: SAT.Lit -> Int
encodeLit :: Int -> Int
encodeLit Int
l =
  if Int
l Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0
  then (Int
lInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)Int -> Int -> Int
forall a. Num a => a -> a -> a
*Int
2
  else (-Int
lInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)Int -> Int -> Int
forall a. Num a => a -> a -> a
*Int
2Int -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1

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