msakai / toysolver / 767

Committed 22 May 2025 12:57PM UTC coverage: 71.847% (-0.06%) from 71.906%

Build # 767

Build Type

push

github

Committed by

web-flow

Commit Message

Merge f4d92f6d1 into c10d256d2

Run Details

11104 of 15455 relevant lines covered (71.85%)

0.72 hits per line

Source File
Press 'n' to go to next uncovered line, 'b' for previous

60.87

/src/ToySolver/QBF.hs

{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_HADDOCK show-extensions #-}
{-# LANGUAGE BangPatterns #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  ToySolver.QBF
-- Copyright   :  (c) Masahiro Sakai 2016
-- License     :  BSD-style
--
-- Maintainer  :  masahiro.sakai@gmail.com
-- Stability   :  provisional
-- Portability :  non-portable
--
-- Reference:
--
-- * Mikoláš Janota, William Klieber, Joao Marques-Silva, Edmund Clarke.
--   Solving QBF with Counterexample Guided Refinement.
--   In Theory and Applications of Satisfiability Testing (SAT 2012), pp. 114-128.
--   <https://doi.org/10.1007/978-3-642-31612-8_10>
--   <https://www.cs.cmu.edu/~wklieber/papers/qbf-cegar-sat-2012.pdf>
--
-----------------------------------------------------------------------------
module ToySolver.QBF
  ( Quantifier (..)
  , Prefix
  , normalizePrefix
  , quantifyFreeVariables
  , Matrix
  , litToMatrix
  , solve
  , solveNaive
  , solveCEGAR
  , solveCEGARIncremental
  , solveQE
  , solveQE_CNF
  ) where

import Control.Monad
import Control.Monad.State.Strict
import Control.Monad.Trans.Except
import qualified Data.IntMap as IntMap
import qualified Data.IntSet as IntSet
import Data.Function (on)
import Data.List (foldl')
import qualified Data.List.NonEmpty as NonEmpty
import Data.Maybe

import ToySolver.Data.Boolean
import ToySolver.FileFormat.CNF (Quantifier (..))
import qualified ToySolver.FileFormat.CNF as CNF
import qualified ToySolver.SAT as SAT
import ToySolver.SAT.Types (LitSet, VarSet, VarMap)
import qualified ToySolver.SAT.Encoder.Tseitin as Tseitin
import ToySolver.SAT.Store.CNF

import qualified ToySolver.SAT.ExistentialQuantification as QE

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

type Prefix = [(Quantifier, VarSet)]

normalizePrefix :: Prefix -> Prefix
normalizePrefix = groupQuantifiers . removeEmptyQuantifiers

removeEmptyQuantifiers :: Prefix -> Prefix
removeEmptyQuantifiers = filter (\(_,xs) -> not (IntSet.null xs))

groupQuantifiers :: Prefix -> Prefix
groupQuantifiers = map f . NonEmpty.groupBy ((==) `on` fst)
  where
    f qs = (fst (NonEmpty.head qs), IntSet.unions [xs | (_,xs) <- NonEmpty.toList qs])

quantifyFreeVariables :: Int -> Prefix -> Prefix
quantifyFreeVariables nv prefix
  | IntSet.null rest = prefix
  | otherwise = (E, rest) : prefix
  where
    rest = IntSet.fromList [1..nv] `IntSet.difference` IntSet.unions [vs | (_q, vs) <- prefix]

prefixStartWithA :: Prefix -> Bool
prefixStartWithA ((A,_) : _) = True
prefixStartWithA _ = False

prefixStartWithE :: Prefix -> Bool
prefixStartWithE ((E,_) : _) = True
prefixStartWithE _ = False

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

type Matrix = Tseitin.Formula

litToMatrix :: SAT.Lit -> Matrix
litToMatrix = Tseitin.Atom

reduct :: Matrix -> LitSet -> Matrix
reduct m ls = Tseitin.simplify $ Tseitin.fold s m
  where
    s l
      |   l  `IntSet.member` ls = true
      | (-l) `IntSet.member` ls = false
      | otherwise = litToMatrix l

substVarMap :: Matrix -> VarMap Matrix -> Matrix
substVarMap m s = Tseitin.simplify $ Tseitin.fold f m
  where
    f l = do
      let v = abs l
      (if l > 0 then id else notB) $ IntMap.findWithDefault (litToMatrix v) v s

-- XXX
prenexAnd :: (Int, Prefix, Matrix) -> (Int, Prefix, Matrix) -> (Int, Prefix, Matrix)
prenexAnd (nv1, prefix1, matrix1) (nv2, prefix2, matrix2) =
  evalState (f [] IntSet.empty IntMap.empty IntMap.empty prefix1 prefix2) (nv1 `max` nv2)
  where
    f :: Prefix -> VarSet
      -> VarMap Tseitin.Formula -> VarMap Tseitin.Formula
      -> Prefix -> Prefix
      -> State Int (Int, Prefix, Matrix)
    f prefix _bvs subst1 subst2 [] [] = do
      nv <- get
      return (nv, prefix, Tseitin.simplify (substVarMap matrix1 subst1 .&&. substVarMap matrix2 subst2))
    f prefix bvs subst1 subst2 ((A,xs1) : prefix1') ((A,xs2) : prefix2') = do
      let xs = IntSet.union xs1 xs2
          ys = IntSet.intersection bvs xs
      nv <- get
      put (nv + IntSet.size ys)
      let s  = IntMap.fromList $ zip (IntSet.toList ys) [(nv+1) ..]
          xs' = (xs `IntSet.difference` bvs) `IntSet.union` IntSet.fromList (IntMap.elems s)
          subst1' = fmap litToMatrix (IntMap.filterWithKey (\x _ -> x `IntSet.member` xs1) s) `IntMap.union` subst1
          subst2' = fmap litToMatrix (IntMap.filterWithKey (\x _ -> x `IntSet.member` xs2) s) `IntMap.union` subst2
      f (prefix ++ [(A, xs')]) (bvs `IntSet.union` xs') subst1' subst2' prefix1' prefix2'
    f prefix bvs subst1 subst2 ((q,xs) : prefix1') prefix2 | q==E || not (prefixStartWithE prefix2) = do
      let ys = IntSet.intersection bvs xs
      nv <- get
      put (nv + IntSet.size ys)
      let s  = IntMap.fromList $ zip (IntSet.toList ys) [(nv+1) ..]
          xs' = (xs `IntSet.difference` bvs) `IntSet.union` IntSet.fromList (IntMap.elems s)
          subst1' = fmap litToMatrix s `IntMap.union` subst1
      f (prefix ++ [(q, xs')]) (bvs `IntSet.union` xs') subst1' subst2 prefix1' prefix2
    f prefix bvs subst1 subst2 prefix1 ((q,xs) : prefix2')  = do
      let ys = IntSet.intersection bvs xs
      nv <- get
      put (nv + IntSet.size ys)
      let s  = IntMap.fromList $ zip (IntSet.toList ys) [(nv+1) ..]
          xs' = (xs `IntSet.difference` bvs) `IntSet.union` IntSet.fromList (IntMap.elems s)
          subst2' = fmap litToMatrix s `IntMap.union` subst2
      f (prefix ++ [(q, xs')]) (bvs `IntSet.union` xs') subst1 subst2' prefix1 prefix2'

-- XXX
prenexOr :: (Int, Prefix, Matrix) -> (Int, Prefix, Matrix) -> (Int, Prefix, Matrix)
prenexOr (nv1, prefix1, matrix1) (nv2, prefix2, matrix2) =
  evalState (f [] IntSet.empty IntMap.empty IntMap.empty prefix1 prefix2) (nv1 `max` nv2)
  where
    f :: Prefix -> VarSet
      -> VarMap Tseitin.Formula -> VarMap Tseitin.Formula
      -> Prefix -> Prefix
      -> State Int (Int, Prefix, Matrix)
    f prefix _bvs subst1 subst2 [] [] = do
      nv <- get
      return (nv, prefix, Tseitin.simplify (substVarMap matrix1 subst1 .||. substVarMap matrix2 subst2))
    f prefix bvs subst1 subst2 ((E,xs1) : prefix1') ((E,xs2) : prefix2') = do
      let xs = IntSet.union xs1 xs2
          ys = IntSet.intersection bvs xs
      nv <- get
      put (nv + IntSet.size ys)
      let s  = IntMap.fromList $ zip (IntSet.toList ys) [(nv+1) ..]
          xs' = (xs `IntSet.difference` bvs) `IntSet.union` IntSet.fromList (IntMap.elems s)
          subst1' = fmap litToMatrix (IntMap.filterWithKey (\x _ -> x `IntSet.member` xs1) s) `IntMap.union` subst1
          subst2' = fmap litToMatrix (IntMap.filterWithKey (\x _ -> x `IntSet.member` xs2) s) `IntMap.union` subst2
      f (prefix ++ [(A, xs')]) (bvs `IntSet.union` xs') subst1' subst2' prefix1' prefix2'
    f prefix bvs subst1 subst2 ((q,xs) : prefix1') prefix2 | q==A || not (prefixStartWithA prefix2)= do
      let ys = IntSet.intersection bvs xs
      nv <- get
      put (nv + IntSet.size ys)
      let s  = IntMap.fromList $ zip (IntSet.toList ys) [(nv+1) ..]
          xs' = (xs `IntSet.difference` bvs) `IntSet.union` IntSet.fromList (IntMap.elems s)
          subst1' = fmap litToMatrix s `IntMap.union` subst1
      f (prefix ++ [(q, xs')]) (bvs `IntSet.union` xs') subst1' subst2 prefix1' prefix2
    f prefix bvs subst1 subst2 prefix1 ((q,xs) : prefix2')  = do
      let ys = IntSet.intersection bvs xs
      nv <- get
      put (nv + IntSet.size ys)
      let s  = IntMap.fromList $ zip (IntSet.toList ys) [(nv+1) ..]
          xs' = (xs `IntSet.difference` bvs) `IntSet.union` IntSet.fromList (IntMap.elems s)
          subst2' = fmap litToMatrix s `IntMap.union` subst2
      f (prefix ++ [(q, xs')]) (bvs `IntSet.union` xs') subst1 subst2' prefix1 prefix2'

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

solve :: Int -> Prefix -> Matrix -> IO (Bool, Maybe LitSet)
solve = solveCEGARIncremental

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

-- | Naive Algorithm for a Winning Move
solveNaive :: Int -> Prefix -> Matrix -> IO (Bool, Maybe LitSet)
solveNaive nv prefix matrix =
  case prefix' of
    [] -> if Tseitin.fold undefined matrix
          then return (True, Just IntSet.empty)
          else return (False, Nothing)
    (E,_) : _ -> do
      m <- f prefix' matrix
      return (isJust m, m)
    (A,_) : _ -> do
      m <- f prefix' matrix
      return (isNothing m, m)
  where
    prefix' = normalizePrefix prefix

    {- Naive Algorithm for a Winning Move
    Function Solve (QX. Φ)
    begin
      if Φ has no quant then
        return (Q = ∃) ? SAT(φ) : SAT(¬φ)
      Λ ← {true, false}^X  // consider all assignments
      while true do
        if Λ = ∅ then      // all assignments used up
          return NULL
        τ ← pick(Λ)        // pick a candidate solution
        μ ← Solve(Φ[τ])    // find a countermove
        if μ = NULL then   // winning move
          return τ
        Λ ← Λ \ {τ}        // remove bad candidate
      end
    end
    -}
    f :: Prefix -> Matrix -> IO (Maybe LitSet)
    f [] _matrix = error "should not happen"
    f [(q,xs)] matrix = do
      solver <- SAT.newSolver
      SAT.newVars_ solver nv
      enc <- Tseitin.newEncoder solver
      case q of
        E -> Tseitin.addFormula enc matrix
        A -> Tseitin.addFormula enc (notB matrix)
      ret <- SAT.solve solver
      if ret then do
        m <- SAT.getModel solver
        return $ Just $ IntSet.fromList [if SAT.evalLit m x then x else -x | x <- IntSet.toList xs]
      else
        return Nothing
    f ((_q,xs) : prefix') matrix = do
      ret <- runExceptT $ do
        let moves :: [LitSet]
            moves = map IntSet.fromList $ sequence [[x, -x] | x <- IntSet.toList xs]
        forM_ moves $ \tau -> do
          ret <- lift $ f prefix' (reduct matrix tau)
          case ret of
            Nothing  -> throwE tau
            Just _nu -> return ()
      case ret of
        Left tau -> return (Just tau)
        Right () -> return Nothing

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

-- | Abstraction-Based Algorithm for a Winning Move
solveCEGAR :: Int -> Prefix -> Matrix -> IO (Bool, Maybe LitSet)
solveCEGAR nv prefix matrix =
  case prefix' of
    [] -> if Tseitin.fold undefined matrix
          then return (True, Just IntSet.empty)
          else return (False, Nothing)
    (E,_) : _ -> do
      m <- f nv prefix' matrix
      return (isJust m, m)
    (A,_) : _ -> do
      m <- f nv prefix' matrix
      return (isNothing m, m)
  where
    prefix' = normalizePrefix prefix

    {-
    Function Solve (QX. Φ)
    begin
      if Φ has no quant then
        return (Q = ∃) ? SAT(φ) : SAT(¬φ)
      ω ← ∅
      while true do
        α ← (Q = ∃) ? ∧_{μ∈ω} Φ[μ] : ∨_{μ∈ω} Φ[μ] // abstraction
        τ' ← Solve(Prenex(QX.α)) // find a candidate
        if τ' = NULL then return NULL // no winning move
        τ ← {l | l ∈ τ′ ∧ var(l) ∈ X} // filter a move for X
        μ ← Solve(Φ[τ])
        if μ = NULL then return τ
        ω ← ω∪{μ}
      end
    end
    -}
    f :: Int -> Prefix -> Matrix -> IO (Maybe LitSet)
    f _nv [] _matrix = error "should not happen"
    f nv [(q,xs)] matrix = do
      solver <- SAT.newSolver
      SAT.newVars_ solver nv
      enc <- Tseitin.newEncoder solver
      case q of
        E -> Tseitin.addFormula enc matrix
        A -> Tseitin.addFormula enc (notB matrix)
      ret <- SAT.solve solver
      if ret then do
        m <- SAT.getModel solver
        return $ Just $ IntSet.fromList [if SAT.evalLit m x then x else -x | x <- IntSet.toList xs]
      else
        return Nothing
    f nv ((q,xs) : prefix'@((_q2,_) : prefix'')) matrix = do
      let loop counterMoves = do
            let ys = [(nv, prefix'', reduct matrix nu) | nu <- counterMoves]
                (nv2, prefix2, matrix2) =
                  if q==E
                  then foldl' prenexAnd (nv,[],true) ys
                  else foldl' prenexOr (nv,[],false) ys
            ret <- f nv2 (normalizePrefix ((q,xs) : prefix2)) matrix2
            case ret of
              Nothing -> return Nothing
              Just tau' -> do
                let tau = IntSet.filter (\l -> abs l `IntSet.member` xs) tau'
                ret2 <- f nv prefix' (reduct matrix tau)
                case ret2 of
                  Nothing -> return (Just tau)
                  Just nu -> loop (nu : counterMoves)
      loop []

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

-- | Abstraction-Based Algorithm for a Winning Move
solveCEGARIncremental :: Int -> Prefix -> Matrix -> IO (Bool, Maybe LitSet)
solveCEGARIncremental nv prefix matrix =
  case prefix' of
    [] -> if Tseitin.fold undefined matrix
          then return (True, Just IntSet.empty)
          else return (False, Nothing)
    (E,_) : _ -> do
      m <- f nv IntSet.empty prefix' matrix
      return (isJust m, m)
    (A,_) : _ -> do
      m <- f nv IntSet.empty prefix' matrix
      return (isNothing m, m)
  where
    prefix' = normalizePrefix prefix

    {-
    Function Solve (QX. Φ)
    begin
      if Φ has no quant then
        return (Q = ∃) ? SAT(φ) : SAT(¬φ)
      ω ← ∅
      while true do
        α ← (Q = ∃) ? ∧_{μ∈ω} Φ[μ] : ∨_{μ∈ω} Φ[μ] // abstraction
        τ' ← Solve(Prenex(QX.α)) // find a candidate
        if τ' = NULL then return NULL // no winning move
        τ ← {l | l ∈ τ′ ∧ var(l) ∈ X} // filter a move for X
        μ ← Solve(Φ[τ])
        if μ = NULL then return τ
        ω ← ω∪{μ}
      end
    end
    -}
    f :: Int -> LitSet -> Prefix -> Matrix -> IO (Maybe LitSet)
    f nv _assumptions prefix matrix = do
      solver <- SAT.newSolver
      SAT.newVars_ solver nv
      enc <- Tseitin.newEncoder solver
      _xs <-
        case last prefix of
          (E, xs) -> do
            Tseitin.addFormula enc matrix
            return xs
          (A, xs) -> do
            Tseitin.addFormula enc (notB matrix)
            return xs
      let g :: Int -> LitSet -> Prefix -> Matrix -> IO (Maybe LitSet)
          g _nv _assumptions [] _matrix = error "should not happen"
          g _nv assumptions [(_q,xs)] _matrix = do
            ret <- SAT.solveWith solver (IntSet.toList assumptions)
            if ret then do
              m <- SAT.getModel solver
              return $ Just $ IntSet.fromList [if SAT.evalLit m x then x else -x | x <- IntSet.toList xs]
            else
              return Nothing
          g nv assumptions ((q,xs) : prefix'@((_q2,_) : prefix'')) matrix = do
            let loop counterMoves = do
                  let ys = [(nv, prefix'', reduct matrix nu) | nu <- counterMoves]
                      (nv2, prefix2, matrix2) =
                        if q==E
                        then foldl' prenexAnd (nv,[],true) ys
                        else foldl' prenexOr (nv,[],false) ys
                  ret <- f nv2 assumptions (normalizePrefix ((q,xs) : prefix2)) matrix2
                  case ret of
                    Nothing -> return Nothing
                    Just tau' -> do
                      let tau = IntSet.filter (\l -> abs l `IntSet.member` xs) tau'
                      ret2 <- g nv (assumptions `IntSet.union` tau) prefix' (reduct matrix tau)
                      case ret2 of
                        Nothing -> return (Just tau)
                        Just nu -> loop (nu : counterMoves)
            loop []
      g nv IntSet.empty prefix matrix

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

data CNFOrDNF
  = CNF [LitSet]
  | DNF [LitSet]
  deriving (Show)

negateCNFOrDNF :: CNFOrDNF -> CNFOrDNF
negateCNFOrDNF (CNF xss) = DNF (map (IntSet.map negate) xss)
negateCNFOrDNF (DNF xss) = CNF (map (IntSet.map negate) xss)

toCNF :: Int -> CNFOrDNF -> CNF.CNF
toCNF nv (CNF clauses) = CNF.CNF nv (length clauses) (map (SAT.packClause . IntSet.toList) clauses)
toCNF nv (DNF [])    = CNF.CNF nv 1 [SAT.packClause []]
toCNF nv (DNF cubes) = CNF.CNF (nv + length cubes) (length cs) (map SAT.packClause cs)
  where
    zs = zip [nv+1..] cubes
    cs = map fst zs : [[-sel, lit] | (sel, cube) <- zs, lit <- IntSet.toList cube]

solveQE :: Int -> Prefix -> Matrix -> IO (Bool, Maybe LitSet)
solveQE nv prefix matrix = do
  store <- newCNFStore
  SAT.newVars_ store nv
  encoder <- Tseitin.newEncoder store
  Tseitin.addFormula encoder matrix
  cnf <- getCNFFormula store
  let prefix' =
        if CNF.cnfNumVars cnf > nv then
          prefix ++ [(E, IntSet.fromList [nv+1 .. CNF.cnfNumVars cnf])]
        else
          prefix
  (b, m) <- solveQE_CNF (CNF.cnfNumVars cnf) prefix' (map SAT.unpackClause (CNF.cnfClauses cnf))
  return (b, fmap (IntSet.filter (\lit -> abs lit <= nv)) m)

solveQE_CNF :: Int -> Prefix -> [SAT.Clause] -> IO (Bool, Maybe LitSet)
solveQE_CNF nv prefix matrix = g (normalizePrefix prefix) matrix
  where
    g :: Prefix -> [SAT.Clause] -> IO (Bool, Maybe LitSet)
    g ((E,xs) : prefix') matrix = do
      cnf <- liftM (toCNF nv) $ f prefix' matrix
      solver <- SAT.newSolver
      SAT.newVars_ solver (CNF.cnfNumVars cnf)
      forM_ (CNF.cnfClauses cnf) $ \clause -> do
        SAT.addClause solver (SAT.unpackClause clause)
      ret <- SAT.solve solver
      if ret then do
        m <- SAT.getModel solver
        return (True, Just $ IntSet.fromList [if SAT.evalLit m x then x else -x | x <- IntSet.toList xs])
      else do
        return (False, Nothing)
    g ((A,xs) : prefix') matrix = do
      cnf <- liftM (toCNF nv . negateCNFOrDNF) $ f prefix' matrix
      solver <- SAT.newSolver
      SAT.newVars_ solver (CNF.cnfNumVars cnf)
      forM_ (CNF.cnfClauses cnf) $ \clause -> do
        SAT.addClause solver (SAT.unpackClause clause)
      ret <- SAT.solve solver
      if ret then do
        m <- SAT.getModel solver
        return (False, Just $ IntSet.fromList [if SAT.evalLit m x then x else -x | x <- IntSet.toList xs])
      else do
        return (True, Nothing)
    g prefix matrix = do
      ret <- f prefix matrix
      case ret of
        CNF xs -> return (not (any IntSet.null xs), Nothing)
        DNF xs -> return (any IntSet.null xs, Nothing)

    f :: Prefix -> [SAT.Clause] -> IO CNFOrDNF
    f [] matrix = return $ CNF [IntSet.fromList clause | clause <- matrix]
    f ((E,xs) : prefix') matrix = do
      cnf <- liftM (toCNF nv) $ f prefix' matrix
      dnf <- QE.shortestImplicantsE (xs `IntSet.union` IntSet.fromList [nv+1 .. CNF.cnfNumVars cnf]) cnf
      return $ DNF dnf
    f ((A,xs) : prefix') matrix = do
      cnf <- liftM (toCNF nv . negateCNFOrDNF) $ f prefix' matrix
      dnf <- QE.shortestImplicantsE (xs `IntSet.union` IntSet.fromList [nv+1 .. CNF.cnfNumVars cnf]) cnf
      return $ negateCNFOrDNF $ DNF dnf

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

-- ∀y ∃x. x ∧ (y ∨ ¬x)
_test :: IO (Bool, Maybe LitSet)
_test = solveNaive 2 [(A, IntSet.singleton 2), (E, IntSet.singleton 1)] (x .&&. (y .||. notB x))
  where
    x  = litToMatrix 1
    y  = litToMatrix 2

_test' :: IO (Bool, Maybe LitSet)
_test' = solveCEGAR 2 [(A, IntSet.singleton 2), (E, IntSet.singleton 1)] (x .&&. (y .||. notB x))
  where
    x  = litToMatrix 1
    y  = litToMatrix 2

_test1 :: (Int, Prefix, Matrix)
_test1 = prenexAnd (1, [(A, IntSet.singleton 1)], litToMatrix 1) (1, [(A, IntSet.singleton 1)], notB (litToMatrix 1))

_test2 :: (Int, Prefix, Matrix)
_test2 = prenexOr (1, [(A, IntSet.singleton 1)], litToMatrix 1) (1, [(A, IntSet.singleton 1)], litToMatrix 1)

1	{-# OPTIONS_GHC -Wall #-}
2	{-# OPTIONS_HADDOCK show-extensions #-}
3	{-# LANGUAGE BangPatterns #-}
4	-----------------------------------------------------------------------------
5	-- \|
6	-- Module : ToySolver.QBF
7	-- Copyright : (c) Masahiro Sakai 2016
8	-- License : BSD-style
9	--
10	-- Maintainer : masahiro.sakai@gmail.com
11	-- Stability : provisional
12	-- Portability : non-portable
13	--
14	-- Reference:
15	--
16	-- * Mikoláš Janota, William Klieber, Joao Marques-Silva, Edmund Clarke.
17	-- Solving QBF with Counterexample Guided Refinement.
18	-- In Theory and Applications of Satisfiability Testing (SAT 2012), pp. 114-128.
19	-- <https://doi.org/10.1007/978-3-642-31612-8_10>
20	-- <https://www.cs.cmu.edu/~wklieber/papers/qbf-cegar-sat-2012.pdf>
21	--
22	-----------------------------------------------------------------------------
23	module ToySolver.QBF
24	( Quantifier (..)
25	, Prefix
26	, normalizePrefix
27	, quantifyFreeVariables
28	, Matrix
29	, litToMatrix
30	, solve
31	, solveNaive
32	, solveCEGAR
33	, solveCEGARIncremental
34	, solveQE
35	, solveQE_CNF
36	) where
37
38	import Control.Monad
39	import Control.Monad.State.Strict
40	import Control.Monad.Trans.Except
41	import qualified Data.IntMap as IntMap
42	import qualified Data.IntSet as IntSet
43	import Data.Function (on)
44	import Data.List (foldl')
45	import qualified Data.List.NonEmpty as NonEmpty
46	import Data.Maybe
47
48	import ToySolver.Data.Boolean
49	import ToySolver.FileFormat.CNF (Quantifier (..))
50	import qualified ToySolver.FileFormat.CNF as CNF
51	import qualified ToySolver.SAT as SAT
52	import ToySolver.SAT.Types (LitSet, VarSet, VarMap)
53	import qualified ToySolver.SAT.Encoder.Tseitin as Tseitin
54	import ToySolver.SAT.Store.CNF
55
56	import qualified ToySolver.SAT.ExistentialQuantification as QE
57
58	-- ----------------------------------------------------------------------------
59
60	type Prefix = [(Quantifier, VarSet)]
61
62	normalizePrefix :: Prefix -> Prefix
63	normalizePrefix = groupQuantifiers . removeEmptyQuantifiers	1✔
64
65	removeEmptyQuantifiers :: Prefix -> Prefix
66	removeEmptyQuantifiers = filter (\(_,xs) -> not (IntSet.null xs))	1✔
67
68	groupQuantifiers :: Prefix -> Prefix
69	groupQuantifiers = map f . NonEmpty.groupBy ((==) `on` fst)	1✔
70	where
71	f qs = (fst (NonEmpty.head qs), IntSet.unions [xs \| (_,xs) <- NonEmpty.toList qs])	1✔
72
73	quantifyFreeVariables :: Int -> Prefix -> Prefix
74	quantifyFreeVariables nv prefix	×
75	\| IntSet.null rest = prefix	×
76	\| otherwise = (E, rest) : prefix	×
77	where
78	rest = IntSet.fromList [1..nv] `IntSet.difference` IntSet.unions [vs \| (_q, vs) <- prefix]	×
79
80	prefixStartWithA :: Prefix -> Bool
81	prefixStartWithA ((A,_) : _) = True	×
82	prefixStartWithA _ = False	×
83
84	prefixStartWithE :: Prefix -> Bool
85	prefixStartWithE ((E,_) : _) = True	×
86	prefixStartWithE _ = False	×
87
88	-- ----------------------------------------------------------------------------
89
90	type Matrix = Tseitin.Formula
91
92	litToMatrix :: SAT.Lit -> Matrix
93	litToMatrix = Tseitin.Atom	1✔
94
95	reduct :: Matrix -> LitSet -> Matrix
96	reduct m ls = Tseitin.simplify $ Tseitin.fold s m	1✔
97	where
98	s l	1✔
99	\| l `IntSet.member` ls = true	1✔
100	\| (-l) `IntSet.member` ls = false	1✔
101	\| otherwise = litToMatrix l	×
102
103	substVarMap :: Matrix -> VarMap Matrix -> Matrix
104	substVarMap m s = Tseitin.simplify $ Tseitin.fold f m	1✔
105	where
106	f l = do	1✔
107	let v = abs l	1✔
108	(if l > 0 then id else notB) $ IntMap.findWithDefault (litToMatrix v) v s	×
109
110	-- XXX
111	prenexAnd :: (Int, Prefix, Matrix) -> (Int, Prefix, Matrix) -> (Int, Prefix, Matrix)
112	prenexAnd (nv1, prefix1, matrix1) (nv2, prefix2, matrix2) =	1✔
113	evalState (f [] IntSet.empty IntMap.empty IntMap.empty prefix1 prefix2) (nv1 `max` nv2)	1✔
114	where
115	f :: Prefix -> VarSet
116	-> VarMap Tseitin.Formula -> VarMap Tseitin.Formula
117	-> Prefix -> Prefix
118	-> State Int (Int, Prefix, Matrix)
119	f prefix _bvs subst1 subst2 [] [] = do	1✔
120	nv <- get	1✔
121	return (nv, prefix, Tseitin.simplify (substVarMap matrix1 subst1 .&&. substVarMap matrix2 subst2))	1✔
122	f prefix bvs subst1 subst2 ((A,xs1) : prefix1') ((A,xs2) : prefix2') = do	×
123	let xs = IntSet.union xs1 xs2	×
124	ys = IntSet.intersection bvs xs	×
125	nv <- get	×
126	put (nv + IntSet.size ys)	×
127	let s = IntMap.fromList $ zip (IntSet.toList ys) [(nv+1) ..]	×
128	xs' = (xs `IntSet.difference` bvs) `IntSet.union` IntSet.fromList (IntMap.elems s)	×
129	subst1' = fmap litToMatrix (IntMap.filterWithKey (\x _ -> x `IntSet.member` xs1) s) `IntMap.union` subst1	×
130	subst2' = fmap litToMatrix (IntMap.filterWithKey (\x _ -> x `IntSet.member` xs2) s) `IntMap.union` subst2	×
131	f (prefix ++ [(A, xs')]) (bvs `IntSet.union` xs') subst1' subst2' prefix1' prefix2'	×
132	f prefix bvs subst1 subst2 ((q,xs) : prefix1') prefix2 \| q==E \|\| not (prefixStartWithE prefix2) = do	×
133	let ys = IntSet.intersection bvs xs	×
134	nv <- get	×
135	put (nv + IntSet.size ys)	×
136	let s = IntMap.fromList $ zip (IntSet.toList ys) [(nv+1) ..]	×
137	xs' = (xs `IntSet.difference` bvs) `IntSet.union` IntSet.fromList (IntMap.elems s)	×
138	subst1' = fmap litToMatrix s `IntMap.union` subst1	×
139	f (prefix ++ [(q, xs')]) (bvs `IntSet.union` xs') subst1' subst2 prefix1' prefix2	×
140	f prefix bvs subst1 subst2 prefix1 ((q,xs) : prefix2') = do	1✔
141	let ys = IntSet.intersection bvs xs	×
142	nv <- get	1✔
143	put (nv + IntSet.size ys)	1✔
144	let s = IntMap.fromList $ zip (IntSet.toList ys) [(nv+1) ..]	×
145	xs' = (xs `IntSet.difference` bvs) `IntSet.union` IntSet.fromList (IntMap.elems s)	1✔
146	subst2' = fmap litToMatrix s `IntMap.union` subst2	×
147	f (prefix ++ [(q, xs')]) (bvs `IntSet.union` xs') subst1 subst2' prefix1 prefix2'	×
148
149	-- XXX
150	prenexOr :: (Int, Prefix, Matrix) -> (Int, Prefix, Matrix) -> (Int, Prefix, Matrix)
151	prenexOr (nv1, prefix1, matrix1) (nv2, prefix2, matrix2) =	1✔
152	evalState (f [] IntSet.empty IntMap.empty IntMap.empty prefix1 prefix2) (nv1 `max` nv2)	1✔
153	where
154	f :: Prefix -> VarSet
155	-> VarMap Tseitin.Formula -> VarMap Tseitin.Formula
156	-> Prefix -> Prefix
157	-> State Int (Int, Prefix, Matrix)
158	f prefix _bvs subst1 subst2 [] [] = do	1✔
159	nv <- get	1✔
160	return (nv, prefix, Tseitin.simplify (substVarMap matrix1 subst1 .\|\|. substVarMap matrix2 subst2))	1✔
161	f prefix bvs subst1 subst2 ((E,xs1) : prefix1') ((E,xs2) : prefix2') = do	×
162	let xs = IntSet.union xs1 xs2	×
163	ys = IntSet.intersection bvs xs	×
164	nv <- get	×
165	put (nv + IntSet.size ys)	×
166	let s = IntMap.fromList $ zip (IntSet.toList ys) [(nv+1) ..]	×
167	xs' = (xs `IntSet.difference` bvs) `IntSet.union` IntSet.fromList (IntMap.elems s)	×
168	subst1' = fmap litToMatrix (IntMap.filterWithKey (\x _ -> x `IntSet.member` xs1) s) `IntMap.union` subst1	×
169	subst2' = fmap litToMatrix (IntMap.filterWithKey (\x _ -> x `IntSet.member` xs2) s) `IntMap.union` subst2	×
170	f (prefix ++ [(A, xs')]) (bvs `IntSet.union` xs') subst1' subst2' prefix1' prefix2'	×
171	f prefix bvs subst1 subst2 ((q,xs) : prefix1') prefix2 \| q==A \|\| not (prefixStartWithA prefix2)= do	×
172	let ys = IntSet.intersection bvs xs	×
173	nv <- get	1✔
174	put (nv + IntSet.size ys)	1✔
175	let s = IntMap.fromList $ zip (IntSet.toList ys) [(nv+1) ..]	×
176	xs' = (xs `IntSet.difference` bvs) `IntSet.union` IntSet.fromList (IntMap.elems s)	1✔
177	subst1' = fmap litToMatrix s `IntMap.union` subst1	×
178	f (prefix ++ [(q, xs')]) (bvs `IntSet.union` xs') subst1' subst2 prefix1' prefix2	1✔
179	f prefix bvs subst1 subst2 prefix1 ((q,xs) : prefix2') = do	1✔
180	let ys = IntSet.intersection bvs xs	1✔
181	nv <- get	1✔
182	put (nv + IntSet.size ys)	1✔
183	let s = IntMap.fromList $ zip (IntSet.toList ys) [(nv+1) ..]	1✔
184	xs' = (xs `IntSet.difference` bvs) `IntSet.union` IntSet.fromList (IntMap.elems s)	1✔
185	subst2' = fmap litToMatrix s `IntMap.union` subst2	×
186	f (prefix ++ [(q, xs')]) (bvs `IntSet.union` xs') subst1 subst2' prefix1 prefix2'	×
187
188	-- ----------------------------------------------------------------------------
189
190	solve :: Int -> Prefix -> Matrix -> IO (Bool, Maybe LitSet)
191	solve = solveCEGARIncremental	×
192
193	-- ----------------------------------------------------------------------------
194
195	-- \| Naive Algorithm for a Winning Move
196	solveNaive :: Int -> Prefix -> Matrix -> IO (Bool, Maybe LitSet)
197	solveNaive nv prefix matrix =	×
198	case prefix' of	×
199	[] -> if Tseitin.fold undefined matrix	×
200	then return (True, Just IntSet.empty)	×
201	else return (False, Nothing)	×
202	(E,_) : _ -> do	×
203	m <- f prefix' matrix	×
204	return (isJust m, m)	×
205	(A,_) : _ -> do	×
206	m <- f prefix' matrix	×
207	return (isNothing m, m)	×
208	where
209	prefix' = normalizePrefix prefix	×
210
211	{- Naive Algorithm for a Winning Move
212	Function Solve (QX. Φ)
213	begin
214	if Φ has no quant then
215	return (Q = ∃) ? SAT(φ) : SAT(¬φ)
216	Λ ← {true, false}^X // consider all assignments
217	while true do
218	if Λ = ∅ then // all assignments used up
219	return NULL
220	τ ← pick(Λ) // pick a candidate solution
221	μ ← Solve(Φ[τ]) // find a countermove
222	if μ = NULL then // winning move
223	return τ
224	Λ ← Λ \ {τ} // remove bad candidate
225	end
226	end
227	-}
228	f :: Prefix -> Matrix -> IO (Maybe LitSet)
229	f [] _matrix = error "should not happen"	×
230	f [(q,xs)] matrix = do	×
231	solver <- SAT.newSolver	×
232	SAT.newVars_ solver nv	×
233	enc <- Tseitin.newEncoder solver	×
234	case q of	×
235	E -> Tseitin.addFormula enc matrix	×
236	A -> Tseitin.addFormula enc (notB matrix)	×
237	ret <- SAT.solve solver	×
238	if ret then do	×
239	m <- SAT.getModel solver	×
240	return $ Just $ IntSet.fromList [if SAT.evalLit m x then x else -x \| x <- IntSet.toList xs]	×
241	else
242	return Nothing	×
243	f ((_q,xs) : prefix') matrix = do	×
244	ret <- runExceptT $ do	×
245	let moves :: [LitSet]
246	moves = map IntSet.fromList $ sequence [[x, -x] \| x <- IntSet.toList xs]	×
247	forM_ moves $ \tau -> do	×
248	ret <- lift $ f prefix' (reduct matrix tau)	×
249	case ret of	×
250	Nothing -> throwE tau	×
251	Just _nu -> return ()	×
252	case ret of	×
253	Left tau -> return (Just tau)	×
254	Right () -> return Nothing	×
255
256	-- ----------------------------------------------------------------------------
257
258	-- \| Abstraction-Based Algorithm for a Winning Move
259	solveCEGAR :: Int -> Prefix -> Matrix -> IO (Bool, Maybe LitSet)
260	solveCEGAR nv prefix matrix =	1✔
261	case prefix' of	1✔
262	[] -> if Tseitin.fold undefined matrix	×
263	then return (True, Just IntSet.empty)	×
264	else return (False, Nothing)	1✔
265	(E,_) : _ -> do	1✔
266	m <- f nv prefix' matrix	1✔
267	return (isJust m, m)	1✔
268	(A,_) : _ -> do	1✔
269	m <- f nv prefix' matrix	1✔
270	return (isNothing m, m)	1✔
271	where
272	prefix' = normalizePrefix prefix	1✔
273
274	{-
275	Function Solve (QX. Φ)
276	begin
277	if Φ has no quant then
278	return (Q = ∃) ? SAT(φ) : SAT(¬φ)
279	ω ← ∅
280	while true do
281	α ← (Q = ∃) ? ∧_{μ∈ω} Φ[μ] : ∨_{μ∈ω} Φ[μ] // abstraction
282	τ' ← Solve(Prenex(QX.α)) // find a candidate
283	if τ' = NULL then return NULL // no winning move
284	τ ← {l \| l ∈ τ′ ∧ var(l) ∈ X} // filter a move for X
285	μ ← Solve(Φ[τ])
286	if μ = NULL then return τ
287	ω ← ω∪{μ}
288	end
289	end
290	-}
291	f :: Int -> Prefix -> Matrix -> IO (Maybe LitSet)
292	f _nv [] _matrix = error "should not happen"	×
293	f nv [(q,xs)] matrix = do	1✔
294	solver <- SAT.newSolver	1✔
295	SAT.newVars_ solver nv	1✔
296	enc <- Tseitin.newEncoder solver	1✔
297	case q of	1✔
298	E -> Tseitin.addFormula enc matrix	1✔
299	A -> Tseitin.addFormula enc (notB matrix)	1✔
300	ret <- SAT.solve solver	1✔
301	if ret then do	1✔
302	m <- SAT.getModel solver	1✔
303	return $ Just $ IntSet.fromList [if SAT.evalLit m x then x else -x \| x <- IntSet.toList xs]	1✔
304	else
305	return Nothing	1✔
306	f nv ((q,xs) : prefix'@((_q2,_) : prefix'')) matrix = do	1✔
307	let loop counterMoves = do	1✔
308	let ys = [(nv, prefix'', reduct matrix nu) \| nu <- counterMoves]	1✔
309	(nv2, prefix2, matrix2) =
310	if q==E	1✔
311	then foldl' prenexAnd (nv,[],true) ys	1✔
312	else foldl' prenexOr (nv,[],false) ys	1✔
313	ret <- f nv2 (normalizePrefix ((q,xs) : prefix2)) matrix2	1✔
314	case ret of	1✔
315	Nothing -> return Nothing	1✔
316	Just tau' -> do	1✔
317	let tau = IntSet.filter (\l -> abs l `IntSet.member` xs) tau'	1✔
318	ret2 <- f nv prefix' (reduct matrix tau)	1✔
319	case ret2 of	1✔
320	Nothing -> return (Just tau)	1✔
321	Just nu -> loop (nu : counterMoves)	1✔
322	loop []	1✔
323
324	-- ----------------------------------------------------------------------------
325
326	-- \| Abstraction-Based Algorithm for a Winning Move
327	solveCEGARIncremental :: Int -> Prefix -> Matrix -> IO (Bool, Maybe LitSet)
328	solveCEGARIncremental nv prefix matrix =	1✔
329	case prefix' of	1✔
330	[] -> if Tseitin.fold undefined matrix	×
331	then return (True, Just IntSet.empty)	×
332	else return (False, Nothing)	1✔
333	(E,_) : _ -> do	1✔
334	m <- f nv IntSet.empty prefix' matrix	×
335	return (isJust m, m)	1✔
336	(A,_) : _ -> do	1✔
337	m <- f nv IntSet.empty prefix' matrix	×
338	return (isNothing m, m)	1✔
339	where
340	prefix' = normalizePrefix prefix	1✔
341
342	{-
343	Function Solve (QX. Φ)
344	begin
345	if Φ has no quant then
346	return (Q = ∃) ? SAT(φ) : SAT(¬φ)
347	ω ← ∅
348	while true do
349	α ← (Q = ∃) ? ∧_{μ∈ω} Φ[μ] : ∨_{μ∈ω} Φ[μ] // abstraction
350	τ' ← Solve(Prenex(QX.α)) // find a candidate
351	if τ' = NULL then return NULL // no winning move
352	τ ← {l \| l ∈ τ′ ∧ var(l) ∈ X} // filter a move for X
353	μ ← Solve(Φ[τ])
354	if μ = NULL then return τ
355	ω ← ω∪{μ}
356	end
357	end
358	-}
359	f :: Int -> LitSet -> Prefix -> Matrix -> IO (Maybe LitSet)
360	f nv _assumptions prefix matrix = do	1✔
361	solver <- SAT.newSolver	1✔
362	SAT.newVars_ solver nv	1✔
363	enc <- Tseitin.newEncoder solver	1✔
364	_xs <-
365	case last prefix of	1✔
366	(E, xs) -> do	1✔
367	Tseitin.addFormula enc matrix	1✔
368	return xs	×
369	(A, xs) -> do	1✔
370	Tseitin.addFormula enc (notB matrix)	1✔
371	return xs	×
372	let g :: Int -> LitSet -> Prefix -> Matrix -> IO (Maybe LitSet)
373	g _nv _assumptions [] _matrix = error "should not happen"	×
374	g _nv assumptions [(_q,xs)] _matrix = do	1✔
375	ret <- SAT.solveWith solver (IntSet.toList assumptions)	1✔
376	if ret then do	1✔
377	m <- SAT.getModel solver	1✔
378	return $ Just $ IntSet.fromList [if SAT.evalLit m x then x else -x \| x <- IntSet.toList xs]	1✔
379	else
380	return Nothing	1✔
381	g nv assumptions ((q,xs) : prefix'@((_q2,_) : prefix'')) matrix = do	1✔
382	let loop counterMoves = do	1✔
383	let ys = [(nv, prefix'', reduct matrix nu) \| nu <- counterMoves]	1✔
384	(nv2, prefix2, matrix2) =
385	if q==E	1✔
386	then foldl' prenexAnd (nv,[],true) ys	1✔
387	else foldl' prenexOr (nv,[],false) ys	1✔
388	ret <- f nv2 assumptions (normalizePrefix ((q,xs) : prefix2)) matrix2	×
389	case ret of	1✔
390	Nothing -> return Nothing	1✔
391	Just tau' -> do	1✔
392	let tau = IntSet.filter (\l -> abs l `IntSet.member` xs) tau'	1✔
393	ret2 <- g nv (assumptions `IntSet.union` tau) prefix' (reduct matrix tau)	1✔
394	case ret2 of	1✔
395	Nothing -> return (Just tau)	1✔
396	Just nu -> loop (nu : counterMoves)	1✔
397	loop []	1✔
398	g nv IntSet.empty prefix matrix	1✔
399
400	-- ----------------------------------------------------------------------------
401
402	data CNFOrDNF
403	= CNF [LitSet]
404	\| DNF [LitSet]
405	deriving (Show)	×
406
407	negateCNFOrDNF :: CNFOrDNF -> CNFOrDNF
408	negateCNFOrDNF (CNF xss) = DNF (map (IntSet.map negate) xss)	1✔
409	negateCNFOrDNF (DNF xss) = CNF (map (IntSet.map negate) xss)	1✔
410
411	toCNF :: Int -> CNFOrDNF -> CNF.CNF
412	toCNF nv (CNF clauses) = CNF.CNF nv (length clauses) (map (SAT.packClause . IntSet.toList) clauses)	1✔
413	toCNF nv (DNF []) = CNF.CNF nv 1 [SAT.packClause []]	1✔
414	toCNF nv (DNF cubes) = CNF.CNF (nv + length cubes) (length cs) (map SAT.packClause cs)	1✔
415	where
416	zs = zip [nv+1..] cubes	1✔
417	cs = map fst zs : [[-sel, lit] \| (sel, cube) <- zs, lit <- IntSet.toList cube]	1✔
418
419	solveQE :: Int -> Prefix -> Matrix -> IO (Bool, Maybe LitSet)
420	solveQE nv prefix matrix = do	1✔
421	store <- newCNFStore	1✔
422	SAT.newVars_ store nv	1✔
423	encoder <- Tseitin.newEncoder store	1✔
424	Tseitin.addFormula encoder matrix	1✔
425	cnf <- getCNFFormula store	1✔
426	let prefix' =	1✔
427	if CNF.cnfNumVars cnf > nv then	×
428	prefix ++ [(E, IntSet.fromList [nv+1 .. CNF.cnfNumVars cnf])]	×
429	else
430	prefix	1✔
431	(b, m) <- solveQE_CNF (CNF.cnfNumVars cnf) prefix' (map SAT.unpackClause (CNF.cnfClauses cnf))	1✔
432	return (b, fmap (IntSet.filter (\lit -> abs lit <= nv)) m)	1✔
433
434	solveQE_CNF :: Int -> Prefix -> [SAT.Clause] -> IO (Bool, Maybe LitSet)
435	solveQE_CNF nv prefix matrix = g (normalizePrefix prefix) matrix	1✔
436	where
437	g :: Prefix -> [SAT.Clause] -> IO (Bool, Maybe LitSet)
438	g ((E,xs) : prefix') matrix = do	1✔
439	cnf <- liftM (toCNF nv) $ f prefix' matrix	1✔
440	solver <- SAT.newSolver	1✔
441	SAT.newVars_ solver (CNF.cnfNumVars cnf)	1✔
442	forM_ (CNF.cnfClauses cnf) $ \clause -> do	1✔
443	SAT.addClause solver (SAT.unpackClause clause)	1✔
444	ret <- SAT.solve solver	1✔
445	if ret then do	1✔
446	m <- SAT.getModel solver	1✔
447	return (True, Just $ IntSet.fromList [if SAT.evalLit m x then x else -x \| x <- IntSet.toList xs])	1✔
448	else do	1✔
449	return (False, Nothing)	1✔
450	g ((A,xs) : prefix') matrix = do	1✔
451	cnf <- liftM (toCNF nv . negateCNFOrDNF) $ f prefix' matrix	1✔
452	solver <- SAT.newSolver	1✔
453	SAT.newVars_ solver (CNF.cnfNumVars cnf)	1✔
454	forM_ (CNF.cnfClauses cnf) $ \clause -> do	1✔
455	SAT.addClause solver (SAT.unpackClause clause)	1✔
456	ret <- SAT.solve solver	1✔
457	if ret then do	1✔
458	m <- SAT.getModel solver	1✔
459	return (False, Just $ IntSet.fromList [if SAT.evalLit m x then x else -x \| x <- IntSet.toList xs])	1✔
460	else do	1✔
461	return (True, Nothing)	1✔
462	g prefix matrix = do	1✔
463	ret <- f prefix matrix	1✔
464	case ret of	1✔
465	CNF xs -> return (not (any IntSet.null xs), Nothing)	1✔
466	DNF xs -> return (any IntSet.null xs, Nothing)	×
467
468	f :: Prefix -> [SAT.Clause] -> IO CNFOrDNF
469	f [] matrix = return $ CNF [IntSet.fromList clause \| clause <- matrix]	1✔
470	f ((E,xs) : prefix') matrix = do	1✔
471	cnf <- liftM (toCNF nv) $ f prefix' matrix	1✔
472	dnf <- QE.shortestImplicantsE (xs `IntSet.union` IntSet.fromList [nv+1 .. CNF.cnfNumVars cnf]) cnf	1✔
473	return $ DNF dnf	1✔
474	f ((A,xs) : prefix') matrix = do	1✔
475	cnf <- liftM (toCNF nv . negateCNFOrDNF) $ f prefix' matrix	1✔
476	dnf <- QE.shortestImplicantsE (xs `IntSet.union` IntSet.fromList [nv+1 .. CNF.cnfNumVars cnf]) cnf	1✔
477	return $ negateCNFOrDNF $ DNF dnf	1✔
478
479	-- ----------------------------------------------------------------------------
480
481	-- ∀y ∃x. x ∧ (y ∨ ¬x)
482	_test :: IO (Bool, Maybe LitSet)
483	_test = solveNaive 2 [(A, IntSet.singleton 2), (E, IntSet.singleton 1)] (x .&&. (y .\|\|. notB x))	×
484	where
485	x = litToMatrix 1	×
486	y = litToMatrix 2	×
487
488	_test' :: IO (Bool, Maybe LitSet)
489	_test' = solveCEGAR 2 [(A, IntSet.singleton 2), (E, IntSet.singleton 1)] (x .&&. (y .\|\|. notB x))	×
490	where
491	x = litToMatrix 1	×
492	y = litToMatrix 2	×
493
494	_test1 :: (Int, Prefix, Matrix)
495	_test1 = prenexAnd (1, [(A, IntSet.singleton 1)], litToMatrix 1) (1, [(A, IntSet.singleton 1)], notB (litToMatrix 1))	×
496
497	_test2 :: (Int, Prefix, Matrix)
498	_test2 = prenexOr (1, [(A, IntSet.singleton 1)], litToMatrix 1) (1, [(A, IntSet.singleton 1)], litToMatrix 1)	×

msakai / toysolver / 767

Source File Press 'n' to go to next uncovered line, 'b' for previous

Source File
Press 'n' to go to next uncovered line, 'b' for previous