Types.hs

{-# OPTIONS_HADDOCK show-extensions #-}
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  ToySolver.SAT.Types
-- Copyright   :  (c) Masahiro Sakai 2012
-- License     :  BSD-style
--
-- Maintainer  :  masahiro.sakai@gmail.com
-- Stability   :  provisional
-- Portability :  non-portable
--
-----------------------------------------------------------------------------
module ToySolver.SAT.Types
  (
  -- * Variable
    Var
  , VarSet
  , VarMap
  , validVar

  -- * Model
  , IModel (..)
  , Model
  , restrictModel

  -- * Literal
  , Lit
  , LitSet
  , LitMap
  , litUndef
  , validLit
  , literal
  , litNot
  , litVar
  , litPolarity
  , evalLit

  -- * Clause
  , Clause
  , normalizeClause
  , instantiateClause
  , clauseSubsume
  , evalClause
  , clauseToPBLinAtLeast

  -- * Packed Clause
  , PackedVar
  , PackedLit
  , packLit
  , unpackLit
  , PackedClause
  , packClause
  , unpackClause

  -- * Cardinality Constraint
  , AtLeast
  , Exactly
  , normalizeAtLeast
  , instantiateAtLeast
  , evalAtLeast
  , evalExactly

  -- * (Linear) Pseudo Boolean Constraint
  , PBLinTerm
  , PBLinSum
  , PBLinAtLeast
  , PBLinExactly
  , normalizePBLinSum
  , normalizePBLinAtLeast
  , normalizePBLinExactly
  , instantiatePBLinAtLeast
  , instantiatePBLinExactly
  , cutResolve
  , cardinalityReduction
  , negatePBLinAtLeast
  , evalPBLinSum
  , evalPBLinAtLeast
  , evalPBLinExactly
  , pbLinLowerBound
  , pbLinUpperBound
  , pbLinSubsume

  -- * Non-linear Pseudo Boolean constraint
  , PBTerm
  , PBSum
  , evalPBSum
  , evalPBConstraint
  , evalPBFormula
  , evalPBSoftFormula
  , pbLowerBound
  , pbUpperBound
  , removeNegationFromPBSum

  -- * XOR Clause
  , XORClause
  , normalizeXORClause
  , instantiateXORClause
  , evalXORClause

  -- * Type classes for solvers
  , NewVar (..)
  , AddClause (..)
  , AddCardinality (..)
  , AddPBLin (..)
  , AddPBNL (..)
  , AddXORClause (..)

  -- * Type-2 SOS constraints
  , addSOS2
  , evalSOS2
  ) where

import Control.Monad
import Control.Exception
import Data.Array.Unboxed
import Data.Ord
import Data.List
import Data.Int
import Data.IntMap.Strict (IntMap)
import qualified Data.IntMap.Strict as IntMap
import Data.IntSet (IntSet)
import qualified Data.IntSet as IntSet
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import Data.Maybe
import qualified Data.Vector as V
import qualified Data.Vector.Unboxed as VU
import qualified Data.PseudoBoolean as PBFile
import ToySolver.Data.LBool
import qualified ToySolver.Combinatorial.SubsetSum as SubsetSum

-- | Variable is represented as positive integers (DIMACS format).
type Var = Int

type VarSet = IntSet
type VarMap = IntMap

{-# INLINE validVar #-}
validVar :: Var -> Bool
validVar v = v > 0

class IModel a where
  evalVar :: a -> Var -> Bool

-- | A model is represented as a mapping from variables to its values.
type Model = UArray Var Bool

-- | Restrict model to first @nv@ variables.
restrictModel :: Int -> Model -> Model
restrictModel nv m = array (1,nv) [(v, m ! v) | v <- [1..nv]]

instance IModel (UArray Var Bool) where
  evalVar m v = m ! v

instance IModel (Array Var Bool) where
  evalVar m v = m ! v

instance IModel (Var -> Bool) where
  evalVar m v = m v

-- | Positive (resp. negative) literals are represented as positive (resp.
-- negative) integers. (DIMACS format).
type Lit = Int

{-# INLINE litUndef #-}
litUndef :: Lit
litUndef = 0

type LitSet = IntSet
type LitMap = IntMap

{-# INLINE validLit #-}
validLit :: Lit -> Bool
validLit l = l /= 0

{-# INLINE literal #-}
-- | Construct a literal from a variable and its polarity.
-- 'True' (resp 'False') means positive (resp. negative) literal.
literal :: Var  -- ^ variable
        -> Bool -- ^ polarity
        -> Lit
literal v polarity =
  assert (validVar v) $ if polarity then v else litNot v

{-# INLINE litNot #-}
-- | Negation of the 'Lit'.
litNot :: Lit -> Lit
litNot l = assert (validLit l) $ negate l

{-# INLINE litVar #-}
-- | Underlying variable of the 'Lit'
litVar :: Lit -> Var
litVar l = assert (validLit l) $ abs l

{-# INLINE litPolarity #-}
-- | Polarity of the 'Lit'.
-- 'True' means positive literal and 'False' means negative literal.
litPolarity :: Lit -> Bool
litPolarity l = assert (validLit l) $ l > 0

{-# INLINEABLE evalLit #-}
{-# SPECIALIZE evalLit :: Model -> Lit -> Bool #-}
evalLit :: IModel m => m -> Lit -> Bool
evalLit m l = if l > 0 then evalVar m l else not (evalVar m (abs l))

-- | Disjunction of 'Lit'.
type Clause = [Lit]

-- | Normalizing clause
--
-- 'Nothing' if the clause is trivially true.
normalizeClause :: Clause -> Maybe Clause
normalizeClause lits = assert (IntSet.size ys `mod` 2 == 0) $
  if IntSet.null ys
    then Just (IntSet.toList xs)
    else Nothing
  where
    xs = IntSet.fromList lits
    ys = xs `IntSet.intersection` (IntSet.map litNot xs)

{-# SPECIALIZE instantiateClause :: (Lit -> IO LBool) -> Clause -> IO (Maybe Clause) #-}
instantiateClause :: forall m. Monad m => (Lit -> m LBool) -> Clause -> m (Maybe Clause)
instantiateClause evalLitM = loop []
  where
    loop :: [Lit] -> [Lit] -> m (Maybe Clause)
    loop ret [] = return $ Just ret
    loop ret (l:ls) = do
      val <- evalLitM l
      if val==lTrue then
        return Nothing
      else if val==lFalse then
        loop ret ls
      else
        loop (l : ret) ls

clauseSubsume :: Clause -> Clause -> Bool
clauseSubsume cl1 cl2 = cl1' `IntSet.isSubsetOf` cl2'
  where
    cl1' = IntSet.fromList cl1
    cl2' = IntSet.fromList cl2

evalClause :: IModel m => m -> Clause -> Bool
evalClause m cl = any (evalLit m) cl

clauseToPBLinAtLeast :: Clause -> PBLinAtLeast
clauseToPBLinAtLeast xs = ([(1,l) | l <- xs], 1)

type PackedVar = PackedLit
type PackedLit = Int32

packLit :: Lit -> PackedLit
packLit = fromIntegral

unpackLit :: PackedLit -> Lit
unpackLit = fromIntegral

type PackedClause = VU.Vector PackedLit

packClause :: Clause -> PackedClause
packClause = VU.fromList . map packLit

unpackClause :: PackedClause -> Clause
unpackClause = map unpackLit . VU.toList

type AtLeast = ([Lit], Int)
type Exactly = ([Lit], Int)

normalizeAtLeast :: AtLeast -> AtLeast
normalizeAtLeast (lits,n) = assert (IntSet.size ys `mod` 2 == 0) $
   (IntSet.toList lits', n')
   where
     xs = IntSet.fromList lits
     ys = xs `IntSet.intersection` (IntSet.map litNot xs)
     lits' = xs `IntSet.difference` ys
     n' = n - (IntSet.size ys `div` 2)

{-# SPECIALIZE instantiateAtLeast :: (Lit -> IO LBool) -> AtLeast -> IO AtLeast #-}
instantiateAtLeast :: forall m. Monad m => (Lit -> m LBool) -> AtLeast -> m AtLeast
instantiateAtLeast evalLitM (xs,n) = loop ([],n) xs
  where
    loop :: AtLeast -> [Lit] -> m AtLeast
    loop ret [] = return ret
    loop (ys,m) (l:ls) = do
      val <- evalLitM l
      if val == lTrue then
        loop (ys, m-1) ls
      else if val == lFalse then
        loop (ys, m) ls
      else
        loop (l:ys, m) ls

evalAtLeast :: IModel m => m -> AtLeast -> Bool
evalAtLeast m (lits,n) = sum [1 | lit <- lits, evalLit m lit] >= n

evalExactly :: IModel m => m -> Exactly -> Bool
evalExactly m (lits,n) = sum [1 | lit <- lits, evalLit m lit] == n

type PBLinTerm = (Integer, Lit)
type PBLinSum = [PBLinTerm]
type PBLinAtLeast = (PBLinSum, Integer)
type PBLinExactly = (PBLinSum, Integer)

-- | normalizing PB term of the form /c1 x1 + c2 x2 ... cn xn + c/ into
-- /d1 x1 + d2 x2 ... dm xm + d/ where d1,...,dm ≥ 1.
normalizePBLinSum :: (PBLinSum, Integer) -> (PBLinSum, Integer)
normalizePBLinSum = step2 . step1
  where
    -- 同じ変数が複数回現れないように、一度全部 @v@ に統一。
    step1 :: (PBLinSum, Integer) -> (PBLinSum, Integer)
    step1 (xs,n) =
      case loop (IntMap.empty,n) xs of
        (ys,n') -> ([(c,v) | (v,c) <- IntMap.toList ys], n')
      where
        loop :: (VarMap Integer, Integer) -> PBLinSum -> (VarMap Integer, Integer)
        loop (ys,m) [] = (ys,m)
        loop (ys,m) ((c,l):zs) =
          if litPolarity l
            then loop (IntMap.insertWith (+) l c ys, m) zs
            else loop (IntMap.insertWith (+) (litNot l) (negate c) ys, m+c) zs

    -- 係数が0のものも取り除き、係数が負のリテラルを反転することで、
    -- 係数が正になるようにする。
    step2 :: (PBLinSum, Integer) -> (PBLinSum, Integer)
    step2 (xs,n) = loop ([],n) xs
      where
        loop (ys,m) [] = (ys,m)
        loop (ys,m) (t@(c,l):zs)
          | c == 0 = loop (ys,m) zs
          | c < 0  = loop ((negate c,litNot l):ys, m+c) zs
          | otherwise = loop (t:ys,m) zs

-- | normalizing PB constraint of the form /c1 x1 + c2 cn ... cn xn >= b/.
normalizePBLinAtLeast :: PBLinAtLeast -> PBLinAtLeast
normalizePBLinAtLeast a =
  case step1 a of
    (xs,n)
      | n > 0     -> step4 $ step3 (xs,n)
      | otherwise -> ([], 0) -- trivially true
  where
    step1 :: PBLinAtLeast -> PBLinAtLeast
    step1 (xs,n) =
      case normalizePBLinSum (xs,-n) of
        (ys,m) -> (ys, -m)

    -- saturation + gcd reduction
    step3 :: PBLinAtLeast -> PBLinAtLeast
    step3 (xs,n) =
      case [c | (c,_) <- xs, assert (c>0) (c < n)] of
        [] -> ([(1,l) | (c,l) <- xs], 1)
        cs ->
          let d = foldl1' gcd cs
              m = (n+d-1) `div` d
          in ([(if c >= n then m else c `div` d, l) | (c,l) <- xs], m)

    -- subset sum
    step4 :: PBLinAtLeast -> PBLinAtLeast
    step4 (xs,n) =
      case SubsetSum.minSubsetSum (V.fromList [c | (c,_) <- xs]) n of
        Just (m, _) -> (xs, m)
        Nothing -> ([], 1) -- false

-- | normalizing PB constraint of the form /c1 x1 + c2 cn ... cn xn = b/.
normalizePBLinExactly :: PBLinExactly -> PBLinExactly
normalizePBLinExactly a =
　case step1 $ a of
    (xs,n)
      | n >= 0    -> step3 $ step2 (xs, n)
      | otherwise -> ([], 1) -- false
  where
    step1 :: PBLinExactly -> PBLinExactly
    step1 (xs,n) =
      case normalizePBLinSum (xs,-n) of
        (ys,m) -> (ys, -m)

    -- omega test と同様の係数の gcd による単純化
    step2 :: PBLinExactly -> PBLinExactly
    step2 ([],n) = ([],n)
    step2 (xs,n)
      | n `mod` d == 0 = ([(c `div` d, l) | (c,l) <- xs], n `div` d)
      | otherwise      = ([], 1) -- false
      where
        d = foldl1' gcd [c | (c,_) <- xs]

    -- subset sum
    step3 :: PBLinExactly -> PBLinExactly
    step3 constr@(xs,n) =
      case SubsetSum.subsetSum (V.fromList [c | (c,_) <- xs]) n of
        Just _ -> constr
        Nothing -> ([], 1) -- false

{-# SPECIALIZE instantiatePBLinAtLeast :: (Lit -> IO LBool) -> PBLinAtLeast -> IO PBLinAtLeast #-}
instantiatePBLinAtLeast :: forall m. Monad m => (Lit -> m LBool) -> PBLinAtLeast -> m PBLinAtLeast
instantiatePBLinAtLeast evalLitM (xs,n) = loop ([],n) xs
  where
    loop :: PBLinAtLeast -> PBLinSum -> m PBLinAtLeast
    loop ret [] = return ret
    loop (ys,m) ((c,l):ts) = do
      val <- evalLitM l
      if val == lTrue then
        loop (ys, m-c) ts
      else if val == lFalse then
        loop (ys, m) ts
      else
        loop ((c,l):ys, m) ts

{-# SPECIALIZE instantiatePBLinExactly :: (Lit -> IO LBool) -> PBLinExactly -> IO PBLinExactly #-}
instantiatePBLinExactly :: Monad m => (Lit -> m LBool) -> PBLinExactly -> m PBLinExactly
instantiatePBLinExactly = instantiatePBLinAtLeast

cutResolve :: PBLinAtLeast -> PBLinAtLeast -> Var -> PBLinAtLeast
cutResolve (lhs1,rhs1) (lhs2,rhs2) v = assert (l1 == litNot l2) $ normalizePBLinAtLeast pb
  where
    (c1,l1) = head [(c,l) | (c,l) <- lhs1, litVar l == v]
    (c2,l2) = head [(c,l) | (c,l) <- lhs2, litVar l == v]
    g = gcd c1 c2
    s1 = c2 `div` g
    s2 = c1 `div` g
    pb = ([(s1*c,l) | (c,l) <- lhs1] ++ [(s2*c,l) | (c,l) <- lhs2], s1*rhs1 + s2 * rhs2)

cardinalityReduction :: PBLinAtLeast -> AtLeast
cardinalityReduction (lhs,rhs) = (ls, rhs')
  where
    rhs' = go1 0 0 (sortBy (flip (comparing fst)) lhs)

    go1 !s !k ((a,_):ts)
      | s < rhs   = go1 (s+a) (k+1) ts
      | otherwise = k
    go1 _ _ [] = error "ToySolver.SAT.Types.cardinalityReduction: should not happen"

    ls = go2 (minimum (rhs : map (subtract 1 . fst) lhs)) (sortBy (comparing fst) lhs)

    go2 !guard' ((a,_) : ts)
      | a - 1 < guard' = go2 (guard' - a) ts
      | otherwise      = map snd ts
    go2 _ [] = error "ToySolver.SAT.Types.cardinalityReduction: should not happen"

negatePBLinAtLeast :: PBLinAtLeast -> PBLinAtLeast
negatePBLinAtLeast (xs, rhs) = ([(-c,lit) | (c,lit)<-xs] , -rhs + 1)

evalPBLinSum :: IModel m => m -> PBLinSum -> Integer
evalPBLinSum m xs = sum [c | (c,lit) <- xs, evalLit m lit]

evalPBLinAtLeast :: IModel m => m -> PBLinAtLeast -> Bool
evalPBLinAtLeast m (lhs,rhs) = evalPBLinSum m lhs >= rhs

evalPBLinExactly :: IModel m => m -> PBLinAtLeast -> Bool
evalPBLinExactly m (lhs,rhs) = evalPBLinSum m lhs == rhs

pbLinLowerBound :: PBLinSum -> Integer
pbLinLowerBound xs = sum [if c < 0 then c else 0 | (c,_) <- xs]

pbLinUpperBound :: PBLinSum -> Integer
pbLinUpperBound xs = sum [if c > 0 then c else 0 | (c,_) <- xs]

-- (Σi ci li ≥ rhs1) subsumes (Σi di li ≥ rhs2) iff rhs1≥rhs2 and di≥ci for all i.
pbLinSubsume :: PBLinAtLeast -> PBLinAtLeast -> Bool
pbLinSubsume (lhs1,rhs1) (lhs2,rhs2) =
  rhs1 >= rhs2 && and [di >= ci | (ci,li) <- lhs1, let di = IntMap.findWithDefault 0 li lhs2']
  where
    lhs2' = IntMap.fromList [(l,c) | (c,l) <- lhs2]

type PBTerm = (Integer, [Lit])
type PBSum = [PBTerm]

evalPBSum :: IModel m => m -> PBSum -> Integer
evalPBSum m xs = sum [c | (c,lits) <- xs, all (evalLit m) lits]

evalPBConstraint :: IModel m => m -> PBFile.Constraint -> Bool
evalPBConstraint m (lhs,op,rhs) = op' (evalPBSum m lhs) rhs
  where
    op' = case op of
            PBFile.Ge -> (>=)
            PBFile.Eq -> (==)

evalPBFormula :: IModel m => m -> PBFile.Formula -> Maybe Integer
evalPBFormula m formula = do
  guard $ all (evalPBConstraint m) $ PBFile.pbConstraints formula
  return $ evalPBSum m $ fromMaybe [] $ PBFile.pbObjectiveFunction formula

evalPBSoftFormula :: IModel m => m -> PBFile.SoftFormula -> Maybe Integer
evalPBSoftFormula m formula = do
  obj <- liftM sum $ forM (PBFile.wboConstraints formula) $ \(cost, constr) -> do
    case cost of
      Nothing -> do
        guard $ evalPBConstraint m constr
        return 0
      Just w
        | evalPBConstraint m constr -> return 0
        | otherwise -> return w
  case PBFile.wboTopCost formula of
    Nothing -> return ()
    Just c -> guard (obj < c)
  return obj

pbLowerBound :: PBSum -> Integer
pbLowerBound xs = sum [c | (c,ls) <- xs, c < 0 || null ls]

pbUpperBound :: PBSum -> Integer
pbUpperBound xs = sum [c | (c,ls) <- xs, c > 0 || null ls]

removeNegationFromPBSum :: PBSum -> PBSum
removeNegationFromPBSum ts =
  [(c, IntSet.toList m) | (m, c) <- Map.toList $ Map.unionsWith (+) $ map f ts, c /= 0]
  where
    f :: PBTerm -> Map VarSet Integer
    f (c, ls) = IntSet.foldl' g (Map.singleton IntSet.empty c) (IntSet.fromList ls)

    g :: Map VarSet Integer -> Lit -> Map VarSet Integer
    g m l
      | l > 0     = Map.mapKeysWith (+) (IntSet.insert v) m
      | otherwise = Map.unionWith (+) m $ Map.fromListWith (+) [(IntSet.insert v xs, negate c) | (xs,c) <- Map.toList m]
      where
        v = litVar l

-- | XOR clause
--
-- '([l1,l2..ln], b)' means l1 ⊕ l2 ⊕ ⋯ ⊕ ln = b.
--
-- Note that:
--
-- * True can be represented as ([], False)
--
-- * False can be represented as ([], True)
--
type XORClause = ([Lit], Bool)

-- | Normalize XOR clause
normalizeXORClause :: XORClause -> XORClause
normalizeXORClause (lits, b) =
  case IntMap.keys m of
    0:xs -> (xs, not b)
    xs -> (xs, b)
  where
    m = IntMap.filter id $ IntMap.unionsWith xor [f lit | lit <- lits]
    xor = (/=)

    f 0 = IntMap.singleton 0 True
    f lit =
      if litPolarity lit
      then IntMap.singleton lit True
      else IntMap.fromList [(litVar lit, True), (0, True)]  -- ¬x = x ⊕ 1

{-# SPECIALIZE instantiateXORClause :: (Lit -> IO LBool) -> XORClause -> IO XORClause #-}
instantiateXORClause :: forall m. Monad m => (Lit -> m LBool) -> XORClause -> m XORClause
instantiateXORClause evalLitM (ls,b) = loop [] b ls
  where
    loop :: [Lit] -> Bool -> [Lit] -> m XORClause
    loop lhs !rhs [] = return (lhs, rhs)
    loop lhs !rhs (l:ls) = do
      val <- evalLitM l
      if val==lTrue then
        loop lhs (not rhs) ls
      else if val==lFalse then
        loop lhs rhs ls
      else
        loop (l : lhs) rhs ls

evalXORClause :: IModel m => m -> XORClause -> Bool
evalXORClause m (lits, rhs) = foldl' xor False (map f lits) == rhs
  where
    xor = (/=)
    f 0 = True
    f lit = evalLit m lit


class Monad m => NewVar m a | a -> m where
  {-# MINIMAL newVar #-}

  -- | Add a new variable
  newVar :: a -> m Var

  -- | Add variables. @newVars a n = replicateM n (newVar a)@, but maybe faster.
  newVars :: a -> Int -> m [Var]
  newVars a n = replicateM n (newVar a)

  -- | Add variables. @newVars_ a n = newVars a n >> return ()@, but maybe faster.
  newVars_ :: a -> Int -> m ()
  newVars_ a n = replicateM_ n (newVar a)

class NewVar m a => AddClause m a | a -> m where
  addClause :: a -> Clause -> m ()

class AddClause m a => AddCardinality m a | a -> m where
  {-# MINIMAL addAtLeast #-}

  -- | Add a cardinality constraints /atleast({l1,l2,..},n)/.
  addAtLeast
    :: a
    -> [Lit] -- ^ set of literals /{l1,l2,..}/ (duplicated elements are ignored)
    -> Int   -- ^ /n/
    -> m ()

  -- | Add a cardinality constraints /atmost({l1,l2,..},n)/.
  addAtMost
    :: a
    -> [Lit] -- ^ set of literals /{l1,l2,..}/ (duplicated elements are ignored)
    -> Int   -- ^ /n/
    -> m ()
  addAtMost a lits n = do
    addAtLeast a (map litNot lits) (length lits - n)

  -- | Add a cardinality constraints /exactly({l1,l2,..},n)/.
  addExactly
    :: a
    -> [Lit] -- ^ set of literals /{l1,l2,..}/ (duplicated elements are ignored)
    -> Int   -- ^ /n/
    -> m ()
  addExactly a lits n = do
    addAtLeast a lits n
    addAtMost a lits n

class AddCardinality m a => AddPBLin m a | a -> m where
  {-# MINIMAL addPBAtLeast #-}

  -- | Add a pseudo boolean constraints /c1*l1 + c2*l2 + … ≥ n/.
  addPBAtLeast
    :: a
    -> PBLinSum -- ^ list of terms @[(c1,l1),(c2,l2),…]@
    -> Integer  -- ^ /n/
    -> m ()

  -- | Add a pseudo boolean constraints /c1*l1 + c2*l2 + … ≤ n/.
  addPBAtMost
    :: a
    -> PBLinSum -- ^ list of @[(c1,l1),(c2,l2),…]@
    -> Integer  -- ^ /n/
    -> m ()
  addPBAtMost a ts n = addPBAtLeast a [(-c,l) | (c,l) <- ts] (negate n)

  -- | Add a pseudo boolean constraints /c1*l1 + c2*l2 + … = n/.
  addPBExactly
    :: a
    -> PBLinSum -- ^ list of terms @[(c1,l1),(c2,l2),…]@
    -> Integer  -- ^ /n/
    -> m ()
  addPBExactly a ts n = do
    addPBAtLeast a ts n
    addPBAtMost a ts n

  -- | Add a soft pseudo boolean constraints /sel ⇒ c1*l1 + c2*l2 + … ≥ n/.
  addPBAtLeastSoft
    :: a
    -> Lit             -- ^ Selector literal @sel@
    -> PBLinSum        -- ^ list of terms @[(c1,l1),(c2,l2),…]@
    -> Integer         -- ^ /n/
    -> m ()
  addPBAtLeastSoft a sel lhs rhs = do
    let (lhs2,rhs2) = normalizePBLinAtLeast (lhs,rhs)
    addPBAtLeast a ((rhs2, litNot sel) : lhs2) rhs2

  -- | Add a soft pseudo boolean constraints /sel ⇒ c1*l1 + c2*l2 + … ≤ n/.
  addPBAtMostSoft
    :: a
    -> Lit             -- ^ Selector literal @sel@
    -> PBLinSum        -- ^ list of terms @[(c1,l1),(c2,l2),…]@
    -> Integer         -- ^ /n/
    -> m ()
  addPBAtMostSoft a sel lhs rhs =
    addPBAtLeastSoft a sel [(negate c, lit) | (c,lit) <- lhs] (negate rhs)

  -- | Add a soft pseudo boolean constraints /sel ⇒ c1*l1 + c2*l2 + … = n/.
  addPBExactlySoft
    :: a
    -> Lit             -- ^ Selector literal @sel@
    -> PBLinSum        -- ^ list of terms @[(c1,l1),(c2,l2),…]@
    -> Integer         -- ^ /n/
    -> m ()
  addPBExactlySoft a sel lhs rhs = do
    addPBAtLeastSoft a sel lhs rhs
    addPBAtMostSoft a sel lhs rhs

class AddPBLin m a => AddPBNL m a | a -> m where
  {-# MINIMAL addPBNLAtLeast #-}

  -- | Add a non-linear pseudo boolean constraints /c1*ls1 + c2*ls2 + … ≥ n/.
  addPBNLAtLeast
    :: a
    -> PBSum   -- ^ List of terms @[(c1,ls1),(c2,ls2),…]@
    -> Integer -- ^ /n/
    -> m ()

  -- | Add a non-linear pseudo boolean constraints /c1*ls1 + c2*ls2 + … ≥ n/.
  addPBNLAtMost
    :: a
    -> PBSum   -- ^ List of terms @[(c1,ls1),(c2,ls2),…]@
    -> Integer -- ^ /n/
    -> m ()
  addPBNLAtMost a ts n = addPBNLAtLeast a [(-c,ls) | (c,ls) <- ts] (negate n)

  -- | Add a non-linear pseudo boolean constraints /c1*ls1 + c2*ls2 + … = n/.
  addPBNLExactly
    :: a
    -> PBSum   -- ^ List of terms @[(c1,ls1),(c2,ls2),…]@
    -> Integer -- ^ /n/
    -> m ()
  addPBNLExactly a ts n = do
    addPBNLAtLeast a ts n
    addPBNLAtMost a ts n

  -- | Add a soft non-linear pseudo boolean constraints /sel ⇒ c1*ls1 + c2*ls2 + … ≥ n/.
  addPBNLAtLeastSoft
    :: a
    -> Lit     -- ^ Selector literal @sel@
    -> PBSum   -- ^ List of terms @[(c1,ls1),(c2,ls2),…]@
    -> Integer -- ^ /n/
    -> m ()
  addPBNLAtLeastSoft a sel lhs rhs = do
    let n = rhs - sum [min c 0 | (c,_) <- lhs]
    addPBNLAtLeast a ((n, [litNot sel]) : lhs) rhs

  -- | Add a soft non-linear pseudo boolean constraints /sel ⇒ c1*ls1 + c2*ls2 + … ≤ n/.
  addPBNLAtMostSoft
    :: a
    -> Lit     -- ^ Selector literal @sel@
    -> PBSum   -- ^ List of terms @[(c1,ls1),(c2,ls2),…]@
    -> Integer -- ^ /n/
    -> m ()
  addPBNLAtMostSoft a sel lhs rhs =
    addPBNLAtLeastSoft a sel [(negate c, ls) | (c,ls) <- lhs] (negate rhs)

  -- | Add a soft non-linear pseudo boolean constraints /lit ⇒ c1*ls1 + c2*ls2 + … = n/.
  addPBNLExactlySoft
    :: a
    -> Lit     -- ^ Selector literal @sel@
    -> PBSum   -- ^ List of terms @[(c1,ls1),(c2,ls2),…]@
    -> Integer -- ^ /n/
    -> m ()
  addPBNLExactlySoft a sel lhs rhs = do
    addPBNLAtLeastSoft a sel lhs rhs
    addPBNLAtMostSoft a sel lhs rhs

class AddClause m a => AddXORClause m a | a -> m where
  {-# MINIMAL addXORClause #-}

  -- | Add a parity constraint /l1 ⊕ l2 ⊕ … ⊕ ln = rhs/
  addXORClause
    :: a
    -> [Lit]  -- ^ literals @[l1, l2, …, ln]@
    -> Bool   -- ^ /rhs/
    -> m ()

  -- | Add a soft parity constraint /sel ⇒ l1 ⊕ l2 ⊕ … ⊕ ln = rhs/
  addXORClauseSoft
    :: a
    -> Lit    -- ^ Selector literal @sel@
    -> [Lit]  -- ^ literals @[l1, l2, …, ln]@
    -> Bool   -- ^ /rhs/
    -> m ()
  addXORClauseSoft a sel lits rhs = do
    reified <- newVar a
    addXORClause a (litNot reified : lits) rhs
    addClause a [litNot sel, reified] -- sel ⇒ reified

-- | Add a type-2 SOS constraint
--
-- At most two adjacnt literals can be true.
addSOS2 :: AddClause m a => a -> [Lit] -> m ()
addSOS2 a xs =
  forM_ (nonAdjacentPairs xs) $ \(x1,x2) -> do
    addClause a [litNot v | v <- [x1,x2]]
  where
    nonAdjacentPairs :: [a] -> [(a,a)]
    nonAdjacentPairs (x1:x2:xs) = [(x1,x3) | x3 <- xs] ++ nonAdjacentPairs (x2:xs)
    nonAdjacentPairs _ = []

-- | Evaluate type-2 SOS constraint
evalSOS2 :: IModel m => m -> [Lit] -> Bool
evalSOS2 m = f
  where
    f [] = True
    f [_] = True
    f (l1 : l2 : ls)
      | evalLit m l1 = all (not . evalLit m) ls
      | otherwise = f (l2 : ls)