{-# Language BangPatterns #-}
{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_HADDOCK show-extensions #-}
module ToySolver.SAT.ExistentialQuantification
( project
, shortestImplicantsE
, negateCNF
) where
import Control.Monad
import qualified Data.IntMap as IntMap
import qualified Data.IntSet as IntSet
import Data.IORef
import qualified Data.Vector.Generic as VG
import ToySolver.FileFormat.CNF as CNF
import ToySolver.SAT as SAT
import ToySolver.SAT.Types as SAT
data Info
= Info
{ Info -> VarMap (Lit, Lit)
forwardMap :: SAT.VarMap (SAT.Var, SAT.Var)
, Info -> VarMap Lit
backwardMap :: SAT.VarMap SAT.Lit
}
dualRailEncoding
:: SAT.VarSet
-> CNF.CNF
-> (CNF.CNF, Info)
dualRailEncoding :: VarSet -> CNF -> (CNF, Info)
dualRailEncoding VarSet
vs CNF
cnf =
( CNF
cnf'
, Info
{ forwardMap :: VarMap (Lit, Lit)
forwardMap = VarMap (Lit, Lit)
forward
, backwardMap :: VarMap Lit
backwardMap = VarMap Lit
backward
}
)
where
cnf' :: CNF
cnf' =
CNF.CNF
{ cnfNumVars :: Lit
CNF.cnfNumVars = CNF -> Lit
CNF.cnfNumVars CNF
cnf forall a. Num a => a -> a -> a
+ VarSet -> Lit
IntSet.size VarSet
vs
, cnfNumClauses :: Lit
CNF.cnfNumClauses = CNF -> Lit
CNF.cnfNumClauses CNF
cnf forall a. Num a => a -> a -> a
+ VarSet -> Lit
IntSet.size VarSet
vs
, cnfClauses :: [PackedClause]
CNF.cnfClauses =
[ forall (v :: * -> *) a b.
(Vector v a, Vector v b) =>
(a -> b) -> v a -> v b
VG.map PackedLit -> PackedLit
f PackedClause
c | PackedClause
c <- CNF -> [PackedClause]
CNF.cnfClauses CNF
cnf ] forall a. [a] -> [a] -> [a]
++
[ Clause -> PackedClause
SAT.packClause [-Lit
xp,-Lit
xn] | (Lit
xp,Lit
xn) <- forall a. IntMap a -> [a]
IntMap.elems VarMap (Lit, Lit)
forward ]
}
f :: PackedLit -> PackedLit
f PackedLit
x =
case forall a. Lit -> IntMap a -> Maybe a
IntMap.lookup (forall a. Num a => a -> a
abs (PackedLit -> Lit
SAT.unpackLit PackedLit
x)) VarMap (Lit, Lit)
forward of
Maybe (Lit, Lit)
Nothing -> PackedLit
x
Just (Lit
xp,Lit
xn) -> Lit -> PackedLit
SAT.packLit forall a b. (a -> b) -> a -> b
$ if PackedLit
x forall a. Ord a => a -> a -> Bool
> PackedLit
0 then Lit
xp else Lit
xn
forward :: VarMap (Lit, Lit)
forward =
forall a. [(Lit, a)] -> IntMap a
IntMap.fromList
[ (Lit
x, (Lit
x,Lit
x'))
| (Lit
x,Lit
x') <- forall a b. [a] -> [b] -> [(a, b)]
zip (VarSet -> Clause
IntSet.toList VarSet
vs) [CNF -> Lit
CNF.cnfNumVars CNF
cnf forall a. Num a => a -> a -> a
+ Lit
1 ..]
]
backward :: VarMap Lit
backward = forall a. [(Lit, a)] -> IntMap a
IntMap.fromList forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall a b. (a -> b) -> a -> b
$
[ [(Lit
xp,Lit
x), (Lit
xn,-Lit
x)]
| (Lit
x, (Lit
xp,Lit
xn)) <- forall a. IntMap a -> [(Lit, a)]
IntMap.toList VarMap (Lit, Lit)
forward
]
cube :: Info -> SAT.Model -> LitSet
cube :: Info -> Model -> VarSet
cube Info
info Model
m = Clause -> VarSet
IntSet.fromList forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall a b. (a -> b) -> a -> b
$
[ if forall m. IModel m => m -> Lit -> Bool
SAT.evalLit Model
m Lit
xp then [Lit
x]
else if forall m. IModel m => m -> Lit -> Bool
SAT.evalLit Model
m Lit
xn then [-Lit
x]
else []
| (Lit
x, (Lit
xp,Lit
xn)) <- forall a. IntMap a -> [(Lit, a)]
IntMap.toList (Info -> VarMap (Lit, Lit)
forwardMap Info
info)
]
blockingClause :: Info -> SAT.Model -> Clause
blockingClause :: Info -> Model -> Clause
blockingClause Info
info Model
m = [-Lit
y | Lit
y <- forall a. IntMap a -> Clause
IntMap.keys (Info -> VarMap Lit
backwardMap Info
info), forall m. IModel m => m -> Lit -> Bool
SAT.evalLit Model
m Lit
y]
shortestImplicantsE
:: SAT.VarSet
-> CNF.CNF
-> IO [LitSet]
shortestImplicantsE :: VarSet -> CNF -> IO [VarSet]
shortestImplicantsE VarSet
xs CNF
formula = do
let (CNF
tau_formula, Info
info) = VarSet -> CNF -> (CNF, Info)
dualRailEncoding (Clause -> VarSet
IntSet.fromList [Lit
1 .. CNF -> Lit
CNF.cnfNumVars CNF
formula] VarSet -> VarSet -> VarSet
IntSet.\\ VarSet
xs) CNF
formula
Solver
solver <- IO Solver
SAT.newSolver
forall (m :: * -> *) a. NewVar m a => a -> Lit -> m ()
SAT.newVars_ Solver
solver (CNF -> Lit
CNF.cnfNumVars CNF
tau_formula)
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (CNF -> [PackedClause]
CNF.cnfClauses CNF
tau_formula) forall a b. (a -> b) -> a -> b
$ \PackedClause
c -> do
forall (m :: * -> *) a. AddClause m a => a -> Clause -> m ()
SAT.addClause Solver
solver (PackedClause -> Clause
SAT.unpackClause PackedClause
c)
IORef [VarSet]
ref <- forall a. a -> IO (IORef a)
newIORef []
let lim :: Lit
lim = forall a. IntMap a -> Lit
IntMap.size (Info -> VarMap (Lit, Lit)
forwardMap Info
info)
loop :: Lit -> IO ()
loop !Lit
n | Lit
n forall a. Ord a => a -> a -> Bool
> Lit
lim = forall (m :: * -> *) a. Monad m => a -> m a
return ()
loop !Lit
n = do
Lit
sel <- forall (m :: * -> *) a. NewVar m a => a -> m Lit
SAT.newVar Solver
solver
forall (m :: * -> *) a.
AddPBLin m a =>
a -> Lit -> PBLinSum -> Integer -> m ()
SAT.addPBAtMostSoft Solver
solver Lit
sel [(Integer
1,Lit
l) | Lit
l <- forall a. IntMap a -> Clause
IntMap.keys (Info -> VarMap Lit
backwardMap Info
info)] (forall a b. (Integral a, Num b) => a -> b
fromIntegral Lit
n)
let loop2 :: IO ()
loop2 = do
Bool
b <- Solver -> Clause -> IO Bool
SAT.solveWith Solver
solver [Lit
sel]
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
b forall a b. (a -> b) -> a -> b
$ do
Model
m <- Solver -> IO Model
SAT.getModel Solver
solver
let c :: VarSet
c = Info -> Model -> VarSet
cube Info
info Model
m
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef IORef [VarSet]
ref (VarSet
cforall a. a -> [a] -> [a]
:)
forall (m :: * -> *) a. AddClause m a => a -> Clause -> m ()
SAT.addClause Solver
solver (Info -> Model -> Clause
blockingClause Info
info Model
m)
IO ()
loop2
IO ()
loop2
forall (m :: * -> *) a. AddClause m a => a -> Clause -> m ()
SAT.addClause Solver
solver [-Lit
sel]
Lit -> IO ()
loop (Lit
nforall a. Num a => a -> a -> a
+Lit
1)
Lit -> IO ()
loop Lit
0
forall a. [a] -> [a]
reverse forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. IORef a -> IO a
readIORef IORef [VarSet]
ref
negateCNF
:: CNF.CNF
-> IO CNF.CNF
negateCNF :: CNF -> IO CNF
negateCNF CNF
formula = do
[VarSet]
implicants <- VarSet -> CNF -> IO [VarSet]
shortestImplicantsE VarSet
IntSet.empty CNF
formula
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$
CNF.CNF
{ cnfNumVars :: Lit
CNF.cnfNumVars = CNF -> Lit
CNF.cnfNumVars CNF
formula
, cnfNumClauses :: Lit
CNF.cnfNumClauses = forall (t :: * -> *) a. Foldable t => t a -> Lit
length [VarSet]
implicants
, cnfClauses :: [PackedClause]
CNF.cnfClauses = forall a b. (a -> b) -> [a] -> [b]
map (Clause -> PackedClause
SAT.packClause forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall a. Num a => a -> a
negate forall b c a. (b -> c) -> (a -> b) -> a -> c
. VarSet -> Clause
IntSet.toList) [VarSet]
implicants
}
project
:: SAT.VarSet
-> CNF.CNF
-> IO CNF.CNF
project :: VarSet -> CNF -> IO CNF
project VarSet
xs CNF
cnf = do
let ys :: VarSet
ys = Clause -> VarSet
IntSet.fromList [Lit
1 .. CNF -> Lit
CNF.cnfNumVars CNF
cnf] VarSet -> VarSet -> VarSet
IntSet.\\ VarSet
xs
nv :: Lit
nv = if VarSet -> Bool
IntSet.null VarSet
ys then Lit
0 else VarSet -> Lit
IntSet.findMax VarSet
ys
[VarSet]
implicants <- VarSet -> CNF -> IO [VarSet]
shortestImplicantsE VarSet
xs CNF
cnf
let cnf' :: CNF
cnf' =
CNF.CNF
{ cnfNumVars :: Lit
CNF.cnfNumVars = Lit
nv
, cnfNumClauses :: Lit
CNF.cnfNumClauses = forall (t :: * -> *) a. Foldable t => t a -> Lit
length [VarSet]
implicants
, cnfClauses :: [PackedClause]
CNF.cnfClauses = forall a b. (a -> b) -> [a] -> [b]
map (Clause -> PackedClause
SAT.packClause forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall a. Num a => a -> a
negate forall b c a. (b -> c) -> (a -> b) -> a -> c
. VarSet -> Clause
IntSet.toList) [VarSet]
implicants
}
[VarSet]
negated_implicates <- VarSet -> CNF -> IO [VarSet]
shortestImplicantsE VarSet
xs CNF
cnf'
let implicates :: [PackedClause]
implicates = forall a b. (a -> b) -> [a] -> [b]
map (Clause -> PackedClause
SAT.packClause forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall a. Num a => a -> a
negate forall b c a. (b -> c) -> (a -> b) -> a -> c
. VarSet -> Clause
IntSet.toList) [VarSet]
negated_implicates
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$
CNF.CNF
{ cnfNumVars :: Lit
CNF.cnfNumVars = Lit
nv
, cnfNumClauses :: Lit
CNF.cnfNumClauses = forall (t :: * -> *) a. Foldable t => t a -> Lit
length [PackedClause]
implicates
, cnfClauses :: [PackedClause]
CNF.cnfClauses = [PackedClause]
implicates
}