{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_HADDOCK show-extensions #-}
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE OverloadedStrings #-}
{-# 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
import Control.Monad.State.Strict
import qualified Data.Aeson as J
import Data.Aeson ((.=), (.:))
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 ToySolver.Internal.JSON
import qualified ToySolver.FileFormat.CNF as CNF
import ToySolver.SAT.Internal.JSON
import qualified ToySolver.SAT.Types as SAT

type NAESAT = (Int, [NAEClause])

evalNAESAT :: SAT.IModel m => m -> NAESAT -> Bool
evalNAESAT :: forall m. IModel m => m -> NAESAT -> Bool
evalNAESAT m
m (Lit
_,[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 :: forall m. IModel m => 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 -> Lit -> Bool
forall m. IModel m => m -> Lit -> Bool
SAT.evalLit m
m (Lit -> Bool) -> (PackedLit -> Lit) -> PackedLit -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PackedLit -> Lit
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 -> Lit -> Bool
forall m. IModel m => m -> Lit -> Bool
SAT.evalLit m
m (Lit -> Bool) -> (PackedLit -> Lit) -> PackedLit -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PackedLit -> Lit
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
$c== :: SAT2NAESATInfo -> SAT2NAESATInfo -> Bool
== :: SAT2NAESATInfo -> SAT2NAESATInfo -> Bool
$c/= :: SAT2NAESATInfo -> SAT2NAESATInfo -> Bool
/= :: SAT2NAESATInfo -> SAT2NAESATInfo -> Bool
Eq, Lit -> SAT2NAESATInfo -> ShowS
[SAT2NAESATInfo] -> ShowS
SAT2NAESATInfo -> String
(Lit -> SAT2NAESATInfo -> ShowS)
-> (SAT2NAESATInfo -> String)
-> ([SAT2NAESATInfo] -> ShowS)
-> Show SAT2NAESATInfo
forall a.
(Lit -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Lit -> SAT2NAESATInfo -> ShowS
showsPrec :: Lit -> SAT2NAESATInfo -> ShowS
$cshow :: SAT2NAESATInfo -> String
show :: SAT2NAESATInfo -> String
$cshowList :: [SAT2NAESATInfo] -> ShowS
showList :: [SAT2NAESATInfo] -> ShowS
Show, ReadPrec [SAT2NAESATInfo]
ReadPrec SAT2NAESATInfo
Lit -> ReadS SAT2NAESATInfo
ReadS [SAT2NAESATInfo]
(Lit -> ReadS SAT2NAESATInfo)
-> ReadS [SAT2NAESATInfo]
-> ReadPrec SAT2NAESATInfo
-> ReadPrec [SAT2NAESATInfo]
-> Read SAT2NAESATInfo
forall a.
(Lit -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
$creadsPrec :: Lit -> ReadS SAT2NAESATInfo
readsPrec :: Lit -> ReadS SAT2NAESATInfo
$creadList :: ReadS [SAT2NAESATInfo]
readList :: ReadS [SAT2NAESATInfo]
$creadPrec :: ReadPrec SAT2NAESATInfo
readPrec :: ReadPrec SAT2NAESATInfo
$creadListPrec :: ReadPrec [SAT2NAESATInfo]
readListPrec :: ReadPrec [SAT2NAESATInfo]
Read)

-- | Convert a CNF formula φ to an equisatisfiable NAE-SAT formula ψ,
-- together with a 'SAT2NAESATInfo'
sat2naesat :: CNF.CNF -> (NAESAT, SAT2NAESATInfo)
sat2naesat :: CNF -> (NAESAT, SAT2NAESATInfo)
sat2naesat CNF
cnf = (NAESAT
ret, Lit -> SAT2NAESATInfo
SAT2NAESATInfo Lit
z)
  where
    z :: Lit
z = CNF -> Lit
CNF.cnfNumVars CNF
cnf Lit -> Lit -> Lit
forall a. Num a => a -> a -> a
+ Lit
1
    ret :: NAESAT
ret =
      ( CNF -> Lit
CNF.cnfNumVars CNF
cnf Lit -> Lit -> Lit
forall a. Num a => a -> a -> a
+ Lit
1
      , [NAEClause -> PackedLit -> NAEClause
forall (v :: * -> *) a. Vector v a => v a -> a -> v a
VG.snoc NAEClause
clause (Lit -> PackedLit
SAT.packLit Lit
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 Lit
z) Source SAT2NAESATInfo
m = (Lit, Lit) -> [(Lit, Bool)] -> UArray Lit Bool
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
(i, i) -> [(i, e)] -> a i e
array (Lit
1,Lit
z) ([(Lit, Bool)] -> UArray Lit Bool)
-> [(Lit, Bool)] -> UArray Lit Bool
forall a b. (a -> b) -> a -> b
$ (Lit
z,Bool
False) (Lit, Bool) -> [(Lit, Bool)] -> [(Lit, Bool)]
forall a. a -> [a] -> [a]
: UArray Lit Bool -> [(Lit, Bool)]
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> [(i, e)]
assocs UArray Lit Bool
Source SAT2NAESATInfo
m

instance BackwardTransformer SAT2NAESATInfo where
  transformBackward :: SAT2NAESATInfo -> Target SAT2NAESATInfo -> Source SAT2NAESATInfo
transformBackward (SAT2NAESATInfo Lit
z) Target SAT2NAESATInfo
m =
    Lit -> UArray Lit Bool -> UArray Lit Bool
SAT.restrictModel (Lit
z Lit -> Lit -> Lit
forall a. Num a => a -> a -> a
- Lit
1) (UArray Lit Bool -> UArray Lit Bool)
-> UArray Lit Bool -> UArray Lit Bool
forall a b. (a -> b) -> a -> b
$
      if UArray Lit Bool -> Lit -> Bool
forall m. IModel m => m -> Lit -> Bool
SAT.evalVar UArray Lit Bool
Target SAT2NAESATInfo
m Lit
z then (Bool -> Bool) -> UArray Lit Bool -> UArray Lit 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 Lit Bool
Target SAT2NAESATInfo
m else UArray Lit Bool
Target SAT2NAESATInfo
m

instance J.ToJSON SAT2NAESATInfo where
  toJSON :: SAT2NAESATInfo -> Value
toJSON (SAT2NAESATInfo Lit
z) =
    [Pair] -> Value
J.object
    [ Key
"type" Key -> Value -> Pair
forall v. ToJSON v => Key -> v -> Pair
forall e kv v. (KeyValue e kv, ToJSON v) => Key -> v -> kv
.= (Value
"SAT2NAESATInfo" :: J.Value)
    , Key
"special_variable" Key -> Value -> Pair
forall v. ToJSON v => Key -> v -> Pair
forall e kv v. (KeyValue e kv, ToJSON v) => Key -> v -> kv
.= (Lit -> Value
forall a. IsString a => Lit -> a
jVarName Lit
z :: J.Value)
    ]

instance J.FromJSON SAT2NAESATInfo where
  parseJSON :: Value -> Parser SAT2NAESATInfo
parseJSON = String
-> (Object -> Parser SAT2NAESATInfo)
-> Value
-> Parser SAT2NAESATInfo
forall a. String -> (Object -> Parser a) -> Value -> Parser a
withTypedObject String
"SAT2NAESATInfo" ((Object -> Parser SAT2NAESATInfo)
 -> Value -> Parser SAT2NAESATInfo)
-> (Object -> Parser SAT2NAESATInfo)
-> Value
-> Parser SAT2NAESATInfo
forall a b. (a -> b) -> a -> b
$ \Object
obj -> do
    Lit
z <- Value -> Parser Lit
parseVarName (Value -> Parser Lit) -> Parser Value -> Parser Lit
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (Object
obj Object -> Key -> Parser Value
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"special_variable")
    SAT2NAESATInfo -> Parser SAT2NAESATInfo
forall a. a -> Parser a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SAT2NAESATInfo -> Parser SAT2NAESATInfo)
-> SAT2NAESATInfo -> Parser SAT2NAESATInfo
forall a b. (a -> b) -> a -> b
$ Lit -> SAT2NAESATInfo
SAT2NAESATInfo Lit
z

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

-- | Convert a NAE-SAT formula φ to an equisatisfiable CNF formula ψ,
-- together with a 'NAESAT2SATInfo'
naesat2sat :: NAESAT -> (CNF.CNF, NAESAT2SATInfo)
naesat2sat :: NAESAT -> (CNF, NAESAT2SATInfo)
naesat2sat (Lit
n,[NAEClause]
cs) =
  ( CNF.CNF
    { cnfNumVars :: Lit
CNF.cnfNumVars = Lit
n
    , cnfNumClauses :: Lit
CNF.cnfNumClauses = [NAEClause] -> Lit
forall a. [a] -> Lit
forall (t :: * -> *) a. Foldable t => t a -> Lit
length [NAEClause]
cs Lit -> Lit -> Lit
forall a. Num a => a -> a -> a
* Lit
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 'naesat2naeksat' 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
$c== :: NAESAT2NAEKSATInfo -> NAESAT2NAEKSATInfo -> Bool
== :: NAESAT2NAEKSATInfo -> NAESAT2NAEKSATInfo -> Bool
$c/= :: NAESAT2NAEKSATInfo -> NAESAT2NAEKSATInfo -> Bool
/= :: NAESAT2NAEKSATInfo -> NAESAT2NAEKSATInfo -> Bool
Eq, Lit -> NAESAT2NAEKSATInfo -> ShowS
[NAESAT2NAEKSATInfo] -> ShowS
NAESAT2NAEKSATInfo -> String
(Lit -> NAESAT2NAEKSATInfo -> ShowS)
-> (NAESAT2NAEKSATInfo -> String)
-> ([NAESAT2NAEKSATInfo] -> ShowS)
-> Show NAESAT2NAEKSATInfo
forall a.
(Lit -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Lit -> NAESAT2NAEKSATInfo -> ShowS
showsPrec :: Lit -> NAESAT2NAEKSATInfo -> ShowS
$cshow :: NAESAT2NAEKSATInfo -> String
show :: NAESAT2NAEKSATInfo -> String
$cshowList :: [NAESAT2NAEKSATInfo] -> ShowS
showList :: [NAESAT2NAEKSATInfo] -> ShowS
Show, ReadPrec [NAESAT2NAEKSATInfo]
ReadPrec NAESAT2NAEKSATInfo
Lit -> ReadS NAESAT2NAEKSATInfo
ReadS [NAESAT2NAEKSATInfo]
(Lit -> ReadS NAESAT2NAEKSATInfo)
-> ReadS [NAESAT2NAEKSATInfo]
-> ReadPrec NAESAT2NAEKSATInfo
-> ReadPrec [NAESAT2NAEKSATInfo]
-> Read NAESAT2NAEKSATInfo
forall a.
(Lit -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
$creadsPrec :: Lit -> ReadS NAESAT2NAEKSATInfo
readsPrec :: Lit -> ReadS NAESAT2NAEKSATInfo
$creadList :: ReadS [NAESAT2NAEKSATInfo]
readList :: ReadS [NAESAT2NAEKSATInfo]
$creadPrec :: ReadPrec NAESAT2NAEKSATInfo
readPrec :: ReadPrec NAESAT2NAEKSATInfo
$creadListPrec :: ReadPrec [NAESAT2NAEKSATInfo]
readListPrec :: ReadPrec [NAESAT2NAEKSATInfo]
Read)

naesat2naeksat :: Int -> NAESAT -> (NAESAT, NAESAT2NAEKSATInfo)
naesat2naeksat :: Lit -> NAESAT -> (NAESAT, NAESAT2NAEKSATInfo)
naesat2naeksat Lit
k NAESAT
_ | Lit
k Lit -> Lit -> Bool
forall a. Ord a => a -> a -> Bool
< Lit
3 = String -> (NAESAT, NAESAT2NAEKSATInfo)
forall a. HasCallStack => String -> a
error String
"naesat2naeksat: k must be >=3"
naesat2naeksat Lit
k (Lit
n,[NAEClause]
cs) = ((Lit
n', [NAEClause]
cs'), Lit -> Lit -> [(Lit, NAEClause, NAEClause)] -> NAESAT2NAEKSATInfo
NAESAT2NAEKSATInfo Lit
n Lit
n' ([(Lit, NAEClause, NAEClause)] -> [(Lit, NAEClause, NAEClause)]
forall a. [a] -> [a]
reverse [(Lit, NAEClause, NAEClause)]
table))
  where
    ([NAEClause]
cs',(Lit
n',[(Lit, NAEClause, NAEClause)]
table)) = (State (Lit, [(Lit, NAEClause, NAEClause)]) [NAEClause]
 -> (Lit, [(Lit, NAEClause, NAEClause)])
 -> ([NAEClause], (Lit, [(Lit, NAEClause, NAEClause)])))
-> (Lit, [(Lit, NAEClause, NAEClause)])
-> State (Lit, [(Lit, NAEClause, NAEClause)]) [NAEClause]
-> ([NAEClause], (Lit, [(Lit, NAEClause, NAEClause)]))
forall a b c. (a -> b -> c) -> b -> a -> c
flip State (Lit, [(Lit, NAEClause, NAEClause)]) [NAEClause]
-> (Lit, [(Lit, NAEClause, NAEClause)])
-> ([NAEClause], (Lit, [(Lit, NAEClause, NAEClause)]))
forall s a. State s a -> s -> (a, s)
runState (Lit
n,[]) (State (Lit, [(Lit, NAEClause, NAEClause)]) [NAEClause]
 -> ([NAEClause], (Lit, [(Lit, NAEClause, NAEClause)])))
-> State (Lit, [(Lit, NAEClause, NAEClause)]) [NAEClause]
-> ([NAEClause], (Lit, [(Lit, NAEClause, NAEClause)]))
forall a b. (a -> b) -> a -> b
$ do
      ([[NAEClause]] -> [NAEClause])
-> StateT
     (Lit, [(Lit, NAEClause, NAEClause)]) Identity [[NAEClause]]
-> State (Lit, [(Lit, 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 (Lit, [(Lit, NAEClause, NAEClause)]) Identity [[NAEClause]]
 -> State (Lit, [(Lit, NAEClause, NAEClause)]) [NAEClause])
-> StateT
     (Lit, [(Lit, NAEClause, NAEClause)]) Identity [[NAEClause]]
-> State (Lit, [(Lit, NAEClause, NAEClause)]) [NAEClause]
forall a b. (a -> b) -> a -> b
$ [NAEClause]
-> (NAEClause
    -> State (Lit, [(Lit, NAEClause, NAEClause)]) [NAEClause])
-> StateT
     (Lit, [(Lit, 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 (Lit, [(Lit, NAEClause, NAEClause)]) [NAEClause])
 -> StateT
      (Lit, [(Lit, NAEClause, NAEClause)]) Identity [[NAEClause]])
-> (NAEClause
    -> State (Lit, [(Lit, NAEClause, NAEClause)]) [NAEClause])
-> StateT
     (Lit, [(Lit, NAEClause, NAEClause)]) Identity [[NAEClause]]
forall a b. (a -> b) -> a -> b
$ \NAEClause
c -> do
        let go :: NAEClause
-> [NAEClause]
-> State (Lit, [(Lit, NAEClause, NAEClause)]) [NAEClause]
go NAEClause
c' [NAEClause]
r =
              if NAEClause -> Lit
forall (v :: * -> *) a. Vector v a => v a -> Lit
VG.length NAEClause
c' Lit -> Lit -> Bool
forall a. Ord a => a -> a -> Bool
<= Lit
k then do
                [NAEClause]
-> State (Lit, [(Lit, NAEClause, NAEClause)]) [NAEClause]
forall a.
a -> StateT (Lit, [(Lit, NAEClause, NAEClause)]) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return  ([NAEClause]
 -> State (Lit, [(Lit, NAEClause, NAEClause)]) [NAEClause])
-> [NAEClause]
-> State (Lit, [(Lit, 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) = Lit -> NAEClause -> (NAEClause, NAEClause)
forall (v :: * -> *) a. Vector v a => Lit -> v a -> (v a, v a)
VG.splitAt (Lit
k Lit -> Lit -> Lit
forall a. Num a => a -> a -> a
- Lit
1) NAEClause
c'
                (Lit
i, [(Lit, NAEClause, NAEClause)]
tbl) <- StateT
  (Lit, [(Lit, NAEClause, NAEClause)])
  Identity
  (Lit, [(Lit, NAEClause, NAEClause)])
forall s (m :: * -> *). MonadState s m => m s
get
                let w :: Lit
w = Lit
iLit -> Lit -> Lit
forall a. Num a => a -> a -> a
+Lit
1
                Lit
-> StateT (Lit, [(Lit, NAEClause, NAEClause)]) Identity ()
-> StateT (Lit, [(Lit, NAEClause, NAEClause)]) Identity ()
forall a b. a -> b -> b
seq Lit
w (StateT (Lit, [(Lit, NAEClause, NAEClause)]) Identity ()
 -> StateT (Lit, [(Lit, NAEClause, NAEClause)]) Identity ())
-> StateT (Lit, [(Lit, NAEClause, NAEClause)]) Identity ()
-> StateT (Lit, [(Lit, NAEClause, NAEClause)]) Identity ()
forall a b. (a -> b) -> a -> b
$ (Lit, [(Lit, NAEClause, NAEClause)])
-> StateT (Lit, [(Lit, NAEClause, NAEClause)]) Identity ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Lit
w, (Lit
w,NAEClause
cs1,NAEClause
cs2) (Lit, NAEClause, NAEClause)
-> [(Lit, NAEClause, NAEClause)] -> [(Lit, NAEClause, NAEClause)]
forall a. a -> [a] -> [a]
: [(Lit, NAEClause, NAEClause)]
tbl)
                NAEClause
-> [NAEClause]
-> State (Lit, [(Lit, NAEClause, NAEClause)]) [NAEClause]
go (PackedLit -> NAEClause -> NAEClause
forall (v :: * -> *) a. Vector v a => a -> v a -> v a
VG.cons (Lit -> PackedLit
SAT.packLit (- Lit
w)) NAEClause
cs2) (NAEClause -> PackedLit -> NAEClause
forall (v :: * -> *) a. Vector v a => v a -> a -> v a
VG.snoc NAEClause
cs1 (Lit -> PackedLit
SAT.packLit Lit
w) NAEClause -> [NAEClause] -> [NAEClause]
forall a. a -> [a] -> [a]
: [NAEClause]
r)
        NAEClause
-> [NAEClause]
-> State (Lit, [(Lit, 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 Lit
_n1 Lit
n2 [(Lit, NAEClause, NAEClause)]
table) Source NAESAT2NAEKSATInfo
m =
    (Lit, Lit) -> [(Lit, Bool)] -> UArray Lit Bool
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
(i, i) -> [(i, e)] -> a i e
array (Lit
1,Lit
n2) (IntMap Bool -> [(Lit, NAEClause, NAEClause)] -> [(Lit, Bool)]
forall {v :: * -> *} {v :: * -> *}.
(Vector v PackedLit, Vector v PackedLit) =>
IntMap Bool -> [(Lit, v PackedLit, v PackedLit)] -> [(Lit, Bool)]
go ([(Lit, Bool)] -> IntMap Bool
forall a. [(Lit, a)] -> IntMap a
IntMap.fromList (UArray Lit Bool -> [(Lit, Bool)]
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> [(i, e)]
assocs UArray Lit Bool
Source NAESAT2NAEKSATInfo
m)) [(Lit, NAEClause, NAEClause)]
table)
    where
      go :: IntMap Bool -> [(Lit, v PackedLit, v PackedLit)] -> [(Lit, Bool)]
go IntMap Bool
im [] = IntMap Bool -> [(Lit, Bool)]
forall a. IntMap a -> [(Lit, a)]
IntMap.toList IntMap Bool
im
      go IntMap Bool
im ((Lit
w,v PackedLit
cs1,v PackedLit
cs2) : [(Lit, v PackedLit, v PackedLit)]
tbl) = IntMap Bool -> [(Lit, v PackedLit, v PackedLit)] -> [(Lit, Bool)]
go (Lit -> Bool -> IntMap Bool -> IntMap Bool
forall a. Lit -> a -> IntMap a -> IntMap a
IntMap.insert Lit
w Bool
val IntMap Bool
im) [(Lit, 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 -> Lit -> Bool
forall a. IntMap a -> Lit -> a
IntMap.! (PackedLit -> Lit
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 -> Lit -> Bool
forall a. IntMap a -> Lit -> a
IntMap.! (- PackedLit -> Lit
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 Lit
n1 Lit
_n2 [(Lit, NAEClause, NAEClause)]
_table) = Lit -> UArray Lit Bool -> UArray Lit Bool
SAT.restrictModel Lit
n1

instance J.ToJSON NAESAT2NAEKSATInfo where
  toJSON :: NAESAT2NAEKSATInfo -> Value
toJSON (NAESAT2NAEKSATInfo Lit
nv1 Lit
nv2 [(Lit, NAEClause, NAEClause)]
table) =
    [Pair] -> Value
J.object
    [ Key
"type" Key -> Value -> Pair
forall v. ToJSON v => Key -> v -> Pair
forall e kv v. (KeyValue e kv, ToJSON v) => Key -> v -> kv
.= Text -> Value
J.String Text
"NAESAT2NAEKSATInfo"
    , Key
"num_original_variables" Key -> Lit -> Pair
forall v. ToJSON v => Key -> v -> Pair
forall e kv v. (KeyValue e kv, ToJSON v) => Key -> v -> kv
.= Lit
nv1
    , Key
"num_transformed_variables" Key -> Lit -> Pair
forall v. ToJSON v => Key -> v -> Pair
forall e kv v. (KeyValue e kv, ToJSON v) => Key -> v -> kv
.= Lit
nv2
    , Key
"table" Key -> [(Value, [Value], [Value])] -> Pair
forall v. ToJSON v => Key -> v -> Pair
forall e kv v. (KeyValue e kv, ToJSON v) => Key -> v -> kv
.=
        [ ( Lit -> Value
forall a. IsString a => Lit -> a
jVarName Lit
v :: J.Value
          , (PackedLit -> Value) -> [PackedLit] -> [Value]
forall a b. (a -> b) -> [a] -> [b]
map (Lit -> Value
forall a. IsString a => Lit -> a
jLitName (Lit -> Value) -> (PackedLit -> Lit) -> PackedLit -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PackedLit -> Lit
SAT.unpackLit) (NAEClause -> [PackedLit]
forall (v :: * -> *) a. Vector v a => v a -> [a]
VG.toList NAEClause
cs1) :: [J.Value]
          , (PackedLit -> Value) -> [PackedLit] -> [Value]
forall a b. (a -> b) -> [a] -> [b]
map (Lit -> Value
forall a. IsString a => Lit -> a
jLitName (Lit -> Value) -> (PackedLit -> Lit) -> PackedLit -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PackedLit -> Lit
SAT.unpackLit) (NAEClause -> [PackedLit]
forall (v :: * -> *) a. Vector v a => v a -> [a]
VG.toList NAEClause
cs2) :: [J.Value]
          )
        | (Lit
v, NAEClause
cs1, NAEClause
cs2) <- [(Lit, NAEClause, NAEClause)]
table
        ]
    ]

instance J.FromJSON NAESAT2NAEKSATInfo where
  parseJSON :: Value -> Parser NAESAT2NAEKSATInfo
parseJSON = String
-> (Object -> Parser NAESAT2NAEKSATInfo)
-> Value
-> Parser NAESAT2NAEKSATInfo
forall a. String -> (Object -> Parser a) -> Value -> Parser a
withTypedObject String
"NAESAT2NAEKSATInfo" ((Object -> Parser NAESAT2NAEKSATInfo)
 -> Value -> Parser NAESAT2NAEKSATInfo)
-> (Object -> Parser NAESAT2NAEKSATInfo)
-> Value
-> Parser NAESAT2NAEKSATInfo
forall a b. (a -> b) -> a -> b
$ \Object
obj -> do
    Lit -> Lit -> [(Lit, NAEClause, NAEClause)] -> NAESAT2NAEKSATInfo
NAESAT2NAEKSATInfo
      (Lit -> Lit -> [(Lit, NAEClause, NAEClause)] -> NAESAT2NAEKSATInfo)
-> Parser Lit
-> Parser
     (Lit -> [(Lit, NAEClause, NAEClause)] -> NAESAT2NAEKSATInfo)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Object
obj Object -> Key -> Parser Lit
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"num_original_variables"
      Parser (Lit -> [(Lit, NAEClause, NAEClause)] -> NAESAT2NAEKSATInfo)
-> Parser Lit
-> Parser ([(Lit, NAEClause, NAEClause)] -> NAESAT2NAEKSATInfo)
forall a b. Parser (a -> b) -> Parser a -> Parser b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Object
obj Object -> Key -> Parser Lit
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"num_transformed_variables"
      Parser ([(Lit, NAEClause, NAEClause)] -> NAESAT2NAEKSATInfo)
-> Parser [(Lit, NAEClause, NAEClause)]
-> Parser NAESAT2NAEKSATInfo
forall a b. Parser (a -> b) -> Parser a -> Parser b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (((Text, [Text], [Text]) -> Parser (Lit, NAEClause, NAEClause))
-> [(Text, [Text], [Text])] -> Parser [(Lit, NAEClause, NAEClause)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Text, [Text], [Text]) -> Parser (Lit, NAEClause, NAEClause)
forall {v :: * -> *} {v :: * -> *}.
(Vector v PackedLit, Vector v PackedLit) =>
(Text, [Text], [Text]) -> Parser (Lit, v PackedLit, v PackedLit)
f ([(Text, [Text], [Text])] -> Parser [(Lit, NAEClause, NAEClause)])
-> Parser [(Text, [Text], [Text])]
-> Parser [(Lit, NAEClause, NAEClause)]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Object
obj Object -> Key -> Parser [(Text, [Text], [Text])]
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"table")
    where
      f :: (Text, [Text], [Text]) -> Parser (Lit, v PackedLit, v PackedLit)
f (Text
v, [Text]
cs1, [Text]
cs2) = do
        Lit
v' <- Text -> Parser Lit
parseVarNameText Text
v
        [Lit]
cs1' <- (Text -> Parser Lit) -> [Text] -> Parser [Lit]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Text -> Parser Lit
parseLitNameText [Text]
cs1
        [Lit]
cs2' <- (Text -> Parser Lit) -> [Text] -> Parser [Lit]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Text -> Parser Lit
parseLitNameText [Text]
cs2
        (Lit, v PackedLit, v PackedLit)
-> Parser (Lit, v PackedLit, v PackedLit)
forall a. a -> Parser a
forall (m :: * -> *) a. Monad m => a -> m a
return (Lit
v', [PackedLit] -> v PackedLit
forall (v :: * -> *) a. Vector v a => [a] -> v a
VG.fromList ((Lit -> PackedLit) -> [Lit] -> [PackedLit]
forall a b. (a -> b) -> [a] -> [b]
map Lit -> PackedLit
SAT.packLit [Lit]
cs1'), [PackedLit] -> v PackedLit
forall (v :: * -> *) a. Vector v a => [a] -> v a
VG.fromList ((Lit -> PackedLit) -> [Lit] -> [PackedLit]
forall a b. (a -> b) -> [a] -> [b]
map Lit -> PackedLit
SAT.packLit [Lit]
cs2'))

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

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) = Lit -> NAESAT -> (NAESAT, NAESAT2NAEKSATInfo)
naesat2naeksat Lit
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 (Lit
n,[NAEClause]
cs)
  | (NAEClause -> Bool) -> [NAEClause] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\NAEClause
c -> NAEClause -> Lit
forall (v :: * -> *) a. Vector v a => v a -> Lit
VG.length NAEClause
c Lit -> Lit -> Bool
forall a. Ord a => a -> a -> Bool
< Lit
2) [NAEClause]
cs =
      ( ( CNF.WCNF
          { wcnfTopCost :: Integer
CNF.wcnfTopCost = Integer
2
          , wcnfNumVars :: Lit
CNF.wcnfNumVars = Lit
n
          , wcnfClauses :: [WeightedClause]
CNF.wcnfClauses = [(Integer
1, [Lit] -> NAEClause
SAT.packClause [])]
          , wcnfNumClauses :: Lit
CNF.wcnfNumClauses = Lit
1
          }
        , Integer
0
        )
      , NAESAT2SATInfo
forall a. IdentityTransformer a
IdentityTransformer
      )
  | Bool
otherwise =
      ( ( CNF.WCNF
          { wcnfTopCost :: Integer
CNF.wcnfTopCost = Lit -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Lit
nc' Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1
          , wcnfNumVars :: Lit
CNF.wcnfNumVars = Lit
n
          , wcnfClauses :: [WeightedClause]
CNF.wcnfClauses = [WeightedClause]
cs'
          , wcnfNumClauses :: Lit
CNF.wcnfNumClauses = Lit
nc'
          }
        , Integer
t
        )
      , NAESAT2SATInfo
forall a. IdentityTransformer a
IdentityTransformer
      )
  where
    nc' :: Lit
nc' = [WeightedClause] -> Lit
forall a. [a] -> Lit
forall (t :: * -> *) a. Foldable t => t a -> Lit
length [WeightedClause]
cs'
    ([WeightedClause]
cs', Integer
t) = (([WeightedClause], Integer)
 -> NAEClause -> ([WeightedClause], Integer))
-> ([WeightedClause], Integer)
-> [NAEClause]
-> ([WeightedClause], Integer)
forall b a. (b -> a -> b) -> b -> [a] -> b
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 -> [Lit]
SAT.unpackClause NAEClause
c of
            []  -> String -> ([WeightedClause], Integer)
forall a. HasCallStack => String -> a
error String
"nae3sat2max2sat: should not happen"
            [Lit
_] -> String -> ([WeightedClause], Integer)
forall a. HasCallStack => String -> a
error String
"nae3sat2max2sat: should not happen"
            [Lit
_,Lit
_] ->
                ( [(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
                )
            [Lit
l0,Lit
l1,Lit
l2] ->
                ( [[WeightedClause]] -> [WeightedClause]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[(Integer
1, [Lit] -> NAEClause
SAT.packClause [Lit
a,Lit
b]), (Integer
1, [Lit] -> NAEClause
SAT.packClause [-Lit
a,-Lit
b])] | (Lit
a,Lit
b) <- [(Lit
l0,Lit
l1),(Lit
l1,Lit
l2),(Lit
l2,Lit
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
                )
            [Lit]
_ -> String -> ([WeightedClause], Integer)
forall a. HasCallStack => String -> a
error String
"nae3sat2max2sat: cannot handle nae-clause of size >3"

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