{-# 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.cs.kent.ac.uk/pubs/2011/3094/content.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 Lit -> Lit -> Lit
forall a. Num a => a -> a -> a
+ VarSet -> Lit
IntSet.size VarSet
vs
      , cnfNumClauses :: Lit
CNF.cnfNumClauses = CNF -> Lit
CNF.cnfNumClauses CNF
cnf Lit -> Lit -> Lit
forall a. Num a => a -> a -> a
+ VarSet -> Lit
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 [-Lit
xp,-Lit
xn] | (Lit
xp,Lit
xn) <- VarMap (Lit, Lit) -> [(Lit, Lit)]
forall a. IntMap a -> [a]
IntMap.elems VarMap (Lit, Lit)
forward ]
      }
    f :: PackedLit -> PackedLit
f PackedLit
x =
      case Lit -> VarMap (Lit, Lit) -> Maybe (Lit, Lit)
forall a. Lit -> IntMap a -> Maybe a
IntMap.lookup (Lit -> Lit
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 (Lit -> PackedLit) -> Lit -> PackedLit
forall a b. (a -> b) -> a -> b
$ if PackedLit
x PackedLit -> PackedLit -> Bool
forall a. Ord a => a -> a -> Bool
> PackedLit
0 then Lit
xp else Lit
xn
    forward :: VarMap (Lit, Lit)
forward =
      [(Lit, (Lit, Lit))] -> VarMap (Lit, Lit)
forall a. [(Lit, a)] -> IntMap a
IntMap.fromList
      [ (Lit
x, (Lit
x,Lit
x'))
      | (Lit
x,Lit
x') <- Clause -> Clause -> [(Lit, Lit)]
forall a b. [a] -> [b] -> [(a, b)]
zip (VarSet -> Clause
IntSet.toList VarSet
vs) [CNF -> Lit
CNF.cnfNumVars CNF
cnf Lit -> Lit -> Lit
forall a. Num a => a -> a -> a
+ Lit
1 ..]
      ]
    backward :: VarMap Lit
backward = [(Lit, Lit)] -> VarMap Lit
forall a. [(Lit, a)] -> IntMap a
IntMap.fromList ([(Lit, Lit)] -> VarMap Lit) -> [(Lit, Lit)] -> VarMap Lit
forall a b. (a -> b) -> a -> b
$ [[(Lit, Lit)]] -> [(Lit, Lit)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[(Lit, Lit)]] -> [(Lit, Lit)]) -> [[(Lit, Lit)]] -> [(Lit, Lit)]
forall a b. (a -> b) -> a -> b
$
      [ [(Lit
xp,Lit
x), (Lit
xn,-Lit
x)]
      | (Lit
x, (Lit
xp,Lit
xn)) <- VarMap (Lit, Lit) -> [(Lit, (Lit, Lit))]
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 (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 -> Lit -> Bool
forall m. IModel m => m -> Lit -> Bool
SAT.evalLit Model
m Lit
xp then [Lit
x]
    else if Model -> Lit -> Bool
forall m. IModel m => m -> Lit -> Bool
SAT.evalLit Model
m Lit
xn then [-Lit
x]
    else []
  | (Lit
x, (Lit
xp,Lit
xn)) <- VarMap (Lit, Lit) -> [(Lit, (Lit, Lit))]
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 <- VarMap Lit -> Clause
forall a. IntMap a -> Clause
IntMap.keys (Info -> VarMap Lit
backwardMap Info
info), Model -> Lit -> Bool
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
  Solver -> Lit -> IO ()
forall (m :: * -> *) a. NewVar m a => a -> Lit -> m ()
SAT.newVars_ Solver
solver (CNF -> Lit
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 :: Lit
lim = VarMap (Lit, Lit) -> Lit
forall a. IntMap a -> Lit
IntMap.size (Info -> VarMap (Lit, Lit)
forwardMap Info
info)

      loop :: Lit -> IO ()
loop !Lit
n | Lit
n Lit -> Lit -> Bool
forall a. Ord a => a -> a -> Bool
> Lit
lim = () -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
      loop !Lit
n = do
        Lit
sel <- Solver -> IO Lit
forall (m :: * -> *) a. NewVar m a => a -> m Lit
SAT.newVar Solver
solver
        Solver -> Lit -> PBLinSum -> Integer -> IO ()
forall (m :: * -> *) a.
AddPBLin m a =>
a -> Lit -> PBLinSum -> Integer -> m ()
SAT.addPBAtMostSoft Solver
solver Lit
sel [(Integer
1,Lit
l) | Lit
l <- VarMap Lit -> Clause
forall a. IntMap a -> Clause
IntMap.keys (Info -> VarMap Lit
backwardMap Info
info)] (Lit -> Integer
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]
              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 [-Lit
sel]
        Lit -> IO ()
loop (Lit
nLit -> Lit -> Lit
forall a. Num a => a -> a -> a
+Lit
1)

  Lit -> IO ()
loop Lit
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 a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (CNF -> IO CNF) -> CNF -> IO CNF
forall a b. (a -> b) -> a -> b
$
    CNF.CNF
    { cnfNumVars :: Lit
CNF.cnfNumVars = CNF -> Lit
CNF.cnfNumVars CNF
formula
    , cnfNumClauses :: Lit
CNF.cnfNumClauses = [VarSet] -> Lit
forall a. [a] -> Lit
forall (t :: * -> *) a. Foldable t => t a -> Lit
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
. (Lit -> Lit) -> Clause -> Clause
forall a b. (a -> b) -> [a] -> [b]
map Lit -> Lit
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 [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 = [VarSet] -> Lit
forall a. [a] -> Lit
forall (t :: * -> *) a. Foldable t => t a -> Lit
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
. (Lit -> Lit) -> Clause -> Clause
forall a b. (a -> b) -> [a] -> [b]
map Lit -> Lit
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
. (Lit -> Lit) -> Clause -> Clause
forall a b. (a -> b) -> [a] -> [b]
map Lit -> Lit
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 a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (CNF -> IO CNF) -> CNF -> IO CNF
forall a b. (a -> b) -> a -> b
$
    CNF.CNF
    { cnfNumVars :: Lit
CNF.cnfNumVars = Lit
nv
    , cnfNumClauses :: Lit
CNF.cnfNumClauses = [PackedClause] -> Lit
forall a. [a] -> Lit
forall (t :: * -> *) a. Foldable t => t a -> Lit
length [PackedClause]
implicates
    , cnfClauses :: [PackedClause]
CNF.cnfClauses = [PackedClause]
implicates
    }