{-# 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, (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, (forall a b. a -> b -> ComposedTransformer a b
ComposedTransformer NAESAT2NAEKSATInfo
info1 NAE3SAT2MaxCutInfo
info2))
  where
    (NAESAT
x1, NAESAT2NAEKSATInfo
info1) = Lit -> NAESAT -> (NAESAT, NAESAT2NAEKSATInfo)
NAESAT.naesat2naeksat Lit
3 NAESAT
x
    ((Problem Integer, Integer)
x2, NAE3SAT2MaxCutInfo
info2) = NAESAT -> ((Problem Integer, Integer), NAE3SAT2MaxCutInfo)
nae3sat2maxcut NAESAT
x1

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

data NAE3SAT2MaxCutInfo = NAE3SAT2MaxCutInfo
  deriving (NAE3SAT2MaxCutInfo -> NAE3SAT2MaxCutInfo -> Bool
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, Lit -> NAE3SAT2MaxCutInfo -> ShowS
[NAE3SAT2MaxCutInfo] -> ShowS
NAE3SAT2MaxCutInfo -> String
forall a.
(Lit -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [NAE3SAT2MaxCutInfo] -> ShowS
$cshowList :: [NAE3SAT2MaxCutInfo] -> ShowS
show :: NAE3SAT2MaxCutInfo -> String
$cshow :: NAE3SAT2MaxCutInfo -> String
showsPrec :: Lit -> NAE3SAT2MaxCutInfo -> ShowS
$cshowsPrec :: Lit -> NAE3SAT2MaxCutInfo -> ShowS
Show, ReadPrec [NAE3SAT2MaxCutInfo]
ReadPrec NAE3SAT2MaxCutInfo
Lit -> ReadS NAE3SAT2MaxCutInfo
ReadS [NAE3SAT2MaxCutInfo]
forall a.
(Lit -> 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 :: Lit -> ReadS NAE3SAT2MaxCutInfo
$creadsPrec :: Lit -> 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 (Lit
n,[NAEClause]
cs)
  | forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\Vector Lit
c -> forall (v :: * -> *) a. Vector v a => v a -> Lit
VG.length Vector Lit
c forall a. Ord a => a -> a -> Bool
< Lit
2) [Vector Lit]
cs' =
      ( (forall a. Lit -> [(Lit, Lit, a)] -> EdgeLabeledGraph a
graphFromUnorderedEdges (Lit
nforall a. Num a => a -> a -> a
*Lit
2) [], Integer
1)
      , NAE3SAT2MaxCutInfo
NAE3SAT2MaxCutInfo
      )
  | Bool
otherwise =
      ( ( forall a.
(a -> a -> a) -> Lit -> [(Lit, Lit, a)] -> EdgeLabeledGraph a
graphFromUnorderedEdgesWith forall a. Num a => a -> a -> a
(+) (Lit
nforall a. Num a => a -> a -> a
*Lit
2) ([(Lit, Lit, Integer)]
variableEdges forall a. [a] -> [a] -> [a]
++ [(Lit, Lit, Integer)]
clauseEdges)
        , Integer
bigM forall a. Num a => a -> a -> a
* forall a b. (Integral a, Num b) => a -> b
fromIntegral Lit
n forall a. Num a => a -> a -> a
+ Integer
clauseEdgesObjMax
        )
      , NAE3SAT2MaxCutInfo
NAE3SAT2MaxCutInfo
      )
  where
    cs' :: [Vector Lit]
cs' = forall a b. (a -> b) -> [a] -> [b]
map (forall (v :: * -> *) a. Vector v a => [a] -> v a
VG.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. IntSet -> [Lit]
IntSet.toList forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Lit] -> IntSet
IntSet.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. NAEClause -> [Lit]
SAT.unpackClause) [NAEClause]
cs

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

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

    variableEdges :: [(Lit, Lit, Integer)]
variableEdges = [(Lit -> Lit
encodeLit Lit
v, Lit -> Lit
encodeLit (-Lit
v), Integer
bigM) | Lit
v <- [Lit
1..Lit
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 = forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
(i, i) -> [(i, e)] -> a i e
array (Lit
0,Lit
2forall a. Num a => a -> a -> a
*Lit
nforall a. Num a => a -> a -> a
-Lit
1) forall a b. (a -> b) -> a -> b
$ do
    Lit
v <- [Lit
1..Lit
n]
    let val :: Bool
val = forall a. IModel a => a -> Lit -> Bool
SAT.evalVar Source NAE3SAT2MaxCutInfo
m Lit
v
    [(Lit -> Lit
encodeLit Lit
v, Bool
val), (Lit -> Lit
encodeLit (-Lit
v), Bool -> Bool
not Bool
val)]
    where
      (Lit
_,Lit
n) = forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> (i, i)
bounds Source NAE3SAT2MaxCutInfo
m

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

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

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

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