{-# Language BangPatterns #-}
{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_HADDOCK show-extensions #-}
----------------------------------------------------------------------
-- |
-- Module      :  ToySolver.SAT.ExistentialQuantification
-- Copyright   :  (c) Masahiro Sakai 2017
-- License     :  BSD-style
--
-- Maintainer  :  masahiro.sakai@gmail.com
-- Stability   :  provisional
-- Portability :  non-portable
--
-- References:
--
-- * [BrauerKingKriener2011] Jörg Brauer, Andy King, and Jael Kriener,
--   "Existential quantification as incremental SAT," in Computer Aided
--   Verification (CAV 2011), G. Gopalakrishnan and S. Qadeer, Eds.
--   pp. 191-207.
--   <https://www.embedded.rwth-aachen.de/lib/exe/fetch.php?media=bib:bkk11a.pdf>
--
----------------------------------------------------------------------
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
  }

-- | Given a set of variables \(X = \{x_1, \ldots, x_k\}\) and CNF formula \(\phi\), this function
--
-- * duplicates \(X\) with \(X^+ = \{x^+_1,\ldots,x^+_k\}\) and \(X^- = \{x^-_1,\ldots,x^-_k\}\),
--
-- * replaces positive literals \(x_i\) with \(x^+_i\), and negative literals \(\neg x_i\) with \(x^-_i\), and
--
-- * adds constraints \(\neg x^+_i \vee \neg x^-_i\).
dualRailEncoding
  :: SAT.VarSet -- ^ \(X\)
  -> CNF.CNF    -- ^ \(\phi\)
  -> (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
      ]

{-
forwardLit :: Info -> Lit -> Lit
forwardLit info l =
  case IntMap.lookup (abs l) (forwardMap info) of
    Nothing -> l
    Just (xp,xn) -> if l > 0 then xp else xn
-}

-- -------------------------------------------------------------------

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" #-}
-- | Given a set of variables \(X = \{x_1, \ldots, x_k\}\) and CNF formula \(\phi\),
-- this function computes shortest implicants of \(\phi\) in terms of \(X\).
-- Variables except \(X\) are treated as if they are existentially quantified.
--
-- Resulting shortest implicants form a DNF (disjunctive normal form) formula that is
-- equivalent to the original (existentially quantified) formula.
shortestImplicants
  :: SAT.VarSet  -- ^ \(X\)
  -> CNF.CNF     -- ^ \(\phi\)
  -> 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

-- | Given a set of variables \(X = \{x_1, \ldots, x_k\}\) and CNF formula \(\phi\),
-- this function computes shortest implicants of \(\exists X. \phi\).
--
-- Resulting shortest implicants form a DNF (disjunctive normal form) formula that is
-- equivalent to the original formula \(\exists X. \phi\).
shortestImplicantsE
  :: SAT.VarSet  -- ^ \(X\)
  -> CNF.CNF     -- ^ \(\phi\)
  -> 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

-- | Given a CNF formula \(\phi\), this function returns another CNF formula \(\psi\)
-- that is equivalent to \(\neg\phi\).
negateCNF
  :: CNF.CNF    -- ^ \(\phi\)
  -> IO CNF.CNF -- ^ \(\psi \equiv \neg\phi\)
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
    }

-- | Given a set of variables \(X = \{x_1, \ldots, x_k\}\) and CNF formula \(\phi\),
-- this function computes a CNF formula \(\psi\) that is equivalent to \(\exists X. \phi\)
-- (i.e. \((\exists X. \phi) \leftrightarrow \psi\)).
project
  :: SAT.VarSet  -- ^ \(X\)
  -> CNF.CNF     -- ^ \(\phi\)
  -> IO CNF.CNF  -- ^ \(\psi\)
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
    }