{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_HADDOCK show-extensions #-}
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE TypeFamilies #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  ToySolver.Converter.NAESAT
-- Copyright   :  (c) Masahiro Sakai 2018
-- License     :  BSD-style
--
-- Maintainer  :  masahiro.sakai@gmail.com
-- Stability   :  provisional
-- Portability :  non-portable
--
-- Not-All-Equal SAT problems.
--
-----------------------------------------------------------------------------
module ToySolver.Converter.NAESAT
  (
  -- * Definition of NAE (Not-All-Equall) SAT problems.
    NAESAT
  , evalNAESAT
  , NAEClause
  , evalNAEClause

  -- * Conversion with SAT problem
  , SAT2NAESATInfo (..)
  , sat2naesat
  , NAESAT2SATInfo
  , naesat2sat

  -- * Conversion from general NAE-SAT to NAE-k-SAT
  , NAESAT2NAEKSATInfo (..)
  , naesat2naeksat

  -- ** NAE-SAT to MAX-2-SAT
  , NAESAT2Max2SATInfo
  , naesat2max2sat
  , NAE3SAT2Max2SATInfo
  , nae3sat2max2sat
  ) where

import Control.Monad.State.Strict
import Data.Array.Unboxed
import qualified Data.IntMap as IntMap
import qualified Data.Vector.Generic as VG
import qualified Data.Vector.Unboxed as VU
import ToySolver.Converter.Base
import qualified ToySolver.FileFormat.CNF as CNF
import qualified ToySolver.SAT.Types as SAT

type NAESAT = (Int, [NAEClause])

evalNAESAT :: SAT.IModel m => m -> NAESAT -> Bool
evalNAESAT :: m -> NAESAT -> Bool
evalNAESAT m
m (Int
_,[NAEClause]
cs) = (NAEClause -> Bool) -> [NAEClause] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (m -> NAEClause -> Bool
forall m. IModel m => m -> NAEClause -> Bool
evalNAEClause m
m) [NAEClause]
cs

type NAEClause = VU.Vector SAT.PackedLit

evalNAEClause :: SAT.IModel m => m -> NAEClause -> Bool
evalNAEClause :: m -> NAEClause -> Bool
evalNAEClause m
m NAEClause
c =
  (PackedLit -> Bool) -> NAEClause -> Bool
forall (v :: * -> *) a. Vector v a => (a -> Bool) -> v a -> Bool
VG.any (m -> Int -> Bool
forall m. IModel m => m -> Int -> Bool
SAT.evalLit m
m (Int -> Bool) -> (PackedLit -> Int) -> PackedLit -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PackedLit -> Int
SAT.unpackLit) NAEClause
c Bool -> Bool -> Bool
&& (PackedLit -> Bool) -> NAEClause -> Bool
forall (v :: * -> *) a. Vector v a => (a -> Bool) -> v a -> Bool
VG.any (Bool -> Bool
not (Bool -> Bool) -> (PackedLit -> Bool) -> PackedLit -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m -> Int -> Bool
forall m. IModel m => m -> Int -> Bool
SAT.evalLit m
m (Int -> Bool) -> (PackedLit -> Int) -> PackedLit -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PackedLit -> Int
SAT.unpackLit) NAEClause
c

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

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

-- | Convert a CNF formula φ to an equisatifiable NAE-SAT formula ψ,
-- together with a 'SAT2NAESATInfo'
sat2naesat :: CNF.CNF -> (NAESAT, SAT2NAESATInfo)
sat2naesat :: CNF -> (NAESAT, SAT2NAESATInfo)
sat2naesat CNF
cnf = (NAESAT
ret, Int -> SAT2NAESATInfo
SAT2NAESATInfo Int
z)
  where
    z :: Int
z = CNF -> Int
CNF.cnfNumVars CNF
cnf Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1
    ret :: NAESAT
ret =
      ( CNF -> Int
CNF.cnfNumVars CNF
cnf Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1
      , [NAEClause -> PackedLit -> NAEClause
forall (v :: * -> *) a. Vector v a => v a -> a -> v a
VG.snoc NAEClause
clause (Int -> PackedLit
SAT.packLit Int
z) | NAEClause
clause <- CNF -> [NAEClause]
CNF.cnfClauses CNF
cnf]
      )

instance Transformer SAT2NAESATInfo where
  type Source SAT2NAESATInfo = SAT.Model
  type Target SAT2NAESATInfo = SAT.Model

instance ForwardTransformer SAT2NAESATInfo where
  transformForward :: SAT2NAESATInfo -> Source SAT2NAESATInfo -> Target SAT2NAESATInfo
transformForward (SAT2NAESATInfo Int
z) Source SAT2NAESATInfo
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
1,Int
z) ([(Int, Bool)] -> UArray Int Bool)
-> [(Int, Bool)] -> UArray Int Bool
forall a b. (a -> b) -> a -> b
$ (Int
z,Bool
False) (Int, Bool) -> [(Int, Bool)] -> [(Int, Bool)]
forall a. a -> [a] -> [a]
: UArray Int Bool -> [(Int, Bool)]
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> [(i, e)]
assocs UArray Int Bool
Source SAT2NAESATInfo
m

instance BackwardTransformer SAT2NAESATInfo where
  transformBackward :: SAT2NAESATInfo -> Target SAT2NAESATInfo -> Source SAT2NAESATInfo
transformBackward (SAT2NAESATInfo Int
z) Target SAT2NAESATInfo
m =
    Int -> UArray Int Bool -> UArray Int Bool
SAT.restrictModel (Int
z Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) (UArray Int Bool -> UArray Int Bool)
-> UArray Int Bool -> UArray Int Bool
forall a b. (a -> b) -> a -> b
$
      if UArray Int Bool -> Int -> Bool
forall m. IModel m => m -> Int -> Bool
SAT.evalVar UArray Int Bool
Target SAT2NAESATInfo
m Int
z then (Bool -> Bool) -> UArray Int Bool -> UArray Int Bool
forall (a :: * -> * -> *) e' e i.
(IArray a e', IArray a e, Ix i) =>
(e' -> e) -> a i e' -> a i e
amap Bool -> Bool
not UArray Int Bool
Target SAT2NAESATInfo
m else UArray Int Bool
Target SAT2NAESATInfo
m

-- | Information of 'naesat2sat' conversion
type NAESAT2SATInfo = IdentityTransformer SAT.Model

-- | Convert a NAE-SAT formula φ to an equisatifiable CNF formula ψ,
-- together with a 'NAESAT2SATInfo'
naesat2sat :: NAESAT -> (CNF.CNF, NAESAT2SATInfo)
naesat2sat :: NAESAT -> (CNF, NAESAT2SATInfo)
naesat2sat (Int
n,[NAEClause]
cs) =
  ( CNF :: Int -> Int -> [NAEClause] -> CNF
CNF.CNF
    { cnfNumVars :: Int
CNF.cnfNumVars = Int
n
    , cnfNumClauses :: Int
CNF.cnfNumClauses = [NAEClause] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [NAEClause]
cs Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
2
    , cnfClauses :: [NAEClause]
CNF.cnfClauses = [[NAEClause]] -> [NAEClause]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[NAEClause
c, (PackedLit -> PackedLit) -> NAEClause -> NAEClause
forall (v :: * -> *) a b.
(Vector v a, Vector v b) =>
(a -> b) -> v a -> v b
VG.map PackedLit -> PackedLit
forall a. Num a => a -> a
negate NAEClause
c] | NAEClause
c <- [NAEClause]
cs]
    }
  , NAESAT2SATInfo
forall a. IdentityTransformer a
IdentityTransformer
  )

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

-- Information of 'naesat2naeksta' conversion
data NAESAT2NAEKSATInfo = NAESAT2NAEKSATInfo !Int !Int [(SAT.Var, NAEClause, NAEClause)]
  deriving (NAESAT2NAEKSATInfo -> NAESAT2NAEKSATInfo -> Bool
(NAESAT2NAEKSATInfo -> NAESAT2NAEKSATInfo -> Bool)
-> (NAESAT2NAEKSATInfo -> NAESAT2NAEKSATInfo -> Bool)
-> Eq NAESAT2NAEKSATInfo
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: NAESAT2NAEKSATInfo -> NAESAT2NAEKSATInfo -> Bool
$c/= :: NAESAT2NAEKSATInfo -> NAESAT2NAEKSATInfo -> Bool
== :: NAESAT2NAEKSATInfo -> NAESAT2NAEKSATInfo -> Bool
$c== :: NAESAT2NAEKSATInfo -> NAESAT2NAEKSATInfo -> Bool
Eq, Int -> NAESAT2NAEKSATInfo -> ShowS
[NAESAT2NAEKSATInfo] -> ShowS
NAESAT2NAEKSATInfo -> String
(Int -> NAESAT2NAEKSATInfo -> ShowS)
-> (NAESAT2NAEKSATInfo -> String)
-> ([NAESAT2NAEKSATInfo] -> ShowS)
-> Show NAESAT2NAEKSATInfo
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [NAESAT2NAEKSATInfo] -> ShowS
$cshowList :: [NAESAT2NAEKSATInfo] -> ShowS
show :: NAESAT2NAEKSATInfo -> String
$cshow :: NAESAT2NAEKSATInfo -> String
showsPrec :: Int -> NAESAT2NAEKSATInfo -> ShowS
$cshowsPrec :: Int -> NAESAT2NAEKSATInfo -> ShowS
Show, ReadPrec [NAESAT2NAEKSATInfo]
ReadPrec NAESAT2NAEKSATInfo
Int -> ReadS NAESAT2NAEKSATInfo
ReadS [NAESAT2NAEKSATInfo]
(Int -> ReadS NAESAT2NAEKSATInfo)
-> ReadS [NAESAT2NAEKSATInfo]
-> ReadPrec NAESAT2NAEKSATInfo
-> ReadPrec [NAESAT2NAEKSATInfo]
-> Read NAESAT2NAEKSATInfo
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [NAESAT2NAEKSATInfo]
$creadListPrec :: ReadPrec [NAESAT2NAEKSATInfo]
readPrec :: ReadPrec NAESAT2NAEKSATInfo
$creadPrec :: ReadPrec NAESAT2NAEKSATInfo
readList :: ReadS [NAESAT2NAEKSATInfo]
$creadList :: ReadS [NAESAT2NAEKSATInfo]
readsPrec :: Int -> ReadS NAESAT2NAEKSATInfo
$creadsPrec :: Int -> ReadS NAESAT2NAEKSATInfo
Read)

naesat2naeksat :: Int -> NAESAT -> (NAESAT, NAESAT2NAEKSATInfo)
naesat2naeksat :: Int -> NAESAT -> (NAESAT, NAESAT2NAEKSATInfo)
naesat2naeksat Int
k NAESAT
_ | Int
k Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
3 = String -> (NAESAT, NAESAT2NAEKSATInfo)
forall a. HasCallStack => String -> a
error String
"naesat2naeksat: k must be >=3"
naesat2naeksat Int
k (Int
n,[NAEClause]
cs) = ((Int
n', [NAEClause]
cs'), Int -> Int -> [(Int, NAEClause, NAEClause)] -> NAESAT2NAEKSATInfo
NAESAT2NAEKSATInfo Int
n Int
n' ([(Int, NAEClause, NAEClause)] -> [(Int, NAEClause, NAEClause)]
forall a. [a] -> [a]
reverse [(Int, NAEClause, NAEClause)]
table))
  where
    ([NAEClause]
cs',(Int
n',[(Int, NAEClause, NAEClause)]
table)) = (State (Int, [(Int, NAEClause, NAEClause)]) [NAEClause]
 -> (Int, [(Int, NAEClause, NAEClause)])
 -> ([NAEClause], (Int, [(Int, NAEClause, NAEClause)])))
-> (Int, [(Int, NAEClause, NAEClause)])
-> State (Int, [(Int, NAEClause, NAEClause)]) [NAEClause]
-> ([NAEClause], (Int, [(Int, NAEClause, NAEClause)]))
forall a b c. (a -> b -> c) -> b -> a -> c
flip State (Int, [(Int, NAEClause, NAEClause)]) [NAEClause]
-> (Int, [(Int, NAEClause, NAEClause)])
-> ([NAEClause], (Int, [(Int, NAEClause, NAEClause)]))
forall s a. State s a -> s -> (a, s)
runState (Int
n,[]) (State (Int, [(Int, NAEClause, NAEClause)]) [NAEClause]
 -> ([NAEClause], (Int, [(Int, NAEClause, NAEClause)])))
-> State (Int, [(Int, NAEClause, NAEClause)]) [NAEClause]
-> ([NAEClause], (Int, [(Int, NAEClause, NAEClause)]))
forall a b. (a -> b) -> a -> b
$ do
      ([[NAEClause]] -> [NAEClause])
-> StateT
     (Int, [(Int, NAEClause, NAEClause)]) Identity [[NAEClause]]
-> State (Int, [(Int, NAEClause, NAEClause)]) [NAEClause]
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM [[NAEClause]] -> [NAEClause]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (StateT (Int, [(Int, NAEClause, NAEClause)]) Identity [[NAEClause]]
 -> State (Int, [(Int, NAEClause, NAEClause)]) [NAEClause])
-> StateT
     (Int, [(Int, NAEClause, NAEClause)]) Identity [[NAEClause]]
-> State (Int, [(Int, NAEClause, NAEClause)]) [NAEClause]
forall a b. (a -> b) -> a -> b
$ [NAEClause]
-> (NAEClause
    -> State (Int, [(Int, NAEClause, NAEClause)]) [NAEClause])
-> StateT
     (Int, [(Int, NAEClause, NAEClause)]) Identity [[NAEClause]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [NAEClause]
cs ((NAEClause
  -> State (Int, [(Int, NAEClause, NAEClause)]) [NAEClause])
 -> StateT
      (Int, [(Int, NAEClause, NAEClause)]) Identity [[NAEClause]])
-> (NAEClause
    -> State (Int, [(Int, NAEClause, NAEClause)]) [NAEClause])
-> StateT
     (Int, [(Int, NAEClause, NAEClause)]) Identity [[NAEClause]]
forall a b. (a -> b) -> a -> b
$ \NAEClause
c -> do
        let go :: NAEClause
-> [NAEClause]
-> State (Int, [(Int, NAEClause, NAEClause)]) [NAEClause]
go NAEClause
c' [NAEClause]
r =
              if NAEClause -> Int
forall (v :: * -> *) a. Vector v a => v a -> Int
VG.length NAEClause
c' Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
k then do
                [NAEClause]
-> State (Int, [(Int, NAEClause, NAEClause)]) [NAEClause]
forall (m :: * -> *) a. Monad m => a -> m a
return  ([NAEClause]
 -> State (Int, [(Int, NAEClause, NAEClause)]) [NAEClause])
-> [NAEClause]
-> State (Int, [(Int, NAEClause, NAEClause)]) [NAEClause]
forall a b. (a -> b) -> a -> b
$ [NAEClause] -> [NAEClause]
forall a. [a] -> [a]
reverse (NAEClause
c' NAEClause -> [NAEClause] -> [NAEClause]
forall a. a -> [a] -> [a]
: [NAEClause]
r)
              else do
                let (NAEClause
cs1, NAEClause
cs2) = Int -> NAEClause -> (NAEClause, NAEClause)
forall (v :: * -> *) a. Vector v a => Int -> v a -> (v a, v a)
VG.splitAt (Int
k Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) NAEClause
c'
                (Int
i, [(Int, NAEClause, NAEClause)]
tbl) <- StateT
  (Int, [(Int, NAEClause, NAEClause)])
  Identity
  (Int, [(Int, NAEClause, NAEClause)])
forall s (m :: * -> *). MonadState s m => m s
get
                let w :: Int
w = Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1
                Int
-> StateT (Int, [(Int, NAEClause, NAEClause)]) Identity ()
-> StateT (Int, [(Int, NAEClause, NAEClause)]) Identity ()
seq Int
w (StateT (Int, [(Int, NAEClause, NAEClause)]) Identity ()
 -> StateT (Int, [(Int, NAEClause, NAEClause)]) Identity ())
-> StateT (Int, [(Int, NAEClause, NAEClause)]) Identity ()
-> StateT (Int, [(Int, NAEClause, NAEClause)]) Identity ()
forall a b. (a -> b) -> a -> b
$ (Int, [(Int, NAEClause, NAEClause)])
-> StateT (Int, [(Int, NAEClause, NAEClause)]) Identity ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Int
w, (Int
w,NAEClause
cs1,NAEClause
cs2) (Int, NAEClause, NAEClause)
-> [(Int, NAEClause, NAEClause)] -> [(Int, NAEClause, NAEClause)]
forall a. a -> [a] -> [a]
: [(Int, NAEClause, NAEClause)]
tbl)
                NAEClause
-> [NAEClause]
-> State (Int, [(Int, NAEClause, NAEClause)]) [NAEClause]
go (PackedLit -> NAEClause -> NAEClause
forall (v :: * -> *) a. Vector v a => a -> v a -> v a
VG.cons (Int -> PackedLit
SAT.packLit (- Int
w)) NAEClause
cs2) (NAEClause -> PackedLit -> NAEClause
forall (v :: * -> *) a. Vector v a => v a -> a -> v a
VG.snoc NAEClause
cs1 (Int -> PackedLit
SAT.packLit Int
w) NAEClause -> [NAEClause] -> [NAEClause]
forall a. a -> [a] -> [a]
: [NAEClause]
r)
        NAEClause
-> [NAEClause]
-> State (Int, [(Int, NAEClause, NAEClause)]) [NAEClause]
go NAEClause
c []

instance Transformer NAESAT2NAEKSATInfo where
  type Source NAESAT2NAEKSATInfo = SAT.Model
  type Target NAESAT2NAEKSATInfo = SAT.Model

instance ForwardTransformer NAESAT2NAEKSATInfo where
  transformForward :: NAESAT2NAEKSATInfo
-> Source NAESAT2NAEKSATInfo -> Target NAESAT2NAEKSATInfo
transformForward (NAESAT2NAEKSATInfo Int
_n1 Int
n2 [(Int, NAEClause, NAEClause)]
table) Source NAESAT2NAEKSATInfo
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
1,Int
n2) (IntMap Bool -> [(Int, NAEClause, NAEClause)] -> [(Int, Bool)]
forall (v :: * -> *) (v :: * -> *).
(Vector v PackedLit, Vector v PackedLit) =>
IntMap Bool -> [(Int, v PackedLit, v PackedLit)] -> [(Int, Bool)]
go ([(Int, Bool)] -> IntMap Bool
forall a. [(Int, a)] -> IntMap a
IntMap.fromList (UArray Int Bool -> [(Int, Bool)]
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> [(i, e)]
assocs UArray Int Bool
Source NAESAT2NAEKSATInfo
m)) [(Int, NAEClause, NAEClause)]
table)
    where
      go :: IntMap Bool -> [(Int, v PackedLit, v PackedLit)] -> [(Int, Bool)]
go IntMap Bool
im [] = IntMap Bool -> [(Int, Bool)]
forall a. IntMap a -> [(Int, a)]
IntMap.toList IntMap Bool
im
      go IntMap Bool
im ((Int
w,v PackedLit
cs1,v PackedLit
cs2) : [(Int, v PackedLit, v PackedLit)]
tbl) = IntMap Bool -> [(Int, v PackedLit, v PackedLit)] -> [(Int, Bool)]
go (Int -> Bool -> IntMap Bool -> IntMap Bool
forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert Int
w Bool
val IntMap Bool
im) [(Int, v PackedLit, v PackedLit)]
tbl
        where
          ev :: PackedLit -> Bool
ev PackedLit
x
            | PackedLit
x PackedLit -> PackedLit -> Bool
forall a. Ord a => a -> a -> Bool
> PackedLit
0     = IntMap Bool
im IntMap Bool -> Int -> Bool
forall a. IntMap a -> Int -> a
IntMap.! (PackedLit -> Int
SAT.unpackLit PackedLit
x)
            | Bool
otherwise = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ IntMap Bool
im IntMap Bool -> Int -> Bool
forall a. IntMap a -> Int -> a
IntMap.! (- PackedLit -> Int
SAT.unpackLit PackedLit
x)
          needTrue :: Bool
needTrue  = (PackedLit -> Bool) -> v PackedLit -> Bool
forall (v :: * -> *) a. Vector v a => (a -> Bool) -> v a -> Bool
VG.all PackedLit -> Bool
ev v PackedLit
cs2 Bool -> Bool -> Bool
|| (PackedLit -> Bool) -> v PackedLit -> Bool
forall (v :: * -> *) a. Vector v a => (a -> Bool) -> v a -> Bool
VG.all (Bool -> Bool
not (Bool -> Bool) -> (PackedLit -> Bool) -> PackedLit -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PackedLit -> Bool
ev) v PackedLit
cs1
          needFalse :: Bool
needFalse = (PackedLit -> Bool) -> v PackedLit -> Bool
forall (v :: * -> *) a. Vector v a => (a -> Bool) -> v a -> Bool
VG.all PackedLit -> Bool
ev v PackedLit
cs1 Bool -> Bool -> Bool
|| (PackedLit -> Bool) -> v PackedLit -> Bool
forall (v :: * -> *) a. Vector v a => (a -> Bool) -> v a -> Bool
VG.all (Bool -> Bool
not (Bool -> Bool) -> (PackedLit -> Bool) -> PackedLit -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PackedLit -> Bool
ev) v PackedLit
cs2
          val :: Bool
val
            | Bool
needTrue Bool -> Bool -> Bool
&& Bool
needFalse = Bool
True -- error "naesat2naeksat_forward: invalid model"
            | Bool
needTrue  = Bool
True
            | Bool
needFalse = Bool
False
            | Bool
otherwise = Bool
False

instance BackwardTransformer NAESAT2NAEKSATInfo where
  transformBackward :: NAESAT2NAEKSATInfo
-> Target NAESAT2NAEKSATInfo -> Source NAESAT2NAEKSATInfo
transformBackward (NAESAT2NAEKSATInfo Int
n1 Int
_n2 [(Int, NAEClause, NAEClause)]
_table) = Int -> UArray Int Bool -> UArray Int Bool
SAT.restrictModel Int
n1

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

type NAESAT2Max2SATInfo = ComposedTransformer NAESAT2NAEKSATInfo NAE3SAT2Max2SATInfo

naesat2max2sat :: NAESAT -> ((CNF.WCNF, Integer), NAESAT2Max2SATInfo)
naesat2max2sat :: NAESAT -> ((WCNF, Integer), NAESAT2Max2SATInfo)
naesat2max2sat NAESAT
x = ((WCNF, Integer)
x2, (NAESAT2NAEKSATInfo -> NAESAT2SATInfo -> NAESAT2Max2SATInfo
forall a b. a -> b -> ComposedTransformer a b
ComposedTransformer NAESAT2NAEKSATInfo
info1 NAESAT2SATInfo
info2))
  where
    (NAESAT
x1, NAESAT2NAEKSATInfo
info1) = Int -> NAESAT -> (NAESAT, NAESAT2NAEKSATInfo)
naesat2naeksat Int
3 NAESAT
x
    ((WCNF, Integer)
x2, NAESAT2SATInfo
info2) = NAESAT -> ((WCNF, Integer), NAESAT2SATInfo)
nae3sat2max2sat NAESAT
x1

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

type NAE3SAT2Max2SATInfo = IdentityTransformer SAT.Model

-- Original nae-sat problem is satisfiable iff MAX-2-SAT problem has solution with cost <=threshold.
nae3sat2max2sat :: NAESAT -> ((CNF.WCNF, Integer), NAE3SAT2Max2SATInfo)
nae3sat2max2sat :: NAESAT -> ((WCNF, Integer), NAESAT2SATInfo)
nae3sat2max2sat (Int
n,[NAEClause]
cs)
  | (NAEClause -> Bool) -> [NAEClause] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\NAEClause
c -> NAEClause -> Int
forall (v :: * -> *) a. Vector v a => v a -> Int
VG.length NAEClause
c Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
2) [NAEClause]
cs =
      ( ( WCNF :: Int -> Int -> Integer -> [WeightedClause] -> WCNF
CNF.WCNF
          { wcnfTopCost :: Integer
CNF.wcnfTopCost = Integer
2
          , wcnfNumVars :: Int
CNF.wcnfNumVars = Int
n
          , wcnfClauses :: [WeightedClause]
CNF.wcnfClauses = [(Integer
1, Clause -> NAEClause
SAT.packClause [])]
          , wcnfNumClauses :: Int
CNF.wcnfNumClauses = Int
1
          }
        , Integer
0
        )
      , NAESAT2SATInfo
forall a. IdentityTransformer a
IdentityTransformer
      )
  | Bool
otherwise =
      ( ( WCNF :: Int -> Int -> Integer -> [WeightedClause] -> WCNF
CNF.WCNF
          { wcnfTopCost :: Integer
CNF.wcnfTopCost = Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
nc' Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1
          , wcnfNumVars :: Int
CNF.wcnfNumVars = Int
n
          , wcnfClauses :: [WeightedClause]
CNF.wcnfClauses = [WeightedClause]
cs'
          , wcnfNumClauses :: Int
CNF.wcnfNumClauses = Int
nc'
          }
        , Integer
t
        )
      , NAESAT2SATInfo
forall a. IdentityTransformer a
IdentityTransformer
      )
  where
    nc' :: Int
nc' = [WeightedClause] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [WeightedClause]
cs'
    ([WeightedClause]
cs', Integer
t) = (([WeightedClause], Integer)
 -> NAEClause -> ([WeightedClause], Integer))
-> ([WeightedClause], Integer)
-> [NAEClause]
-> ([WeightedClause], Integer)
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl ([WeightedClause], Integer)
-> NAEClause -> ([WeightedClause], Integer)
f ([],Integer
0) [NAEClause]
cs
      where
        f :: ([CNF.WeightedClause], Integer) -> NAEClause -> ([CNF.WeightedClause], Integer)
        f :: ([WeightedClause], Integer)
-> NAEClause -> ([WeightedClause], Integer)
f ([WeightedClause]
cs, !Integer
t) NAEClause
c =
          case NAEClause -> Clause
SAT.unpackClause NAEClause
c of
            []  -> String -> ([WeightedClause], Integer)
forall a. HasCallStack => String -> a
error String
"nae3sat2max2sat: should not happen"
            [Int
_] -> String -> ([WeightedClause], Integer)
forall a. HasCallStack => String -> a
error String
"nae3sat2max2sat: should not happen"
            [Int
_,Int
_] ->
                ( [(Integer
1, NAEClause
c), (Integer
1, (PackedLit -> PackedLit) -> NAEClause -> NAEClause
forall (v :: * -> *) a b.
(Vector v a, Vector v b) =>
(a -> b) -> v a -> v b
VG.map PackedLit -> PackedLit
forall a. Num a => a -> a
negate NAEClause
c)] [WeightedClause] -> [WeightedClause] -> [WeightedClause]
forall a. [a] -> [a] -> [a]
++ [WeightedClause]
cs
                , Integer
t
                )
            [Int
l0,Int
l1,Int
l2] ->
                ( [[WeightedClause]] -> [WeightedClause]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[(Integer
1, Clause -> NAEClause
SAT.packClause [Int
a,Int
b]), (Integer
1, Clause -> NAEClause
SAT.packClause [-Int
a,-Int
b])] | (Int
a,Int
b) <- [(Int
l0,Int
l1),(Int
l1,Int
l2),(Int
l2,Int
l0)]] [WeightedClause] -> [WeightedClause] -> [WeightedClause]
forall a. [a] -> [a] -> [a]
++ [WeightedClause]
cs
                , Integer
t Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1
                )
            Clause
_ -> String -> ([WeightedClause], Integer)
forall a. HasCallStack => String -> a
error String
"nae3sat2max2sat: cannot handle nae-clause of size >3"

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