{-# Language BangPatterns #-}
{-# OPTIONS_GHC -Wall #-}
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
{ forwardMap :: SAT.VarMap (SAT.Var, SAT.Var)
, backwardMap :: SAT.VarMap SAT.Lit
}
dualRailEncoding
:: SAT.VarSet
-> CNF.CNF
-> (CNF.CNF, Info)
dualRailEncoding vs cnf =
( cnf'
, Info
{ forwardMap = forward
, backwardMap = backward
}
)
where
cnf' =
CNF.CNF
{ CNF.cnfNumVars = CNF.cnfNumVars cnf + IntSet.size vs
, CNF.cnfNumClauses = CNF.cnfNumClauses cnf + IntSet.size vs
, CNF.cnfClauses = [ VG.map f c | c <- CNF.cnfClauses cnf ] ++ [SAT.packClause [-xp,-xn] | (xp,xn) <- IntMap.elems forward]
}
f x =
case IntMap.lookup (abs x) forward of
Nothing -> x
Just (xp,xn) -> if x > 0 then xp else xn
forward =
IntMap.fromList
[ (x, (x,x'))
| (x,x') <- zip (IntSet.toList vs) [CNF.cnfNumVars cnf + 1 ..]
]
backward = IntMap.fromList $ concat $
[ [(xp,x), (xn,-x)]
| (x, (xp,xn)) <- IntMap.toList forward
]
cube :: Info -> SAT.Model -> LitSet
cube info m = IntSet.fromList $ concat $
[ if SAT.evalLit m xp then [x]
else if SAT.evalLit m xn then [-x]
else []
| (x, (xp,xn)) <- IntMap.toList (forwardMap info)
]
blockingClause :: Info -> SAT.Model -> Clause
blockingClause info m = [-y | y <- IntMap.keys (backwardMap info), SAT.evalLit m y]
{-# DEPRECATED shortestImplicants "Use shortestImplicantsE instead" #-}
shortestImplicants
:: SAT.VarSet
-> CNF.CNF
-> IO [LitSet]
shortestImplicants xs formula =
shortestImplicantsE (IntSet.fromList [1 .. CNF.cnfNumVars formula] IntSet.\\ xs) formula
shortestImplicantsE
:: SAT.VarSet
-> CNF.CNF
-> IO [LitSet]
shortestImplicantsE xs formula = do
let (tau_formula, info) = dualRailEncoding (IntSet.fromList [1 .. CNF.cnfNumVars formula] IntSet.\\ xs) formula
solver <- SAT.newSolver
SAT.newVars_ solver (CNF.cnfNumVars tau_formula)
forM_ (CNF.cnfClauses tau_formula) $ \c -> do
SAT.addClause solver (SAT.unpackClause c)
ref <- newIORef []
let lim = IntMap.size (forwardMap info)
loop !n | n > lim = return ()
loop !n = do
sel <- SAT.newVar solver
SAT.addPBAtMostSoft solver sel [(1,l) | l <- IntMap.keys (backwardMap info)] (fromIntegral n)
let loop2 = do
b <- SAT.solveWith solver [sel]
when b $ do
m <- SAT.getModel solver
let c = cube info m
modifyIORef ref (c:)
SAT.addClause solver (blockingClause info m)
loop2
loop2
SAT.addClause solver [-sel]
loop (n+1)
loop 0
reverse <$> readIORef ref
negateCNF
:: CNF.CNF
-> IO CNF.CNF
negateCNF formula = do
implicants <- shortestImplicantsE IntSet.empty formula
return $
CNF.CNF
{ CNF.cnfNumVars = CNF.cnfNumVars formula
, CNF.cnfNumClauses = length implicants
, CNF.cnfClauses = map (SAT.packClause . map negate . IntSet.toList) implicants
}
project
:: SAT.VarSet
-> CNF.CNF
-> IO CNF.CNF
project xs cnf = do
let ys = IntSet.fromList [1 .. CNF.cnfNumVars cnf] IntSet.\\ xs
nv = if IntSet.null ys then 0 else IntSet.findMax ys
implicants <- shortestImplicantsE xs cnf
let cnf' =
CNF.CNF
{ CNF.cnfNumVars = nv
, CNF.cnfNumClauses = length implicants
, CNF.cnfClauses = map (SAT.packClause . map negate . IntSet.toList) implicants
}
negated_implicates <- shortestImplicantsE xs cnf'
let implicates = map (SAT.packClause . map negate . IntSet.toList) negated_implicates
return $
CNF.CNF
{ CNF.cnfNumVars = nv
, CNF.cnfNumClauses = length implicates
, CNF.cnfClauses = implicates
}