{-# 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
  , 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
  }

-- | 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
    { 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
      ]

{-
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 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]

-- | 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 [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

-- | 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
  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
    }

-- | 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 [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
    }