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