msakai / toysolver / 563

Committed 15 Dec 2024 01:20AM UTC coverage: 71.768% (+0.5%) from 71.267%

Build # 563

Build Type

push

github

Committed by

web-flow

Commit Message

update URL of “Existential Quantification as Incremental SAT”

Run Details

10438 of 14544 relevant lines covered (71.77%)

0.72 hits per line

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

97.44

/src/ToySolver/SAT/ExistentialQuantification.hs

{-# 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
  { forwardMap :: SAT.VarMap (SAT.Var, SAT.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 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 (SAT.unpackLit x)) forward of
        Nothing -> x
        Just (xp,xn) -> SAT.packLit $ 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
      ]

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

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

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

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

1	{-# Language BangPatterns #-}
2	{-# OPTIONS_GHC -Wall #-}
3	{-# OPTIONS_HADDOCK show-extensions #-}
4	----------------------------------------------------------------------
5	-- \|
6	-- Module : ToySolver.SAT.ExistentialQuantification
7	-- Copyright : (c) Masahiro Sakai 2017
8	-- License : BSD-style
9	--
10	-- Maintainer : masahiro.sakai@gmail.com
11	-- Stability : provisional
12	-- Portability : non-portable
13	--
14	-- References:
15	--
16	-- * [BrauerKingKriener2011] Jörg Brauer, Andy King, and Jael Kriener,
17	-- "Existential quantification as incremental SAT," in Computer Aided
18	-- Verification (CAV 2011), G. Gopalakrishnan and S. Qadeer, Eds.
19	-- pp. 191-207.
20	-- <https://www.cs.kent.ac.uk/pubs/2011/3094/content.pdf>
21	--
22	----------------------------------------------------------------------
23	module ToySolver.SAT.ExistentialQuantification
24	( project
25	, shortestImplicantsE
26	, negateCNF
27	) where
28
29	import Control.Monad
30	import qualified Data.IntMap as IntMap
31	import qualified Data.IntSet as IntSet
32	import Data.IORef
33	import qualified Data.Vector.Generic as VG
34	import ToySolver.FileFormat.CNF as CNF
35	import ToySolver.SAT as SAT
36	import ToySolver.SAT.Types as SAT
37
38	-- -------------------------------------------------------------------
39
40	data Info
41	= Info
42	{ forwardMap :: SAT.VarMap (SAT.Var, SAT.Var)	1✔
43	, backwardMap :: SAT.VarMap SAT.Lit	1✔
44	}
45
46	-- \| Given a set of variables \(X = \{x_1, \ldots, x_k\}\) and CNF formula \(\phi\), this function
47	--
48	-- * duplicates \(X\) with \(X^+ = \{x^+_1,\ldots,x^+_k\}\) and \(X^- = \{x^-_1,\ldots,x^-_k\}\),
49	--
50	-- * replaces positive literals \(x_i\) with \(x^+_i\), and negative literals \(\neg x_i\) with \(x^-_i\), and
51	--
52	-- * adds constraints \(\neg x^+_i \vee \neg x^-_i\).
53	dualRailEncoding
54	:: SAT.VarSet -- ^ \(X\)
55	-> CNF.CNF -- ^ \(\phi\)
56	-> (CNF.CNF, Info)
57	dualRailEncoding vs cnf =	1✔
58	( cnf'	1✔
59	, Info	1✔
60	{ forwardMap = forward	1✔
61	, backwardMap = backward	1✔
62	}
63	)
64	where
65	cnf' =	1✔
66	CNF.CNF	1✔
67	{ CNF.cnfNumVars = CNF.cnfNumVars cnf + IntSet.size vs	1✔
68	, CNF.cnfNumClauses = CNF.cnfNumClauses cnf + IntSet.size vs	1✔
69	, CNF.cnfClauses =
70	[ VG.map f c \| c <- CNF.cnfClauses cnf ] ++	1✔
71	[ SAT.packClause [-xp,-xn] \| (xp,xn) <- IntMap.elems forward ]	1✔
72	}
73	f x =	1✔
74	case IntMap.lookup (abs (SAT.unpackLit x)) forward of	1✔
75	Nothing -> x	1✔
76	Just (xp,xn) -> SAT.packLit $ if x > 0 then xp else xn	1✔
77	forward =	1✔
78	IntMap.fromList	1✔
79	[ (x, (x,x'))	1✔
80	\| (x,x') <- zip (IntSet.toList vs) [CNF.cnfNumVars cnf + 1 ..]	1✔
81	]
82	backward = IntMap.fromList $ concat $	1✔
83	[ [(xp,x), (xn,-x)]	×
84	\| (x, (xp,xn)) <- IntMap.toList forward	1✔
85	]
86
87	{-
88	forwardLit :: Info -> Lit -> Lit
89	forwardLit info l =
90	case IntMap.lookup (abs l) (forwardMap info) of
91	Nothing -> l
92	Just (xp,xn) -> if l > 0 then xp else xn
93	-}
94
95	-- -------------------------------------------------------------------
96
97	cube :: Info -> SAT.Model -> LitSet
98	cube info m = IntSet.fromList $ concat $	1✔
99	[ if SAT.evalLit m xp then [x]	1✔
100	else if SAT.evalLit m xn then [-x]	1✔
101	else []	1✔
102	\| (x, (xp,xn)) <- IntMap.toList (forwardMap info)	1✔
103	]
104
105	blockingClause :: Info -> SAT.Model -> Clause
106	blockingClause info m = [-y \| y <- IntMap.keys (backwardMap info), SAT.evalLit m y]	1✔
107
108	-- \| Given a set of variables \(X = \{x_1, \ldots, x_k\}\) and CNF formula \(\phi\),
109	-- this function computes shortest implicants of \(\exists X. \phi\).
110	--
111	-- Resulting shortest implicants form a DNF (disjunctive normal form) formula that is
112	-- equivalent to the original formula \(\exists X. \phi\).
113	shortestImplicantsE
114	:: SAT.VarSet -- ^ \(X\)
115	-> CNF.CNF -- ^ \(\phi\)
116	-> IO [LitSet]
117	shortestImplicantsE xs formula = do	1✔
118	let (tau_formula, info) = dualRailEncoding (IntSet.fromList [1 .. CNF.cnfNumVars formula] IntSet.\\ xs) formula	1✔
119	solver <- SAT.newSolver	1✔
120	SAT.newVars_ solver (CNF.cnfNumVars tau_formula)	1✔
121	forM_ (CNF.cnfClauses tau_formula) $ \c -> do	1✔
122	SAT.addClause solver (SAT.unpackClause c)	1✔
123
124	ref <- newIORef []	1✔
125
126	let lim = IntMap.size (forwardMap info)	1✔
127
128	loop !n \| n > lim = return ()	×
129	loop !n = do	1✔
130	sel <- SAT.newVar solver	1✔
131	SAT.addPBAtMostSoft solver sel [(1,l) \| l <- IntMap.keys (backwardMap info)] (fromIntegral n)	1✔
132	let loop2 = do	1✔
133	b <- SAT.solveWith solver [sel]	1✔
134	when b $ do	1✔
135	m <- SAT.getModel solver	1✔
136	let c = cube info m	1✔
137	modifyIORef ref (c:)	1✔
138	SAT.addClause solver (blockingClause info m)	1✔
139	loop2	1✔
140	loop2	1✔
141	SAT.addClause solver [-sel]	1✔
142	loop (n+1)	1✔
143
144	loop 0	1✔
145	reverse <$> readIORef ref	1✔
146
147	-- \| Given a CNF formula \(\phi\), this function returns another CNF formula \(\psi\)
148	-- that is equivalent to \(\neg\phi\).
149	negateCNF
150	:: CNF.CNF -- ^ \(\phi\)
151	-> IO CNF.CNF -- ^ \(\psi \equiv \neg\phi\)
152	negateCNF formula = do	1✔
153	implicants <- shortestImplicantsE IntSet.empty formula	1✔
154	return $	1✔
155	CNF.CNF	1✔
156	{ CNF.cnfNumVars = CNF.cnfNumVars formula	1✔
157	, CNF.cnfNumClauses = length implicants	1✔
158	, CNF.cnfClauses = map (SAT.packClause . map negate . IntSet.toList) implicants	1✔
159	}
160
161	-- \| Given a set of variables \(X = \{x_1, \ldots, x_k\}\) and CNF formula \(\phi\),
162	-- this function computes a CNF formula \(\psi\) that is equivalent to \(\exists X. \phi\)
163	-- (i.e. \((\exists X. \phi) \leftrightarrow \psi\)).
164	project
165	:: SAT.VarSet -- ^ \(X\)
166	-> CNF.CNF -- ^ \(\phi\)
167	-> IO CNF.CNF -- ^ \(\psi\)
168	project xs cnf = do	1✔
169	let ys = IntSet.fromList [1 .. CNF.cnfNumVars cnf] IntSet.\\ xs	1✔
170	nv = if IntSet.null ys then 0 else IntSet.findMax ys	1✔
171	implicants <- shortestImplicantsE xs cnf	1✔
172	let cnf' =	1✔
173	CNF.CNF	1✔
174	{ CNF.cnfNumVars = nv	1✔
175	, CNF.cnfNumClauses = length implicants	1✔
176	, CNF.cnfClauses = map (SAT.packClause . map negate . IntSet.toList) implicants	1✔
177	}
178	negated_implicates <- shortestImplicantsE xs cnf'	1✔
179	let implicates = map (SAT.packClause . map negate . IntSet.toList) negated_implicates	1✔
180	return $	1✔
181	CNF.CNF	1✔
182	{ CNF.cnfNumVars = nv	1✔
183	, CNF.cnfNumClauses = length implicates	1✔
184	, CNF.cnfClauses = implicates	1✔
185	}

msakai / toysolver / 563

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