{-# LANGUAGE ScopedTypeVariables, BangPatterns, FlexibleInstances, MultiParamTypeClasses, FunctionalDependencies #-}
module ToySolver.SAT.Types
(
Var
, VarSet
, VarMap
, validVar
, IModel (..)
, Model
, restrictModel
, Lit
, LitSet
, LitMap
, litUndef
, validLit
, literal
, litNot
, litVar
, litPolarity
, evalLit
, Clause
, normalizeClause
, instantiateClause
, clauseSubsume
, evalClause
, clauseToPBLinAtLeast
, PackedClause
, packClause
, unpackClause
, AtLeast
, Exactly
, normalizeAtLeast
, instantiateAtLeast
, evalAtLeast
, evalExactly
, PBLinTerm
, PBLinSum
, PBLinAtLeast
, PBLinExactly
, normalizePBLinSum
, normalizePBLinAtLeast
, normalizePBLinExactly
, instantiatePBLinAtLeast
, instantiatePBLinExactly
, cutResolve
, cardinalityReduction
, negatePBLinAtLeast
, evalPBLinSum
, evalPBLinAtLeast
, evalPBLinExactly
, pbLinLowerBound
, pbLinUpperBound
, pbLinSubsume
, PBTerm
, PBSum
, evalPBSum
, evalPBConstraint
, evalPBFormula
, pbLowerBound
, pbUpperBound
, removeNegationFromPBSum
, XORClause
, normalizeXORClause
, instantiateXORClause
, evalXORClause
, NewVar (..)
, AddClause (..)
, AddCardinality (..)
, AddPBLin (..)
, AddPBNL (..)
, AddXORClause (..)
) where
import Control.Monad
import Control.Exception
import Data.Array.Unboxed
import Data.Ord
import Data.List
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
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
type Model = UArray Var Bool
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
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 #-}
literal :: Var
-> Bool
-> Lit
literal v polarity =
assert (validVar v) $ if polarity then v else litNot v
{-# INLINE litNot #-}
litNot :: Lit -> Lit
litNot l = assert (validLit l) $ negate l
{-# INLINE litVar #-}
litVar :: Lit -> Var
litVar l = assert (validLit l) $ abs l
{-# INLINE litPolarity #-}
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))
type Clause = [Lit]
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 PackedClause = VU.Vector Lit
packClause :: Clause -> PackedClause
packClause = VU.fromList
unpackClause :: PackedClause -> Clause
unpackClause = 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)
normalizePBLinSum :: (PBLinSum, Integer) -> (PBLinSum, Integer)
normalizePBLinSum = step2 . step1
where
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
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
normalizePBLinAtLeast :: PBLinAtLeast -> PBLinAtLeast
normalizePBLinAtLeast a =
case step1 a of
(xs,n)
| n > 0 -> step4 $ step3 (xs,n)
| otherwise -> ([], 0)
where
step1 :: PBLinAtLeast -> PBLinAtLeast
step1 (xs,n) =
case normalizePBLinSum (xs,-n) of
(ys,m) -> (ys, -m)
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)
step4 :: PBLinAtLeast -> PBLinAtLeast
step4 (xs,n) =
case SubsetSum.minSubsetSum (V.fromList [c | (c,_) <- xs]) n of
Just (m, _) -> (xs, m)
Nothing -> ([], 1)
normalizePBLinExactly :: PBLinExactly -> PBLinExactly
normalizePBLinExactly a =
case step1 $ a of
(xs,n)
| n >= 0 -> step3 $ step2 (xs, n)
| otherwise -> ([], 1)
where
step1 :: PBLinExactly -> PBLinExactly
step1 (xs,n) =
case normalizePBLinSum (xs,-n) of
(ys,m) -> (ys, -m)
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)
where
d = foldl1' gcd [c | (c,_) <- xs]
step3 :: PBLinExactly -> PBLinExactly
step3 constr@(xs,n) =
case SubsetSum.subsetSum (V.fromList [c | (c,_) <- xs]) n of
Just _ -> constr
Nothing -> ([], 1)
{-# 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]
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
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
type XORClause = ([Lit], Bool)
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)]
{-# 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 #-}
newVar :: a -> m Var
newVars :: a -> Int -> m [Var]
newVars a n = replicateM n (newVar a)
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 #-}
addAtLeast
:: a
-> [Lit]
-> Int
-> m ()
addAtMost
:: a
-> [Lit]
-> Int
-> m ()
addAtMost a lits n = do
addAtLeast a (map litNot lits) (length lits - n)
addExactly
:: a
-> [Lit]
-> Int
-> 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 #-}
addPBAtLeast
:: a
-> PBLinSum
-> Integer
-> m ()
addPBAtMost
:: a
-> PBLinSum
-> Integer
-> m ()
addPBAtMost a ts n = addPBAtLeast a [(-c,l) | (c,l) <- ts] (negate n)
addPBExactly
:: a
-> PBLinSum
-> Integer
-> m ()
addPBExactly a ts n = do
addPBAtLeast a ts n
addPBAtMost a ts n
addPBAtLeastSoft
:: a
-> Lit
-> PBLinSum
-> Integer
-> m ()
addPBAtLeastSoft a sel lhs rhs = do
let (lhs2,rhs2) = normalizePBLinAtLeast (lhs,rhs)
addPBAtLeast a ((rhs2, litNot sel) : lhs2) rhs2
addPBAtMostSoft
:: a
-> Lit
-> PBLinSum
-> Integer
-> m ()
addPBAtMostSoft a sel lhs rhs =
addPBAtLeastSoft a sel [(negate c, lit) | (c,lit) <- lhs] (negate rhs)
addPBExactlySoft
:: a
-> Lit
-> PBLinSum
-> Integer
-> 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 #-}
addPBNLAtLeast
:: a
-> PBSum
-> Integer
-> m ()
addPBNLAtMost
:: a
-> PBSum
-> Integer
-> m ()
addPBNLAtMost a ts n = addPBNLAtLeast a [(-c,ls) | (c,ls) <- ts] (negate n)
addPBNLExactly
:: a
-> PBSum
-> Integer
-> m ()
addPBNLExactly a ts n = do
addPBNLAtLeast a ts n
addPBNLAtMost a ts n
addPBNLAtLeastSoft
:: a
-> Lit
-> PBSum
-> Integer
-> m ()
addPBNLAtLeastSoft a sel lhs rhs = do
let n = rhs - sum [min c 0 | (c,_) <- lhs]
addPBNLAtLeast a ((n, [litNot sel]) : lhs) rhs
addPBNLAtMostSoft
:: a
-> Lit
-> PBSum
-> Integer
-> m ()
addPBNLAtMostSoft a sel lhs rhs =
addPBNLAtLeastSoft a sel [(negate c, ls) | (c,ls) <- lhs] (negate rhs)
addPBNLExactlySoft
:: a
-> Lit
-> PBSum
-> Integer
-> 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 #-}
addXORClause
:: a
-> [Lit]
-> Bool
-> m ()
addXORClauseSoft
:: a
-> Lit
-> [Lit]
-> Bool
-> m ()
addXORClauseSoft a sel lits rhs = do
reified <- newVar a
addXORClause a (litNot reified : lits) rhs
addClause a [litNot sel, reified]