{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_HADDOCK show-extensions #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  ToySolver.SAT.Encoder.Cardinality
-- Copyright   :  (c) Masahiro Sakai 2019
-- License     :  BSD-style
--
-- Maintainer  :  masahiro.sakai@gmail.com
-- Stability   :  provisional
-- Portability :  non-portable
--
-----------------------------------------------------------------------------
module ToySolver.SAT.Encoder.Cardinality
  ( Encoder
  , Strategy (..)
  , newEncoder
  , newEncoderWithStrategy
  , encodeAtLeast
  , encodeAtLeastWithPolarity
  , getTseitinEncoder

    -- XXX
  , TotalizerDefinitions
  , getTotalizerDefinitions
  , evalTotalizerDefinitions

  -- * Polarity
  , Polarity (..)
  , negatePolarity
  , polarityPos
  , polarityNeg
  , polarityBoth
  , polarityNone
  ) where

import Control.Monad.Primitive
import qualified ToySolver.SAT.Types as SAT
import qualified ToySolver.SAT.Encoder.Tseitin as Tseitin
import ToySolver.SAT.Encoder.Tseitin (Polarity (..), negatePolarity, polarityPos, polarityNeg, polarityBoth, polarityNone)
import ToySolver.SAT.Encoder.Cardinality.Internal.Naive
import ToySolver.SAT.Encoder.Cardinality.Internal.ParallelCounter
import ToySolver.SAT.Encoder.PB.Internal.BDD as BDD
import qualified ToySolver.SAT.Encoder.Cardinality.Internal.Totalizer as Totalizer

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

-- XXX
data Encoder m = Encoder (Totalizer.Encoder m) Strategy

data Strategy
  = Naive
  | SequentialCounter
  | ParallelCounter
  | Totalizer
  deriving (Int -> Strategy -> ShowS
[Strategy] -> ShowS
Strategy -> String
(Int -> Strategy -> ShowS)
-> (Strategy -> String) -> ([Strategy] -> ShowS) -> Show Strategy
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Strategy -> ShowS
showsPrec :: Int -> Strategy -> ShowS
$cshow :: Strategy -> String
show :: Strategy -> String
$cshowList :: [Strategy] -> ShowS
showList :: [Strategy] -> ShowS
Show, Strategy -> Strategy -> Bool
(Strategy -> Strategy -> Bool)
-> (Strategy -> Strategy -> Bool) -> Eq Strategy
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Strategy -> Strategy -> Bool
== :: Strategy -> Strategy -> Bool
$c/= :: Strategy -> Strategy -> Bool
/= :: Strategy -> Strategy -> Bool
Eq, Eq Strategy
Eq Strategy =>
(Strategy -> Strategy -> Ordering)
-> (Strategy -> Strategy -> Bool)
-> (Strategy -> Strategy -> Bool)
-> (Strategy -> Strategy -> Bool)
-> (Strategy -> Strategy -> Bool)
-> (Strategy -> Strategy -> Strategy)
-> (Strategy -> Strategy -> Strategy)
-> Ord Strategy
Strategy -> Strategy -> Bool
Strategy -> Strategy -> Ordering
Strategy -> Strategy -> Strategy
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Strategy -> Strategy -> Ordering
compare :: Strategy -> Strategy -> Ordering
$c< :: Strategy -> Strategy -> Bool
< :: Strategy -> Strategy -> Bool
$c<= :: Strategy -> Strategy -> Bool
<= :: Strategy -> Strategy -> Bool
$c> :: Strategy -> Strategy -> Bool
> :: Strategy -> Strategy -> Bool
$c>= :: Strategy -> Strategy -> Bool
>= :: Strategy -> Strategy -> Bool
$cmax :: Strategy -> Strategy -> Strategy
max :: Strategy -> Strategy -> Strategy
$cmin :: Strategy -> Strategy -> Strategy
min :: Strategy -> Strategy -> Strategy
Ord, Int -> Strategy
Strategy -> Int
Strategy -> [Strategy]
Strategy -> Strategy
Strategy -> Strategy -> [Strategy]
Strategy -> Strategy -> Strategy -> [Strategy]
(Strategy -> Strategy)
-> (Strategy -> Strategy)
-> (Int -> Strategy)
-> (Strategy -> Int)
-> (Strategy -> [Strategy])
-> (Strategy -> Strategy -> [Strategy])
-> (Strategy -> Strategy -> [Strategy])
-> (Strategy -> Strategy -> Strategy -> [Strategy])
-> Enum Strategy
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
$csucc :: Strategy -> Strategy
succ :: Strategy -> Strategy
$cpred :: Strategy -> Strategy
pred :: Strategy -> Strategy
$ctoEnum :: Int -> Strategy
toEnum :: Int -> Strategy
$cfromEnum :: Strategy -> Int
fromEnum :: Strategy -> Int
$cenumFrom :: Strategy -> [Strategy]
enumFrom :: Strategy -> [Strategy]
$cenumFromThen :: Strategy -> Strategy -> [Strategy]
enumFromThen :: Strategy -> Strategy -> [Strategy]
$cenumFromTo :: Strategy -> Strategy -> [Strategy]
enumFromTo :: Strategy -> Strategy -> [Strategy]
$cenumFromThenTo :: Strategy -> Strategy -> Strategy -> [Strategy]
enumFromThenTo :: Strategy -> Strategy -> Strategy -> [Strategy]
Enum, Strategy
Strategy -> Strategy -> Bounded Strategy
forall a. a -> a -> Bounded a
$cminBound :: Strategy
minBound :: Strategy
$cmaxBound :: Strategy
maxBound :: Strategy
Bounded)
{-
"Sequential Counter" from "Towards an Optimal CNF Encoding of Boolean
Cardinality Constraints" is a special case of BDD-based encoding of
"Translating Pseudo-Boolean Constraints into SAT" (using the fact C→B
to represent ite(A,B,C) as (A∧B)∨C instead of (A∧B)∨(¬A∧C))?

http://www.carstensinz.de/papers/CP-2005.pdf
http://www.st.ewi.tudelft.nl/jsat/content/volume2/JSAT2_1_Een.pdf
-}

newEncoder :: PrimMonad m => Tseitin.Encoder m -> m (Encoder m)
newEncoder :: forall (m :: * -> *). PrimMonad m => Encoder m -> m (Encoder m)
newEncoder Encoder m
tseitin = Encoder m -> Strategy -> m (Encoder m)
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Strategy -> m (Encoder m)
newEncoderWithStrategy Encoder m
tseitin Strategy
ParallelCounter

newEncoderWithStrategy :: PrimMonad m => Tseitin.Encoder m -> Strategy -> m (Encoder m)
newEncoderWithStrategy :: forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Strategy -> m (Encoder m)
newEncoderWithStrategy Encoder m
tseitin Strategy
strategy = do
  Encoder m
base <- Encoder m -> m (Encoder m)
forall (m :: * -> *). PrimMonad m => Encoder m -> m (Encoder m)
Totalizer.newEncoder Encoder m
tseitin
  Encoder m -> m (Encoder m)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Encoder m -> m (Encoder m)) -> Encoder m -> m (Encoder m)
forall a b. (a -> b) -> a -> b
$ Encoder m -> Strategy -> Encoder m
forall (m :: * -> *). Encoder m -> Strategy -> Encoder m
Encoder Encoder m
base Strategy
strategy

type TotalizerDefinitions = Totalizer.Definitions

getTotalizerDefinitions :: PrimMonad m => Encoder m -> m TotalizerDefinitions
getTotalizerDefinitions :: forall (m :: * -> *).
PrimMonad m =>
Encoder m -> m TotalizerDefinitions
getTotalizerDefinitions (Encoder Encoder m
base Strategy
_) = Encoder m -> m TotalizerDefinitions
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> m TotalizerDefinitions
Totalizer.getDefinitions Encoder m
base

evalTotalizerDefinitions :: SAT.IModel m => m -> TotalizerDefinitions -> [(SAT.Var, Bool)]
evalTotalizerDefinitions :: forall m. IModel m => m -> TotalizerDefinitions -> [(Int, Bool)]
evalTotalizerDefinitions m
m TotalizerDefinitions
defs = m -> TotalizerDefinitions -> [(Int, Bool)]
forall m. IModel m => m -> TotalizerDefinitions -> [(Int, Bool)]
Totalizer.evalDefinitions m
m TotalizerDefinitions
defs

getTseitinEncoder :: Encoder m -> Tseitin.Encoder m
getTseitinEncoder :: forall (m :: * -> *). Encoder m -> Encoder m
getTseitinEncoder (Encoder (Totalizer.Encoder Encoder m
tseitin MutVar (PrimState m) (Map LitSet (Vector Int))
_) Strategy
_) = Encoder m
tseitin

instance Monad m => SAT.NewVar m (Encoder m) where
  newVar :: Encoder m -> m Int
newVar   (Encoder Encoder m
base Strategy
_) = Encoder m -> m Int
forall (m :: * -> *) a. NewVar m a => a -> m Int
SAT.newVar Encoder m
base
  newVars :: Encoder m -> Int -> m [Int]
newVars  (Encoder Encoder m
base Strategy
_) = Encoder m -> Int -> m [Int]
forall (m :: * -> *) a. NewVar m a => a -> Int -> m [Int]
SAT.newVars Encoder m
base
  newVars_ :: Encoder m -> Int -> m ()
newVars_ (Encoder Encoder m
base Strategy
_) = Encoder m -> Int -> m ()
forall (m :: * -> *) a. NewVar m a => a -> Int -> m ()
SAT.newVars_ Encoder m
base

instance Monad m => SAT.AddClause m (Encoder m) where
  addClause :: Encoder m -> [Int] -> m ()
addClause (Encoder Encoder m
base Strategy
_) = Encoder m -> [Int] -> m ()
forall (m :: * -> *) a. AddClause m a => a -> [Int] -> m ()
SAT.addClause Encoder m
base

instance PrimMonad m => SAT.AddCardinality m (Encoder m) where
  addAtLeast :: Encoder m -> [Int] -> Int -> m ()
addAtLeast (Encoder base :: Encoder m
base@(Totalizer.Encoder Encoder m
tseitin MutVar (PrimState m) (Map LitSet (Vector Int))
_) Strategy
strategy) [Int]
lhs Int
rhs
    | Int
rhs Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
0  = () -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    | Bool
otherwise =
        case Strategy
strategy of
          Strategy
Naive -> Encoder m -> AtLeast -> m ()
forall (m :: * -> *). PrimMonad m => Encoder m -> AtLeast -> m ()
addAtLeastNaive Encoder m
tseitin ([Int]
lhs,Int
rhs)
          Strategy
ParallelCounter -> Encoder m -> AtLeast -> m ()
forall (m :: * -> *). PrimMonad m => Encoder m -> AtLeast -> m ()
addAtLeastParallelCounter Encoder m
tseitin ([Int]
lhs,Int
rhs)
          Strategy
SequentialCounter -> Encoder m -> PBLinAtLeast -> m ()
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> PBLinAtLeast -> m ()
BDD.addPBLinAtLeastBDD Encoder m
tseitin ([(Integer
1,Int
l) | Int
l <- [Int]
lhs], Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
rhs)
          Strategy
Totalizer -> Encoder m -> AtLeast -> m ()
forall (m :: * -> *). PrimMonad m => Encoder m -> AtLeast -> m ()
Totalizer.addAtLeast Encoder m
base ([Int]
lhs,Int
rhs)

encodeAtLeast :: PrimMonad m => Encoder m -> SAT.AtLeast -> m SAT.Lit
encodeAtLeast :: forall (m :: * -> *). PrimMonad m => Encoder m -> AtLeast -> m Int
encodeAtLeast Encoder m
enc = Encoder m -> Polarity -> AtLeast -> m Int
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Polarity -> AtLeast -> m Int
encodeAtLeastWithPolarity Encoder m
enc Polarity
polarityBoth

encodeAtLeastWithPolarity :: PrimMonad m => Encoder m -> Polarity -> SAT.AtLeast -> m SAT.Lit
encodeAtLeastWithPolarity :: forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Polarity -> AtLeast -> m Int
encodeAtLeastWithPolarity (Encoder base :: Encoder m
base@(Totalizer.Encoder Encoder m
tseitin MutVar (PrimState m) (Map LitSet (Vector Int))
_) Strategy
strategy) Polarity
polarity =
  case Strategy
strategy of
    Strategy
Naive -> Encoder m -> Polarity -> AtLeast -> m Int
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Polarity -> AtLeast -> m Int
encodeAtLeastWithPolarityNaive Encoder m
tseitin Polarity
polarity
    Strategy
ParallelCounter -> Encoder m -> Polarity -> AtLeast -> m Int
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Polarity -> AtLeast -> m Int
encodeAtLeastWithPolarityParallelCounter Encoder m
tseitin Polarity
polarity
    Strategy
SequentialCounter -> \([Int]
lhs,Int
rhs) -> Encoder m -> Polarity -> PBLinAtLeast -> m Int
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Polarity -> PBLinAtLeast -> m Int
BDD.encodePBLinAtLeastWithPolarityBDD Encoder m
tseitin Polarity
polarity ([(Integer
1,Int
l) | Int
l <- [Int]
lhs], Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
rhs)
    Strategy
Totalizer -> Encoder m -> Polarity -> AtLeast -> m Int
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Polarity -> AtLeast -> m Int
Totalizer.encodeAtLeastWithPolarity Encoder m
base Polarity
polarity